Miki Beta is based on datatype-generic programming 
Datatype-generic programming provides the genericity over the stucture of types.
It realizes such a genericity by representation of datatypes with a sum-of-product structure.
Here we will learn PolyP 
as an example.
- Define tree and list structures.
- Implement a function `get_params` that returns a list of all values
the given term (tree or list typed) contains
First, let us see how they can be defined in the standard OCaml.
(* Standard definition of tree datatype in OCaml *)
|type tree_t =|
|| Node of tree_t * int * tree_t|
(* Standard definition of list datatype in OCaml *)
|type list_t =|
|| Cons of int * list_t|
In the above program, tree and list structures are defined as OCaml standard datatypes.
Then, let's implement a `get_param` function for their types.
(* get_params_for_tree: tree_t -> int list *)
let rec get_params_for_tree t = match t with
| Leaf -> 
| Node (l, n, r) -> (get_params_for_tree l) @ [n] @ (get_params_for_tree r)
(* get_params_for_list: list_t -> int list *)
let rec get_params_for_list t = match t with
| Empty -> 
| Cons (n, r) -> n :: (get_params_for_list r)
Although the above two functions look similar to each other,
you have to define them separately.
It is because of the type dependency.
Whenever you define a new datatype, you have to add a corresponding function.
On the other hand, using datatype-generic terms,
the main functionality of `get_params` can be defined in a single function as follows.
(* Definition of the datatype to represent generic world *)
|type code_t =|
|| U||(* unit type||*)|
|| P||(* parameter type||*)|
|| I||(* recursive type||*)|
|| Plus of code_t * code_t||(* sum type||*)|
|| Times of code_t * code_t||(* product type||*)|
(* Definition of a represented tree datatype *)
let tree_type =
Plus (U, Times (Times (I, P), I))
(* Definition of a represented list datatype *)
let list_type =
Plus (U, Times (P, I))
(* get_params: code_t -> code_t -> type_f -> int list *)
let rec get_params c r t = match (c, t) with
| (U, Unit ()) -> 
| (I, Rec (t')) -> get_params r r t'
| (P, Par (n)) -> [n]
| (Plus (c1, c2), Sum (Left (t'))) -> get_params c1 r t'
| (Plus (c1, c2), Sum (Right (t'))) -> get_params c2 r t'
| (Times (c1, c2), Pair (t1', t2')) -> (get_params c1 r t1') @ (get_params c2 r t2')
| _ -> failwith "Should not happen"
(* get_params_for_tree: type_f -> int list *)
let get_params_for_tree = get_params tree_type tree_type
(* get_params_for_list: type_f -> int list *)
let get_params_for_list = get_params list_type list_type
Even if you add another representation of datatype, the above function `get_params` works for it.
This is how the datatype-generic programming makes your program smaller.
Miki Beta mixes features of PolyP and Indexed Functors 
While the above example follows PolyP,
Indexed Functor represents indexed datatypes
so that it can construct mutually recursive datatypes.