OCaml `type a. at` синтаксис

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?

Это характерно для GADT?

Answer 1

В руководстве описывается синтаксис несколько разделов вверх: http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc80

Короче говоря, type a. ... означает, что локально абстрактный тип a должен быть полиморфными.