Playing with GADTs

gadt.ml

module type LANG =
  sig
    type 'a t

    val eval : 'a t -> 'a
  end

module L1 : LANG =
  struct
    type _ t =
      | Int : int -> int t
      | Add : (int -> int -> int) t
      | App : ('a -> 'b) t * 'a t -> 'b t

    let rec eval : type a . a t -> a =
      function
      | Int n      -> n
      | Add        -> (+)
      | App (f, x) -> (eval f) (eval x)

    let rec sum : type a. a t -> _ =
      fun x ->
        let y =
          match x with
          | Int n      -> n
          | Add        -> 0
          | App (f, x) -> sum f + sum x
        in
        y + 1

    let two = eval (App (App (Add, Int 1), Int 1))
  end

module L2 : LANG =
  struct
    type _ t =
      | Pair : 'a t * 'b t -> ('a * 'b) t
      | Fst  : ('a * 'b) t -> 'a t
      | Snd  : ('a * 'b) t -> 'b t

    let rec eval : type a . a t -> a =
      function
      | Pair (a, b) -> eval a, eval b
      | Fst  t      -> fst @@ eval t
      | Snd  t      -> snd @@ eval t
  end

module L3 : LANG =
  struct
    type _ t =
      | Int  : int                  -> int       t
      | Bool : bool                 -> bool      t
      | Add  : int  t * int  t      -> int       t
      | And  : bool t * bool t      -> bool      t
      | If   : bool t * 'a t * 'a t -> 'a        t
      | Pair : 'a   t * 'b t        -> ('a * 'b) t
      | Fst  : ('a * 'b) t          -> 'a        t
      | Snd  : ('a * 'b) t          -> 'b        t

    let rec eval : type a. a t -> a =
      function
      | Int  i -> i
      | Bool b -> b
  end