What does the ocaml type 'a. 'a -> 'a mean?

Question

In the ocaml language specification, there's a short section:

poly-typexpr ::= typexpr
               | { ' ident }+ . typexpr

There's no explanation in the text, and the only instance of poly-typexpr is in defining a method type:

method-type ::= method-name : poly-typexpr

What does this allow me to do?

Answer 1

See section 3.11 "Polymorphic methods". Scroll down to "Of course the constraint may also be an explicit method type..."

Answer 2

poly-typexpr is also allowed as the type of a record field (see Section 6.8.1). These are commonly called "existential types," though there is some debate on that point. Using a polymorphic type in this way changes the scope of the type variable. For example, compare the types:

type 'a t = { f : 'a -> int; }
type u = { g : 'a. 'a -> int; }

t is really a family of types, one for each possible value of 'a. Each value of type 'a t must have a field f with the type 'a -> int. For example:

# let x = { f = fun i -> i+1; } ;;
val x : int t = {f = <fun>}
# let y = { f = String.length; } ;;
val y : string t = {f = <fun>}

In comparison, u is a single type. Each value of type u must have a field g with the type 'a -> int for any 'a. For example:

# let z = { g = fun _ -> 0; } ;;
val z : u = {g = <fun>}

Note here that g doesn't depend on the type of its input at all; if it did, it wouldn't have the type 'a. 'a -> int. For example:

# let x2 = { g = fun i -> i+1; } ;;
This field value has type int -> int which is less general than 'a. 'a -> int