16 CHAPTER 2. A TASTE OF CAML
boolean, or another function. Therefore, it is said to have polymorphic type, and
CAML displays a type involving type variables. These can later be set to some
particular type when it is used, different instances with different types.
#let I = fun x -> x;;
I : ’a -> ’a = <fun>
CAML prints type variables as ’a, ’b etc.; these are supposed to be ASCII
representations of α, β and so on. We can now use the polymorphic function
several times with different types:
#I true;;
- : bool = true
#I 1;;
- : int = 1
#I I I I 12;;
- : int = 12
Each instance of I in the last expression has a different type, and intuitively
corresponds to a different function. CAML always assigns the most general type
possible for an expression, without specializing it unnecessarily, using an algorithm
due to Milner (1978). For example, the following is a more complex definition of an
identity function; the reader may wish to study it to see why CAML gives all these
expressions the types it does,
6
and why I’ acts as an identity function. Note that
in contrast to most programming languages, CAML allows the prime character in
variable names, reflecting its background in logic and mathematics where variables
like x
are common.
#let K x y = x;;
K : ’a -> ’b -> ’a = <fun>
#let S f g x = (f x) (g x);;
S : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun>
#let I’ = S K K;;
I’ : ’_a -> ’_a = <fun>
#I’ 2;;
it : int = 2
In the above examples of polymorphic functions, the system very quickly infers a
most general type for each expression, and the type it infers is simple. This usually
happens in practice, but there are pathological cases, e.g. the following example due
to Mairson (1990). The type of this expression takes about 10 seconds to calculate,
and occupies over 4000 lines on an 80-column terminal.
let pair x y = fun z -> z x y in
let x1 = fun y -> pair y y in
let x2 = fun y -> x1(x1 y) in
let x3 = fun y -> x2(x2 y) in
let x4 = fun y -> x3(x3 y) in
let x5 = fun y -> x4(x4 y) in
x5(fun z -> z);;
Because of CAML’s automatic type inference, the programmer need never enter
a type. At least, CAML will already allocate as general a type as possible to an
6
Ignore the underscores for now. This is connected with the typing of imperative features, and
we will discuss it later.