syntaxocamlgadtlocally-abstract-type

OCaml's `type a. a t` syntax

I've just come across the following code snippet in 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)

which, once evaluated in utop, has the following signature:

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

I also noticed that, when replacing type a. a term -> a by 'a term -> 'a or just removing the signature, the function doesn't compile anymore.

...
| 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

So what is this notation? What makes it different of 'a t ?

Is it specific to GADTs?

Solution

  • The manual explains the syntax a few sections up: http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc80

    In short, type a. ... means that the locally abstract type a must be polymorphic.