In this post, I explain a common mistake when writing constraints of polymorphic functions in OCaml programs, then show how to correct it.

## Not-so-polymorphic constraints

One of the earliest lessons of any functional programming tutorial is how to write polymorphic functions and their signatures:

```
val id : 'a -> 'a
val fst : ('a * 'b) -> 'a
val map : ('a -> 'b) -> 'a list -> 'b list
```

A typical explanation of these type signatures goes along the lines of:

Types of the form`'a`

,`'b`

, ..., known astype variables, stand for an unknown type. They allow us to describe functions that work uniformly over many possible input types. This is known as "parametric polymorphism".— Hypothetical education resource

^{1}

As is often the case with introductory explanations, this is *just* specific
enough to be technically correct without introducing too many new concepts,
letting us hurry on to demonstrating useful examples before the student gets
bored. Unfortunately, we've laid a trap: when our reader learns about type
constraints, they naturally try to combine these two "intuitive" features and
get bitten:

```
ᐅ let id1 : 'a -> 'a = (fun x -> x) ;; (* Accepted. So far so good... *)
val id1 : 'a -> 'a = <fun>
ᐅ let id2 : 'a -> 'a = (fun x -> x + 1) ;; (* Also accepted. Uh oh... *)
val id2 : int -> int = <fun>
```

In this case, the student finds that `'a -> 'a`

is a valid constraint for a
function of type `int -> int`

, and their mental model is broken almost
immediately. It's quite natural to expect `id2`

to be rejected as a
non-polymorphic function, particularly given our vague explanation of what `'a`

actually means.

Our hypothetical student's mistake stems from the fact that type variables in
signatures are implicitly *universally-quantified* – that is, they stand for
*all* types – whereas type variables in constraints are not. To understand what
this means, let's try to pin down a more precise idea of what type variables
*are*. If you're already ~~indoctrinated~~ comfortable with type
variables, you may wish to cut to the chase.

## What is a type variable anyway?

Type variables in constraints are referred to as being "unbound" (or "free"),
meaning that they stand for *some* type that is not yet known to the
type-checker: they are placeholders that can later be filled by a particular
type. Without going into the details, these placeholders are
gradually determined as the type-checker resolves constraints. For instance, in
our `id2`

example, the type-checker decides that `'a`

equals `int`

by first
reconciling the user-supplied constraint `'a -> 'a`

with the constraint
`int -> int`

that it inferred from the implementation.

To a theorist (or type-system developer), who regularly has to worry about types
that are not yet fully known, the notion of a "placeholder" is a sensible
default meaning of an unbound type variable. Such people also tend to use
explicit syntax to disambiguate the alternative case, type variables that *are*
bound:

`∀ a. a -> a`

$\quad$ (read as:"For all)`a`

,`a -> a`

"

We call "`∀ a`

" a *universal quantifier* because it introduces a variable `a`

,
bound inside the quantifier, that can stand for any type in the universe of
OCaml types. It's this flavour of type variable that enables parametric
polymorphism and – although the OCaml syntax often tries to hide it from you –
these quantifiers exist everywhere in your programs. As I already mentioned, all
unbound variables in *signatures* are implicitly quantified in this way:

`val length : 'a list -> int`

... secretly means ...

`val length : ∀ a. a list -> int`

On the implementation side of `length`

, the compiler will check to see if there
are any placeholder variables left after type-checking the definition and wrap
them in universal quantifiers (if it's sure that it's safe to do so^{2}). When
this happens, we say that those type variables have been *generalised*. Once
`length`

has been given its polymorphic type, the user gets to pick a specific
type `a`

at each call-site by passing it a list of any element type they want.
This idea of choosing the instantiation of `a`

at each call-site is what is
"parametric" about "parametric polymorphism".

Taking a step back, we can now see what went wrong with our hypothetical
introduction to type variables above: it led our student to think of all type
variables as being implicitly universally-quantified, when this is not true in
constraints^{3}. So, given that we can't rely on implicit generalisation in
constraints, what *can* we do to declare that our code is polymorphic within the
implementation itself?

## True polymorphic constraints

The punchline is that OCaml actually *does* have syntax for expressing
polymorphic constraints – and it even involves an explicit quantifier – but
sadly it's not often taught to beginners:

```
let id : 'a. 'a -> 'a = (fun x -> x + 1)
```

The syntax `'a. 'a -> 'a`

denotes an explicitly-polymorphic
type, where `'a.`

corresponds directly with the
`∀ a.`

quantifier we've been using so far. Applying it here gives us a
satisfyingly readable error message:

```
Error: This definition has type int -> int which is less general than
'a. 'a -> 'a
```

The caveat of polymorphic constraints is that we can only apply them directly to
`let`

-bindings, not to function bodies or other forms of expression:

```
let panic : 'a. unit -> 'a = (fun () -> raise Crisis) (* Works fine... *)
let panic () : 'a. 'a = raise Crisis (* Uh oh... *)
(* ^
* Error: Syntax error *)
```

This somewhat unhelpful error message arises because OCaml will never infer a
polymorphic type for a value that is not `let`

-bound. Trying to make your type
inference algorithm cleverer than this quickly runs into certain undecidable
problems; the parser knows that the type-checker is
afraid of undecidable problems, and so rejects the program straight away^{4}.

In spite of their limitations, explicitly-polymorphic type constraints are a great way to express polymorphic intent in your OCaml programs, either as internal documentation or to have more productive conversations with the type-checker when debugging. I recommend using them frequently and teaching them to beginners as soon as possible.

At this point, if you suffered through my explanation of type variables in the previous section, you may be thinking the following:

"If introducing type variables properly requires so many paragraphs of jargon, weshouldn'tburden beginners with the details right away."— Straw-man argument

Personally, I find that introducing these terms early on in the learning process is easily worthwhile in avoiding early roadblocks, but that discussion can wait for another time. In the spirit of functional programming for the masses, let's summarise with a less jargon-heavy attempt at redrafting our hypothetical education resource:

Types of the form`'a`

,`'b`

, ..., known as type variables, are placeholders for an undetermined type. When bound by for-all quantifiers (of the form`'a.`

), they can be used to describe values that can take on many possible types. For instance, we can write the type of`(fun x -> x)`

as`'a. 'a -> 'a`

, meaning:

"For any type`'a`

, this function can take on type`'a -> 'a`

."

The OCaml type-checker will infer polymorphic types wherever it is safe, but we can also explicitly specify a polymorphic type for a`let`

-binding:`ᐅ let fst : 'a 'b. ('a * 'b) -> 'a = (* "For all ['a] and ['b], ..." *) fun (x, _) -> x ;; val fst : 'a * 'b -> 'a = <fun>`

Note that all type variables in signatures are implicitly universally-quantified: it's not necessary (or even possible) to write`'a 'b.`

before the type.

The explanation is undeniably still longer and more technical than the one we started with, but crucially it uses the extra space to give the reader a clue as to how to debug their polymorphic functions.

The story doesn't end here. We haven't discussed existential quantifiers, the other type of type variable binding; or polymorphic recursion, where polymorphic annotations become compulsory; or locally-abstract types, which offer other useful syntaxes for constraining your OCaml programs to be polymorphic. These will all have to wait for future posts. For now, thanks for reading!

Very similar equivalents of this explanation exist in Real World OCaml, Cornell's OCaml course, and Cambridge's OCaml course. Type variables are variously described as representing

*"any type"*,*"an unknown type"*or*"a generic type"*; explanations that are all as different as they are vague.↩The most famous example of a type variable that is unsafe to generalise is one that has been captured in mutable state:

`ᐅ let state = ref [] ;; ᐅ let sneaky_id x = (state := x :: !state); x ;; val sneaky_id : '_weak1 -> '_weak1 = <fun>`

In this case, it's not possible to give

`sneaky_id`

the type`∀ a. a -> a`

because different choices of the type`a`

are not independent: passing a string to`sneaky_id`

, followed by an integer, would build a list containing both strings and integers, violating type safety. Instead,`sneaky_id`

is given a type containing a "weak type variable" which represents a single, unknown type. This meaning of type variables should be familiar to you; it's exactly the same as the "unbound" type variables we've been discussing!In general, it's not easy to decide if it's safe to generalise a particular type variable. OCaml makes a quick under-approximation called the (relaxed) value restriction.

As an aside, there's no profound reason why constraints must behave differently with respect to implicit quantification. Both SML and Haskell choose to generalise variables in constraints:

`val id1 : 'a -> 'a = (fn x => x + 1); (* Error: pattern and expression in val dec do not agree pattern: 'a -> 'a expression: 'Z[INT] -> 'Z[INT] *)`

(Note:

`val f : t = e`

in SML is analogous to`let f : t = e`

in OCaml.)I suspect that constraints having the same quantification behaviour as signatures is more intuitive, at least for simple examples. In complex cases, the exact point at which type variables are implicitly quantified can be surprising, and so SML '97 provides an explicit quantification syntax for taking control of this behaviour. See the SML/NJ guide (§ 1.1.3) for much more detail.

The advantage of OCaml's approach is that it enables constraining

*subcomponents*of types without needing to specify the entire thing (as in`(1, x) : (int * _)`

), which can be useful when quickly constraining types as a sanity check or for code clarity. As far as I'm aware, SML has no equivalent feature.This limitation of the type-checker can artificially limit the polymorphism that can be extracted from your programs. If you want to take polymorphism to its limits – as God intended – it's sometimes necessary to exploit another point where explicitly-polymorphic types can appear: record and object fields.↩