Polymorphic type constraints

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 as type 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¹

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²). 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³. 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⁴.

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, we shouldn't burden 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!