test.ml

module Type = struct
  type _ t =
    | Bool : bool t
    | Int : int t
    | Float : float t
    | Tuple : (_, 't) tuple -> 't t

  and (_, _) tuple =
    | Nil : ('t, 't) tuple
    | Cons : 'a t * ('t -> 'a) * ('r, 't) tuple -> (('a -> 'r), 't) tuple
end

module Term = struct
  type _ t =
    | Bool : bool -> bool t
    | Int : int -> int t
    | Float : float -> float t
    | Agg : 't agg -> 't t
    | Elt : 't t * ('t -> 'a) -> 'a t

  and 't agg = Agg_ : 'f * ('f, 't) agg_part -> 't agg

  and (_, _) agg_part =
    | Nil : ('t, 't) agg_part
    | Cons : 'a t * ('r, 't) agg_part -> (('a -> 'r), 't) agg_part

  let rec eval : type a . a t -> a = function
    | Int n -> n
    | Bool b -> b
    | Float f -> f
    | Elt (t, f) -> f (eval t)
    | Agg (Agg_ (build, parts)) ->
      let rec loop : type v . v -> (v, a) agg_part -> a =
        fun b parts -> match parts with
          | Nil -> b
          | Cons (term, rest) -> loop (b (eval term)) rest
      in
      loop build parts
end

open Printf

let rec print : type a . a -> a Type.t -> unit =
  fun value -> function
  | Type.Int -> print_int value
  | Type.Bool -> printf "%b" value
  | Type.Float -> printf "%F" value
  | Type.Tuple Type.Nil -> print_string "()"
  | Type.Tuple (Type.Cons (elt_ty, getter, rest)) ->
    let rec loop : type a b . a -> (_, a) Type.tuple -> unit =
      fun tuple -> function
        | Type.Nil -> ()
        | Type.Cons (elt_ty, getter, rest) ->
          print_string ", ";
          print (getter tuple) elt_ty;
          loop tuple rest in
    print_char '(';
    print (getter value) elt_ty;
    loop value rest;
    print_char ')'