Let Polymorphism

Now we'll add let expressions to our little language:

e ::= x | i | b | e1 bop e2
    | if e1 then e2 else e3
    | fun x -> e
    | e1 e2
    | let x = e1 in e2   (* new *)

It turns out type inference for them is considerably trickier than might be expected.

An overly restrictive rule for let

The naive approach would be to add this constraint generation rule:

env |- let x = e1 in e2 : t2 -| C1, C2
  if env |- e1 : t1 -| C1
  and env, x : t1 |- e2 : t2 -| C2

From the type checking perspective, that's the same rule we've always used. And for many let expressions it works perfectly fine. For example:

{} |- let x = 42 in x : int -| {}
  {} |- 42 : int -| {}
  x : int |- x : int -| {}

The problem is that when the value being bound is a polymorphic function, that rule generates constraints that are too restrictive. For example, consider the identity function:

let id = fun x -> x in
let a = id 0 in
id true

OCaml has no trouble inferring the type of id as 'a -> 'a and permitting it to be applied both to an int and a bool. But the rule above isn't so permissive about application to both types. When we use it, we generate the following types and constraints:

{} |- let id = fun x -> x in (let a = id 0 in id true) : 'c -| 'a -> 'a = int -> 'b, 'a -> 'a = bool -> 'c
  {} |- fun x -> x : 'a -| {}
    x : 'a |- x : 'a -| {}
  id : 'a -> 'a |- let a = id 0 in id true : 'c -| 'a -> 'a = int -> 'b, 'a -> 'a = bool -> 'c   <--- POINT 1
    id : 'a -> 'a |- id 0 : 'b -| 'a -> 'a = int -> 'b
      id : 'a -> 'a |- id : 'a -> 'a -| {}
      id : 'a -> 'a |- 0 : int -| {}
    id : 'a -> 'a, a : 'b |- id true : 'c -| 'a -> 'a = bool -> 'c   <--- POINT 2
      id : 'a -> 'a, a : 'b |- id : 'a -> 'a -| {}
      id : 'a -> 'a, a : 'b |- true : bool -| {}

Notice that we do infer a type 'a -> 'a for id, which you can see in the environment in later lines of the example. But, at Point 1, we infer a constraint 'a -> 'a = int -> 'b, and at Point 2, we infer 'a -> 'a = bool -> 'c. When the unification algorithm encounters those constraints, it will break them down into 'a = int, 'a = 'b, 'a = bool, and 'a = 'c. The first and third of those are contradictory, because we can't have 'a = int and 'a = bool. One or the other will be substituted away during unification, leaving an unsatisfiable constraint int = bool. At that point unification will fail, declaring the program to be ill typed.

The problem is that the 'a type variable in the inferred type of id stands for an unknown but fixed type. At each application of id, we want to let 'a become a different type, instead of forcing it to always be the same type.

Type schemes

The solution to the problem of polymorphism for let expressions is not simple. It requires us to introduce a new kind of type: a type scheme. Type schemes resemble universal quantification from mathematical logic. For example, in logic you might write, "for all natural numbers $x$, it holds that $0 \cdot x = 0$". The "for all" is the universal quantification: it abstracts away from a particular $x$ and states a property that is true of all natural numbers.

A type scheme is written 'a . t, where 'a is a type variable and t is a type in which 'a may appear. For example, 'a . 'a -> 'a is a type scheme. It is the type of a function that takes in a value of type 'a and returns a value of type 'a, for all 'a. Thus, it is the type of the polymorphic identity function.

We can also have many type variables to the left of the dot in a type scheme. For example, 'a 'b . 'a -> 'b -> 'a is the type of a function that takes in two arguments and returns the first. In OCaml, we could write that as fun x y -> x. Note that utop infers the type of it as we would expect:

# let f = fun x y -> x;;
val f : 'a -> 'b -> 'a = <fun>

But we could actually manually write down an annotation with a type scheme:

# let f : 'a 'b . 'a -> 'b -> 'a = fun x y -> x;;
val f : 'a -> 'b -> 'a = <fun>

Note that OCaml accepts our manual type annotation but doesn't include the 'a 'b . part of it in its output. But it's implicitly there and always has been. In general, anytime OCaml has inferred a type t and that type has had type variables in it, in reality it's a type scheme. For example, the type of List.length is really a type scheme:

# let mylen : 'a . 'a list -> int = List.length;;
val mylen : 'a list -> int = <fun>

OCaml just doesn't bother outputting the list of type variables that are to the left of the dot in the type scheme. Really they'd just clutter the output, and many programmers never need to know about them. But now that you're learning type inference, it's time for you to know.

A better rule for let

Now we'll have static environments map names to type schemes. We can think of types as being special cases of type schemes in which the list of type variables is empty. With type schemes, the let rule changes in only one way from the naive rule above, which is the generalize on the last line:

env |- let x = e1 in e2 : t2 -| C1, C2
  if env |- e1 : t1 -| C1
  and generalize(C1, env, x : t1) |- e2 : t2 -| C2

The job of generalize is to take a type like 'a -> 'a and generalize it into a type scheme like 'a . 'a -> 'a in an environment env against constraints C1. Let's come back to how it works in a minute. Before that, there's one other rule that needs to change, which is the name rule:

env |- n : instantiate(env(t)) -| {}

The only thing that changes there is that use of instantiate. Its job is to take a type scheme like 'a . 'a -> 'a and instantiate it into a new type (and here we strictly mean a type, not a type scheme) with fresh type variables. For example, 'a . 'a -> 'a could be instantiated as 'b -> 'b, if 'b isn't yet in use anywhere else as a type variable.

Here's how those two revised rules work together to get our earlier example with the identify function right:

{} |- let id = fun x -> x in (let a = id 0 in id true)
  {} |- fun x -> x : 'a -> 'a -| {}
    x : 'a |- x : 'a -| {}
  id : 'a . 'a -> 'a |- let a = id 0 in id true   <--- POINT 1

Let's pause there at Point 1. When id is put into the environment by the let rule, its type is generalized from 'a -> 'a to 'a . 'a -> 'a; that is, from a type to a type scheme. That records the fact that each application of id should get to use its own value for 'a. Going on:

{} |- let id = fun x -> x in (let a = id 0 in id true)
  {} |- fun x -> x : 'a -> 'a -| {}
    x : 'a |- x : 'a -| {}
  id : 'a . 'a -> 'a |- let a = id 0 in id true   <--- POINT 1
    id : 'a . 'a -> 'a |- id 0
      id : 'a . 'a -> 'a |- id : 'b -> 'b -| {}   <--- POINT 3

Pausing here at Point 3, when id is applied to 0, we instantiate its type variable 'a with a fresh type variable 'b. Let's finish:

{} |- let id = fun x -> x in (let a = id 0 in id true) : 'e -| 'b -> 'b = int -> 'c, 'd -> 'd = bool -> 'e
  {} |- fun x -> x : 'a -> 'a -| {}
    x : 'a |- x : 'a -| {}
  id : 'a . 'a -> 'a |- let a = id 0 in id true : 'e -| 'b -> 'b = int -> 'c, 'd -> 'd = bool -> 'e   <--- POINT 1
    id : 'a . 'a -> 'a |- id 0 : 'c -| 'b -> 'b = int -> 'c
      id : 'a . 'a -> 'a |- id : 'b -> 'b -| {}   <--- POINT 3
      id : 'a . 'a -> 'a |- 0 : int -| {}
    id : 'a . 'a -> 'a, a : 'b |- id true : 'e -| 'd -> 'd = bool -> 'e   <--- POINT 2
      id : 'a . 'a -> 'a, a : 'b |- id : 'd -> 'd -| {}   <--- POINT 4
      id : 'a . 'a -> 'a, a : 'b |- true : bool -| {}

At Point 4, when id is applied to true, we again instantiate its type variable 'a with a fresh type variable, this time 'd. So the contraints collected at Points 1 and 2 are no longer contradictory, because they are talking about different type variables. Those contraints are:

'b -> 'b = int -> 'c
'd -> 'd = bool -> 'e

The unification algorithm will therefore conclude:

'b = int
'c = int
'd = bool
'e = bool

So the entire expression is successfully inferred to have type bool.

Instantiation and generalization

We used two new functions, instantiate and generalize, to define type inference for let expressions. Now we need to define those functions.

The easy one is instantiate. Given a type scheme 'a1 'a2 ... 'an . t, we instatiate it by:

• choosing n fresh type variables, and
• substituting each of those for 'a1 through 'an in t.

Substitution is uncomplicated here, compared to how it was for evaluation in thee substitution model, because there is nothing in a type that can bind variable names.

But generalize requires more work. Here's the let rule again:

env |- let x = e1 in e2 : t2 -| C1, C2
  if env |- e1 : t1 -| C1
  and generalize (C1, env, x : t1) |- e2 : t2 -| C2

To generalize t1, we do the following.

First, we pretend like e1 is all that matters, and that the rest of the let expression doesn't exist. If e1 were the entire program, how would we finish type inference? We'd run the unification algorithm on C1, get a substitution S, and return t1 S as the inferred type of e1. So, do that now. Let's call that inferred type u1. Let's also apply S to env to get a new environment env1, which now reflects all the type information we've gleaned from e1.

Second, we figure out which type variables in u1 should be generalized. Why not all of them? Because some type variables could have been introduced by code that surrounds the let expression, e.g.,

fun x ->
  (let y = e1 in e2) (let z = e3 in e4)

The type variable for x should not be generalized in inferring the type of either y or z, because x has to have the same type in all four subexpressions, e1 through e4. Generalizing could mistakenly allow x to have one type in e1 and e2, but a different type in e3 and e4.

So instead we generalize only variables that are in u1 but are not in env1. That way we generalize only the type variables from e1, not variables that were already in the environment when we started inferring the let expression's type. Suppose those variables are 'a1 ... 'an. The type scheme we give to x is then 'a1 ... 'an . u1.

Putting all that together, we end up with:

generalize(C1, env, x : t1) =
  env1, x : 'a1 ... 'an . u1

Returning to our example with the identify function from above, we had generalize({}, {}, x : 'a -> 'a). In that rather simple case, unify discovers no new equalities from the environment, so u1 = 'a -> 'a and env1 = {}. The only type variable in u1 is 'a, and it doesn't appear in env1. So 'a is generalized, yielding 'a . 'a -> 'a as the type scheme for id.

Mutability rears its ugly head again

There is yet one more complication to type inference for let expressions. It appears when we add mutable references to the language. Consider this example code, which does not type check in OCaml:

let succ = fun x -> ( + ) 1 x;;
let id = fun x -> x;;
let r = ref id;;
r := succ;;
!r true;;  (* error *)

It's clear we should infer succ : int -> int and id : 'a . 'a -> 'a. But what should the type of r be? It's tempting to say we should infer r : 'a . ('a -> 'a) ref. That would let us instantiate the type of r to be (int -> int) ref on line 4 and store succ in r. But it also would let us instantiate the type of r to be (bool -> bool) ref on line 5. That's a disaster: it causes the application of succ to true, which is not type safe.

The solution adopted by OCaml and related languages is called the value restriction: the type system is designed to prevent a polymorphic mutable value from ever holding more than one type. Let's redo some of that example again, pausing to look at the toplevel output:

# let id = fun x -> x;;
val id : 'a -> 'a = <fun>   (* as expected *)

# let r = ref id;;
val r : ('_weak1 -> '_weak1) ref = { ... }   (* what is _weak? *)

# r;;
- : ('_weak1 -> '_weak1) ref = { ... }   (* it's consistent at least *)

# r := succ;;
- : unit = ()

# r;;
- : (int -> int) ref = { ... }   (* did r just change type ?! *)

When the type of r is inferred, OCaml gives it a type involving a weak type variable. All such variables have a name starting with '_weak. A weak type variable is one that has not been generalized hence cannot be instantiated on multiple types. Rather, it indicates a single type that is not yet known. Think of it as type inference for that variable is not yet finished: OCaml is waiting for more information to pin down precisely what it is. When r := succ is executed, that information finally becomes available. OCaml infers that '_weak1 = int from the type of succ. Then OCaml replaces '_weak1 with int everywhere. That's what yields an error on the final line:

# !r true;;
Error: This expression has type bool but an expression was expected of type int

Since r : (int -> int) ref, we cannot apply !r to a bool.

We won't cover implementation of weak type variables here.

Polymorphism and mutability

Let's not leave this topic of the interaction between polymorphic types and mutability yet. You might be tempted to think that it's a phenomenon that affects only OCaml. But indeed, even Java suffers.

Consider the following class hierarchy:

class Animal { }
class Elephant extends Animal { }
class Rabbit extends Animal { }

Now suppose we create an array of animals:

Animal[] a= new Rabbit[2]

Here we are using subtype polymorphism to assign an array of Rabbit objects to an Animal[] reference. That's not the same as parametric polymorphism as we've been using in OCaml, but it's nonetheless polymorphism.

What if we try this?

a[0]= new Elephant()

Since a is typed as an Animal array, it stands to reason that we could assign an elephant object into it, just as we could assign a rabbit object. And indeed that code is fine according to the Java compiler. But Java gives us a runtime error if we run that code!

Exception java.lang.ArrayStoreException

The problem is that mutating the first array element to be a rabbit would leave us with a Rabbit array in which one element is a Elephant. (Ouch! An elephant would sit on a rabbit. Poor bun bun.) But in Java, the type of every object of an array is supposed to be a property of the array as a whole. Every element of the array created by new Rabbit[2] therefore must be a Rabbit. So Java prevents the assignment above by detecting the error at run time and raising an exception.

This is really the value restriction in another guise! The type of a value stored in a mutable location may not change, according to the value restriction. With arrays, Java implements that with a run-time check, instead of rejecting the program at compile time. This strikes a balance between soundness (preventing errors from happening) and expressivity (allowing more error-free programs to type check).