ocamlgadtlocally-abstract-type

ocaml GADT : why "type a." needed?

In the basic example of GADT from§7.20 of ocaml manual, what is the meaning of 'type a.' ? Why declaring "eval : a term -> a" is not enough ?

type _ term =
          | Int : int -> int term
          | Add : (int -> int -> int) term
          | App : ('b -> 'a) term * 'b term -> 'a term

        let rec eval : type a. a term -> a = function
          | Int n    -> n                 (* a = int *)
          | Add      -> (fun x y -> x+y)  (* a = int -> int -> int *)
          | App(f,x) -> (eval f) (eval x)
Solution

  • Jacque's slide on ML'2011 workshop has a nice introduction. The idea to use syntax of locally abstract type to introduce universal expression-scoped variable.