syntax - OCaml 的 `type a. a t` 语法

Question

我刚刚在 OCaml's documentation about GADTs 中遇到以下代码片段:

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

一旦在 utop 中进行评估，它具有以下签名:

val eval : 'a term -> 'a = <fun>

我还注意到，在更换 type a. a term -> a 时来自 'a term -> 'a或者只是删除签名，该函数不再编译。

...
| Add -> (fun x y -> x + y)
...
Error: This pattern matches values of type (int -> int -> int) term
  but a pattern was expected which matches values of type int term
  Type int -> int -> int is not compatible with type int 

那么这个记法是什么呢？ 'a t 的不同之处?

它特定于 GADTs 吗？

Answer 1

该手册解释了几个部分的语法:http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc80

总之，type a. ...表示本地抽象类型a必须是多态的。