Fifty Cent Lecture on the Unification-Based Type Inference Algorithm

In December 1978 the Journal of Computer and System Sciences published "A Theory of Type Polymorphism in Programming." In 1992 I was introduced to Standard ML in compilers class, and used it to write a typechecker for our Ada subset compiler. I was in love with types, typecheckers, and type inference. In 1993 my good friend and I tried unsuccessfully to implement type inference as part of a much larger project, without actually researching the prior art. We needed to learn the fine art of finding and reading research papers. A few years later I was back in grad school, and got the help I needed to locate the right papers and understand them enough to implement an inferencing type checker. The paper for that project is dated December 8, 1997. I'm very satisfied that ten years later, type inference has not gone by the wayside but is poised to go mainstream, going the way of automatic memory management (GC) via Java.

In commemoration then, let's explore a bit this fascinating feature that may soon be coming to a programming language near you.

Cocktail Party Explanation (Type Inference in 30 Seconds)

The way most bloggers are explaining type inference lately is with a Java/C# assignment example. Instead of typing

WaitingPageHandler handler = new WaitingPageHandler(args);

which has this offendingly redundant "X x = new X" form, you can get away with something like

var handler = new WaitingPageHandler(args);

How does the typechecker figure this out? This doesn't look too hard to infer. What about an even simpler form:

var delay = 250;

Obviously, the literal 250 is an int, and so is delay. The type of literals like 250, 3.14159, -1L or "duck" are well-defined by the language. An expression involving the new operator is that of new's argument. Here we see the easiest part of understanding type inference -- that there are some expression tree leaves that can be immediately inferred.

Of course you don't just write assignments. As you know from studying lambda calculus, there are three fundamental operations to care about: lambda introduction (corresponding to introducing literals), variable reference, and function application. So how does type inference handle variable reference and function application?

Checking Variable References with Known Type

Let's tackle variable reference first. What if we were given this:

var timeout = 500;
var timeoutTime = System.currentTimeMillis() + timeout;

In the second line, what type does timeout have? It's an int, but how does the typechecker know it? It was inferred from the first line, you're right. But technically, the typechecker probably doesn't know or care that it was inferred. After the typechecker inferred the type of the timeout in the first line, it updated the environment so that in subsequent processing timeout's actual type is known. The typechecker did a lookup in the environment for the type of timeout before doing anything else, as it would in an ordinary static typing typechecker.

So we come to the clue that as with ordinary static typechecking, an environment is needed. The environment is a stack of identifier to type bindings. Environments will come very much into play as we develop the algorithm.

We have looked at how variable reference works when the type is known. There is another possibility, that the type of the variable being referenced is unknown, but first let's look at function application when the function's type is known.

Checking Function Application with Known Type

What about this simple line:

var delay = 15 * 60;

Given two ints, * returns an int, making int the type of the function application expression *(15,60), and thus the type of the variable delay. More generally, when we see a function call and the type of the function is known, the type of the expression is that of the function's return type.

Inferring a Type

The interesting part of type inference comes when a variable is referenced but not immediately inferred. A good example of this situation is when the variable is the argument to a function:

function(x)
{
 print(x);
 if(x < 2)
   1
 else
   x*factorial(x-1)
}

This puts us into a little deeper water. But stay with me, because this is it; the heart of basic type inference using unification. First, notice that the type of x is obviously int from the comparison in the if test, and also from the expression x-1 which is similar to the 15*60 example above. The fun comes in how we can process this line by line and arrive at the right conclusions. The print(x) line is a function call where x's type is as yet unknown. We assume that like in most languages print is overloaded for all types, or at least all the basic ones like int and String. By the time the typechecker is done, we do need to know x's type so our code generator or interpreter has enough information to call the right print code. How?

When we encounter a reference to a variable with unknown type, we tag its type with a unique type variable. Wuzzat? Hello? you say. Yes, we will need a separate environment that tracks type variables. For example, we will say that x's type is that of type variable t1, and in our type environment we say that t1 is bound to an unknown type -- the variable is kept in symbolic form, it's unbound. That's all we can and need to do for the print(x) line, so we move on.

When we encounter the next line, the if expression, we will type check its three arguments: the test expression, the "if true" expression, and the "if false" or "else" expression. So far we haven't mentioned unification, but here's where it really becomes necessary. What we actually do to typecheck the x < 2 expression is run the unification algorithm. The types of the arguments to the less-than operator (which you should always remember to properly escape in your blog editor if you don't want to mysteriously lose portions of your text) are unified with their expected types. For example, we know the less-than operator takes two numeric operands. We'll skip over the overload resolution part here and assume that the literal 2 tells us we're using the int version of the less-than operator. So we know that this operator is a function which takes two ints. We unify the type of the first argument's expression x with the type of the function's first argument, which we just said is int:

Unify(t1,int)

In this case the unification algorithm is getting a type variable and a concrete type, indicating we've discovered what type the variable should be bound to. So at this point we can update t1 in the type environment:

t1 = int

That's it! That's perhaps the key part of the unification-based type inference algorithm.

From this point on, whenever we lookup the type of x in the environment, we'll still be referred to the type variable t1, but when we ask the type environment to evaluate that type expression, we'll get a concrete type of int. We can construct our typechecker to have two passes, one that runs this algorithm and guarantees the type environment has nothing but known types afterwards, and then a subsequent pass that updates the environment to concrete types.

Also, note an assumption in the algorithm: once we had any concrete type for x we used it. If later in your program x was used in a context of a different concrete type, the typechecker would flag a type error. This is where you get errors like "found a real when expecting an int".

Equivalent But Still Unknown Types

Another key part of unification comes when a variable of unknown type is unified with another variable of unknown type. For example:

function(x,y)
{
  z = if(choose()) x else y;
  2^z
}

In this case the first line of the function tells us only that x, y and z are the same type. This is important information that must not be lost. Let's step through these expressions. In the first line, we check the if/else expression. We assume the type of choose() is known to be boolean-valued to match the expected type of an if test expression (and if the return type of choose wasn't known, it would be inferred by its use here). We then check the two branches of the if, and since they simple variable references we generate a unique type variable for each and bind the variable reference appropriately. In other words:

In the type environment,
t1 -> unknown
t2 -> unknown
In the user variable environment,
x -> t1
y -> t2

This is the state of things after checking both expressions. The last part of checking the if/else is to unify those two expressions, since we know they must match. In other words,

Unify(t1, t2)

is evaluated. We saw what happens when unifying a type variable and a concrete type; we assign the type variable to the type. But here both are variables. In this case, unification says we simply remember the equivalence of these unknown type variables. The way I handled this was to augment the type environment to keep a list of known equivalences for a type variable:

In the type environment,
t1 -> equivalences[t2]
t2 -> equivalences[t1]

If we ever find a concrete binding for t2 we can bind t1 as well as t2 at that time. And that should explain the rest of the example.

When we evaluate the assignment statement z = if, we enter a similar type variable entry for z and make it equivalent to both t1 and t2:

In the type environment,
t1 -> equivalences[t2,t3]
t2 -> equivalences[t1,t3]
t3 -> equivalences[t1,t2]

The way you handle this equivalence list is an implementation choice but I hope you get the idea.

When we finally hit the function's final expression 2^z we again have an overloaded operator but the presence of 2 helps us resolve it to the integer power operator, so we can unify the type of z with int, letting us simultaneously bind the type variables t1, t2 and t3 since we know their equivalence.

Where Polymorphic Variables Come From

Sometimes when checking a function the parameter may never be used in a context specific enough to bind its type. What happens then? For example:

function(x)
{
  (x, [])
}

This takes an argument and returns a pair of the original argument x and an empty list, possibly a normalizing step for a function that will visit x and accumulate some results seeded with the empty list. The pair construction works for values of any type, so it adds no information that can be used to deduce a particular type for x. When the typechecker gets to the end of the function declaration, x is found to still be bound to its type variable. When this happens, x is "promoted" to be a polymorphic-typed variable. In order words, since x is not used in any particular way, it can be used for any type. A language designer could choose not to support polymorphic types for some reason, and could flag this as an error.

This example also introduces the notion that type inference operates within a certain boundary. There has to be a point in the abstract syntax tree where the typechecker knows this is where to promote still-symbolic types to be polymorphic. In Standard ML, I believe this boundary is the named function definition introduced by the fun keyword.

Conclusion

The complete algorithm is a little more involved than I've described here, but I hope this helps you understand the essential pieces and the general flow. For more details please see "Principal type-schemes for functional programs" by Luis Damas and Robin Milner (ACM 1982) or the original "A Theory of Type Polymorphism in Programming" by Robin Milner (Journal of Computer and System Sciences, Vol.17, No.3, December 1978, pp.348-375), particularly section 4 "A Well-Typing Algorithm and Its Correctness."