for the two to live in the same universe. If the types were not supplied until execution, the type checker not
be able to detect errors until program execution time, thereby defeating the most important benefit that types
confer.
It is therefore clear that the type procedures must accept arguments and evaluate their bodies before the
type checker even begins execution. By that time, if all the type applications are over, it suffices to use the
type checker built earlier, since what remains is a language with no type variables remaining. We call the
phase that performs these type applications the type elaborator.
The problem with any static procedure applications is to ensure they will lead to terminating processes!
If they don’t, we can’t even begin the next phase, which is traditional type checking. In the case of using
length, the first application (from the procedure use) is on the type num. This in turn inspires a recursive
invocation of length also on type num. Because this latter procedure application is no different from the
initial invocation, the type expander does not need to perform the application. (Remember, if the language
has no side-effects, computations will return the same result every time. Type application has no side-
effects.)
This informal argument suggests that only one pass over the body is necessary. We can formalize this
with the following type judgments:
Γ e : ∀α .τ
Γ e < τ >: τ [α ←τ ]
This judgment says that on encountering a type application, we substitute the quantified type with the type
argument replacing the type variable. The program source contains only a fixed number of type applications
(even if each of these can execute arbitrarily many times), so the type checker performs this application only
once. The corresponding rule for a type abstraction is
Γ[α ] e : τ
Γ
< Λ (α) e >: ∀α.τ
This says that we extend Γ with a binding for the type variable α, but leave the associated type unspecified
so it is chosen nondeterministically. If the choice of type actually matters, then the program must not type-
check.
Observe that the type expander conceptually creates many monomorphically typed procedures, but we
don’t really want most of them during execution. Having checked types, it’s fine if the length function that
29.5. PERSPECTIVE
271
actually runs is essentially the same as Scheme’s length. This is in fact what most evaluators do. The static
type system ensures that the program does not violate types, so the program that runs doesn’t need type
checks.
29.5
Perspective
Explicit polymorphism seems extremely unwieldy: why would anyone want to program with it? There
are two possible reasons. The first is that it’s the only mechanism that the language designer gives for
introducing parameterized types, which aid in code reuse. The second is that the language includes some
additional machinery so you don’t have to write all the types every time. In fact, C++ introduces a little of
both (though much more of the former), so programmers are, in effect, manually programming with explicit
polymorphism virtually every time they use the STL (Standard Template Library). Similarly, the Java 1.5 and
C# languages support explicit polymorphism. But we can possibly also do better than foist this notational
overhead on the programmer.
272
CHAPTER 29. EXPLICIT POLYMORPHISM
Chapter 30
Type Inference
30.1
Inferring Types
We’ve seen the value of having explicit polymorphism in our language—it lets us write programs that work
on may different types of values. Even mainstream languages like C++ and, more recently, Java have recog-
nized the value of this form of parameteric polymorphism, and they have noticed that it complements and is
not subsumed by the polymorphism common to object-oriented languages (called subtype polymorphism).
Despite its benefits, it’s very unwieldy to use explicit parametric polymorphism to write programs such
as this:
(define length
<Λ (τ)
(lambda (l : list(τ)) : number
(cond
[(Empty?<τ> l) 0]
[(Cons?<τ> l) (add1 (length<τ> (Rest<τ> l)))]))>)
when we could instead write
(define length
(lambda (l)
(cond
[(empty? l) 0]
[(cons? l) (add1 (length (rest l)))])))
As computer scientists, we should ask: Is it possible for a programming environment to convert the latter
into the former? That is, can the environment automatically fill in the types necessary for the former? This
would be the best of both worlds, because the programmer would avoid the trouble of the typing while still
getting the benefit of the typing.
While this would be nice, it also seems nearly magical. It seems hard enough for humans to get this
right; can a program (the environment) do better? Still, we should not despair too much. We’ve already seen
several instances such as closure creation, garbage collection, and so on, where the language implementation
273
274
CHAPTER 30. TYPE INFERENCE
was able to do a more accurate job than a human could have done, thereby providing a valuable feature while
reducing the programmer’s burden. Maybe inserting type annotations could be another of those tasks.
Because this is obviously challenging, let’s try to make the problem easier. Let’s ignore the polymor-
phism, and just focus on generating types for monomorphic programs (i.e., those that don’t employ poly-
morphism). In fact, just to make life really simple, let’s just consider a program that operates over numbers,
such as factorial.
30.1.1
Example: Factorial
Suppose we’re given the following program:
(define fact
(lambda (n)
(cond
[(zero? n) 1]
[true
(∗ n (fact (sub1 n)))])))
We’ve purposely written true instead of else for reasons we’ll soon see. It should be clear that using true
doesn’t affect the meaning of the program (in general, else is just a more readable way of writing true).
If we were asked to determine the type of this function and had never seen it before, our reasoning might
proceed roughly along these lines. First, we would name each expression:
(define fact
1 (lambda (n)
2 (cond
[ 3 (zero? n) 4 1]
[ 5 true
6 (∗ n 7 (fact 8 (sub1 n)))])))
We would now reason as follows. We’ll use the notation [ · ] to mean the type of the expression within the
brackets.
• The type of the expression labeled 1 1 is clearly a function type (since the expression is a lambda).
The function’s argument type is that of n, and it computes a value with the type of 2 . In other words,
[ 1 ] = [ n] →[ 2 ]
• Because 2 is a conditional, we want to ensure the following:
– The first and second conditional expressions evaluate to boolean values. That is, we would like
the following to hold:
[ 3 ] = boolean
[ 5 ] = boolean
1We’ll need to use this phrase repeatedly, and it’s quite a mouthful. Therefore, we will henceforth say “the type of n ” when
we mean “the type of the expression labeled by n ”.
30.1. INFERRING TYPES
275
– We would like both branches of the conditional to evaluate to a value of the same type, so we
can assign a meaningful type to the entire conditional expression:
[ 2 ] = [ 4 ] = [ 6 ]
• What is the type of 3 ? We have a constraint on what it can be:
[ zero?] = [ n] →[ 3 ]
Because we know the type of zero?, we know that the right-hand-side of the above equality must be:
[ n] →[ 3 ] = number→boolean
which immediately tells us that [ n] = number.
The first response in the cond tells us that [ 4 ] = number, which immediately resolves the type of 2 and
determines the type of 1 in atomic terms. That is, the type of fact must be number → number. However,
it’s worthwhile to continue with this process as an illustration:
• We have a constraint on the type of 6 : it must be the same as the result type of multiplication.
Concretely,
[ n] × [ 7 ] →[ 6 ] = number × number→number
• The type of 7 must be whatever fact returns, while 8 must be the type that fact consumes:
[ 1 ] = [ 8 ] →[ 7 ]
• Finally, the type of 8 must be the return type of sub1:
[ sub1] = [ n] →[ 8 ] = number→number
30.1.2
Example: Numeric-List Length
Now let’s look at a second example:
(define nlength
(lambda (l)
(cond
[(nempty? l) 0]
[(ncons? l) (add1 (nlength (nrest l)))])))
First, we annotate it:
(define nlength
1 (lambda (l)
2 (cond
[ 3 (nempty? l) 4 0]
[ 5 (ncons? l) 6 (add1 7 (nlength 8 (nrest l)))])))
276
CHAPTER 30. TYPE INFERENCE
We can begin by deriving the following constraints:
[ 1 ] = [ l] →[ 2 ]
[ 2 ] = [ 4 ] = [ 6 ]
[ 3 ] = [ 5 ] = boolean
Because 3 and 5 are each applications, we derive some constraints from them:
[ nempty?] = [ l] →[ 3 ] = numlist→boolean
[ ncons?] = [ l] →[ 5 ] = numlist→boolean
The first conditional’s response is not very interesting:2
[ 4 ] = [ 0] = number
Finally, we get to the second conditional’s response, which yields several constraints:
[ add1] = [ 7 ] →[ 6 ] = number→number
[ 1 ] = [ 8 ] →[ 7 ]
[ nrest] = [ l] →[ 8 ] = numlist→numlist
Notice that in the first and third set of constraints above, because the program applies a primitive, we can
generate an extra constraint which is the type of the primitive itself. In the second set, because the function
is user-defined, we cannot generate any other meaningful constraint just by looking at that one expression.
Solving all these constraints, it’s easy to see both that the constraints are compatible with one another,
and that each expression receives a monomorphic type. In particular, the type of 1 is numlist → number,
which is therefore the type of nlength also (and proves to be compatible with the use of nlength in expression
7 ).
30.2
Formalizing Constraint Generation
What we’ve done so far is extremely informal. Let’s formalize it.
Constraints relate different portions of the program by determining how they should be compatible
for the program to execute without error. Consequently, a single program point may result in multiple
constraints. Each set of constraints represents a “wish list” about that particular point in the program.
Consequently, a program may lead to contradictory constraints; hopefully we will be able to find these later.
One slightly confusing aspect of constraints is that we write them to look like equations, but they reflect
2Note that the 0 inside the [ · ] is an expression itself, not a number labeling an expression.
30.3. ERRORS
277
what we hope will be true, not what we know is true. Specifically, they represent what suffices for safe
program execution.3
For each expression n in the program’s abstract syntax tree, we introduce a variable of the form [ n] .
That is, if the program has the form (foo 1 2), we would want to introduce variables for 1, 2 and (foo 1 2).
Because abstract syntax tree nodes are unwieldy to write down explicitly, we will associate the node with
the expression at that node. We use [ · ] to represent the type of a node, so the types of the expressions in
the example above would be [ 1] , [ 2] and [ (foo 1 2)] .
Each expression type generates different constraints. We present below a table that relates the type of
expression at a node to the (set of) constraints generated for that node. Remember to always read [ · ] as
“the type of the expression” (within the brackets):
Expression at Node
Generated Constraints
n, where n is a numeral
[ n] = number
true
[ true] =boolean
false
[ false] =boolean
(add1 e)
[ (add1 e)] =number
[ e] =number
(+ e1 e2)
[ (+ e1 e2)] =number
[ e1] = number
[ e2] = number
(zero? e)
[ (zero? e)] =boolean
[ e] = number
(ncons e1 e2)
[ (ncons e1 e2)] =list(num)
[ e1] = number
[ e2] = list(num)
(nfirst e)
[ (nfirst e)] =number
[ e] = list(num)
(nrest e)
[ (nrest e)] =list(num)
[ e] = list(num)
(nempty? e)
[ (nempty? e)] =boolean
[ e] = list(num)
nempty
[ nempty] =list(num)
(if c t e)
[ (if c t e)] =[ t]
[ (if c t e)] =[ e]
[ c] =boolean
(lambda (x) b)
[ (lambda (x) b)] = [ x] →[ b]
(f a)
[ f ] = [ a] →[ (f a)]
Notice that in the two prior examples, we did not create new node numbers for those expressions that
consisted of just a program identifier; correspondingly, we have not given a rule for identifiers. We could
have done this, for consistency, but it would have just created more (unnecessary) variables.
Exercise 30.2.1 What is the complexity of constraint generation?
Exercise 30.2.2 Using the expression at the node, rather than the node itself, introduces a subtle ambiguity.
Do you see why?
30.3
Errors
Here’s an erroneous program:
3We use the term “suffices” advisedly: these constraints are sufficient but not necessary. They may reject some programs that
might have run without error had the type system not intervened. This is inherent in the desire to statically approximate dynamic
behavior: the Halting Problem is an insurmountable obstacle. An important constraint on good type system design is to maximize
the set of legal problems while still not permitting errors: balancing programmer liberty with execution safety.
278
CHAPTER 30. TYPE INFERENCE
(define nlsum
(lambda (l)
(cond
[(nempty? l) 0]
[(ncons? l) (+ (nrest l)
(nlsum (nrest l)))])))
Can you spot the problem?
First, we’ll annotate the sub-expressions:
(define nlsum
1 (lambda (l)
2 (cond
[ 3 (nempty? l) 4 0]
[ 5 (ncons? l) 6 (+ 7 (nrest l)
8 (nlsum 9 (nrest l)))])))
Generating constraints as usual, we get the following (amongst others):
[ 8 ] = number
because the function returns a number in both branches of the conditional, and
[ 9 ] = numlist
from the type of nrest. Consequently, it appears we can infer that the value bound to nlsum has the type
numlist → number. This is indeed the type we expect for this procedure.
We should not, however, annotate any types before we’re generated, examined and resolved all the
constraints: we must make sure there are no inconsistencies. Completing the generation and solution process
does, in fact, result in an inconsistency for this program. In particular, we have
[ 7 ] = numlist
from the type of nrest, while
[ 7 ] = number
from the type of +. Indeed, the latter is the type we want: the numlist only materializes because of the faulty
use of nrest. Had the programmer used nfirst instead of nrest in the left-hand-side argument to the addition,
the entire program would have checked correctly. Instead, the type inference engine must recognize that
there is an error resulting from a type conflict: the expression (nrest l) is expected to have both the type
number and the type numlist. Because these are not compatible types, the type “checker” must present the
user with this error.
We use quotes around “checker” because it has, in some sense, disappeared. Instead of checking types
annotated by the programmer, the type system now tries to fill in the programmer’s annotations. If it suc-
ceeds, it can do so only by respecting the types of operations, so there is no checking left to be done. Failure
to annotate the program completely and unambiguously is now the indication of a type error.
30.4. EXAMPLE: USING FIRST-CLASS FUNCTIONS
279
30.4
Example: Using First-Class Functions
We will consider one final example of constraint generation, to show that the process scales in the presence
of functions as arguments. Consider the following program:
(define nmap
1 (lambda (f l)
2 (cond
[ 3 (nempty? l) 4 nempty]
[ 5 (ncons? l) 6 (ncons 7 (f 8 (nfirst l))
9 (nmap f 10 (nrest l)))])))
This program generates the following constraints:
[ 1 ] = [ f ] × [ l] →[ 2 ]
We get the usual constraints about boolean conditional tests and the type equality of the branches (both must
be of type numlist due to the first response). From the second response, we derive
[ ncons] = [ 7 ] × [ 9 ] →[ 6 ] = number × numlist→numlist
The most interesting constraint is this one:
[ f ] = [ 8 ] →[ 7 ]
In other words, we don’t need a sophisticated extension to handle first-class functions: the constraint gener-
ation phase we described before suffices.
Continuing, we obtain the following three constraints also:
[ nfirst] = [ l] →[ 8 ] = numlist→number
[ nmap] = [ f ] × [ 10 ] →[ 9 ]
[ nrest] = [ l] →[ 10 ] = numlist→numlist
Since l is of type numlist, we can substitute and solve to learn that f has type number → number. Conse-
qently, nmap has type
(number → number) × numlist → numlist
which is the type we would desire and expect!
280
CHAPTER 30. TYPE INFERENCE
30.5
Solving Type Constraints
30.5.1
The Unification Algorithm
To solve type constraints, we turn to a classic algorithm: unification. Unification consumes a set of con-
straints and either
• identifies inconsistencies amongst the constraints, or
• generates a substitution that represents the solution of the constraints.
A substitution associates each identifier (for which we are trying to solve) with a constant or another iden-
tifier. Our identifiers represent the types of expressions (thus 4 is a funny notation for an identifier that
represents the type of the expression labeled 4). In our universe, inconsistencies indicate type errors, and
the constants are terms in the type language (such as number and number → boolean).
The unification algorithm is extremely simple. Begin with an empty substitution. Push all the constraints
onto a stack. If the stack is empty, return the substitution; otherwise, pop the constraint X = Y off the stack:
1. If X and Y are identical identifiers, do nothing.
2. If X is an identifier, replace all occurrences of X by Y both on the stack and in the substitution, and
add X → Y to the substitution.
3. If Y is an identifier, replace all occurrences of Y by X both on the stack and in the substitution, and
add Y → X to the substitution.
4. If X is of the form C(X1, . . . , Xn) for some constructor C,4 and Y is of the form C(Y1, . . . ,Yn) (i.e., it has the same constructor), then push Xi = Yi for all 1 ≤ i ≤ n onto the stack.
5. Otherwise, X and Y do not unify. Report an error.
Does this this algorithm terminate? On every iteration of the main loop, it pops a constraint off the stack. In
some cases, however, we push new constraints on. The size of each of these constraints is, however, smaller
than the constraint just popped. Therefore, the total number of iterations cannot be greater than the sum of
the sizes of the initial constraint set. The stack must therefore eventually become empty.
Exercise 30.5.1 What are the space and time complexity of this algorithm?
30.5.2
Example of Unification at Work
Let’s consider the following example:
1 ( 2 (lambda (x) x)
3 7)
4In our type language, the type constructors are → and the base types (which are constructors of arity zero). More on this in
Section 30.5.3.
30.5. SOLVING TYPE CONSTRAINTS
281
This generates the following constraints:
[ 2 ] = [ 3 ] →[ 1 ]
[ 2 ] = [ x] →[ x]
[ 3 ] = number
The unification algorithm works as follows:
Action
Stack
Substitution
Initialize
[ 2 ] = [ 3 ] →[ 1 ]
empty
[ 2 ] = [ x] →[ x]
[ 3 ] = number
Step 2
[ 3 ] →[ 1 ] = [ x] →[ x]
[ 2 ] → [ 3 ] →[ 1 ]
[ 3 ] = number
Step 4
[ 3 ] = [ x]
[ 2 ] → [ 3 ] →[ 1 ]
[ 1 ] = [ x]
[ 3 ] = number
Step 2
[ 1 ] = [ x]
[ 2 ] → [ x] →[ 1 ]
[ x] = number
[ 3 ] → [ x]
Step 2
[ x] = number
[ 2 ] → [ x] →[ x]
[ 3 ] → [ x]
[ 1 ] → [ x]
Step 2
empty
[ 2 ] → number→number
[ 3 ] → number
[ 1 ] → number
[ x] → number
At this point, we have solutions for all the sub-expressions and we know that the constraint set is consistent.
Writing these in detail is painstaking, but it’s usually easy to simulate this algorithm on paper by just
crossing out old values when performing a substitution. Be sure to work through our examples for more
practice with unification!
30.5.3
Parameterized Types
In the presentation of unification above, we saw only one type constructor with positive arity: →. A regular
programming language will typically have many more constuctors. A common source of parameterized
types is containers: lists, trees, queues, stacks, and so forth. For instance, it is common to think of lists
as parameterized over their content, thus yielding list(number), list(symbol), list(list(number)), list(number
→ symbol) and so on. Identifying list as one of the type constructors for the unification algorithm suffices
for typing unityped lists.
282
CHAPTER 30. TYPE INFERENCE
30.5.4
The “Occurs” Check
Suppose we generate the following type constraint:
list([ x] ) = list(list([ x] ))
By Step 4, we should push [ x] = list([ x] ) onto the stack. Eventually, obeying to Step 2, we will add the
mapping [ x] → list([ x] ) to the substition but, in the process, attempt to replace all instances of [ x] in the
substitution with the right-hand side, which does not terminate.
This is a familiar problem: we saw it earlier when trying to define substitution in the presence of recur-
sion. Because these are problematic to handle, a traditional unification algorithm checks in Steps 2 and 3
whether the identifier about to be (re)bound in the substitution occurs in the term that will take its place. If
the identifier does occur, the unifier halts with an error.5 Otherwise, the algorithm proceeds as before.
Exercise 30.5.2 Write a program that will generate the above constraint!
30.6
Underconstrained Systems
We have seen earlier that if the system has too many competing constraints—for instance, forcing an iden-
tifier to have both type number and boolean—there can be no satisfying type assignment, so the system
should halt with an error. We saw this informally earlier; Step 5 of the unification algorithm confirms that
the implementation matches this informal behavior.
But what if the system is under-constrained? This is interesting, because some of the program identifiers
never get assigned a type! In a procedure such as map, for instance:
(define (map f l)
(cond
[(empty? l) empty]
[(cons? l) (cons (f (first l))
(map f (rest l)))]))
This is an instructive example. Solving the constraints reveals that there is no constraint on the type passed
as a parameter to the list type constructor. Working through the steps, we get a type for map of this form:
(α→β )