OCaml `type a. syntax t`

I just looked at the following piece of code in the OCaml Documentation about GADT :

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 after computation in utop has the following signature:

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

      

I also noticed that when replacing type a. a term -> a

with 'a term -> 'a

or just removing the signature, the function no longer compiles.

...
| 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 designation? What makes it different from 'a t

?

Is this GADT specific?

+3


source to share


1 answer


The manual explains the syntax of several sections: http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc80



In short, it type a. ...

means that a locally abstract type a

must be polymorphic.

+2


source







All Articles