ocaml GADT: почему «типа a». нужно?

Question

В базовом примере GADT из §7.20 из ocaml manual, что означает «тип a». ? Почему объявления "eval: термин -> a" недостаточно?

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) 

Answer 1

slide на ML'2011 мастерской Жака имеет хорошее введение. Идея использовать синтаксис локально абстрактного типа для введения универсальной переменной с выражением.