Miki Beta is based on datatype-generic programming

[1].
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

[2] as an example.

Two questions:

- 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 = |

| Leaf |

| Node of tree_t * int * tree_t |

(* Standard definition of list datatype in OCaml *)

type list_t = |

| Empty |

| 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

[3].
While the above example follows PolyP,
Indexed Functor represents indexed datatypes
so that it can construct mutually recursive datatypes.