ocaml GADT：爲什麼「鍵入a」。需要？

Question

在ocaml manual§7.20的GADT的基本示例中，「type 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

在ML'2011研討會上，雅克的slide有一個很好的介紹。使用本地抽象類型的語法來引入通用表達式範圍變量的想法。