OCaml GADT: 为什么需要使用 "type a."？

Question

在OCaml手册的§7.20的GADT基本示例中，“type a.”的含义是什么？ 为什么声明“eval：a term -> 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)

- Pierre G.

---

我不是类型理论学家，但通过阅读@nnarklrh提供的参考资料，我认为eval函数需要多态递归，并且type a. ...的存在部分是为了打开对其的支持信号。如果省略type，则会出现尝试在不允许使用多态递归时使用它所期望的错误。 - Jeffrey Scofield

Answer 1

Jacque在ML'2011研讨会上的幻灯片有一个很好的介绍。使用局部抽象类型的语法来引入通用表达式范围变量的想法。

- objmagic