Type reconstruction

Read TAPL 22.1-6. We’re jumping way ahead in the book, but there’s nothing in these sections that depends on any intervening material (as far as I know).

The goal of this chapter is to develop an algorithm for type reconstruction (or type inference): Given an untyped lambda-term, find the most general (or principal) type.

We could start simply by removing type annotations from the typing rules for the simply-typed lambda calculus:

x:T ∈ Γ
———————                                         (T-Var)
Γ ⊢ x:T

 Γ, x:T1 ⊢ t2 : T2
——————————————————                              (T-Abs')
Γ ⊢ λx.t2 : T1→T2

Γ ⊢ t1 : T11→T12    Γ ⊢ t2 : T11
—————————————————————————————————               (T-App)
        Γ ⊢ t1 t2 : T12

Γ ⊢ t : T→T
—————————————                                   (T-Fix)
Γ ⊢ fix t : T

The problem with these rules is that they are not syntax-directed: Given an untyped term, we used to be able to traverse the syntax tree once and either end up with a type or find that there is no type. Now, the lack of type annotations means that in T-Abs’, we have to guess the type T1. That’s bad news because the set of possible types is infinite.

Constraint-based typing

The solution pursued in the book is to develop a syntax-directed algorithm that assigns every term a type possibly involving type variables, while generating a set of constraints (a system of equations involving the type variables). Then, in a second phase, it tries to solve the system of equations.

The notation in Figure 22-1 is pretty hard to read. I second the suggestion (p. 321) to ignore the subscripts. I’m also going to go ahead and incorporate the implicit type annotation rule from section 22.6. That makes the typing rules look like this:

——————————————  x:T ∈ Γ                          (CT-Var)
Γ ⊢ x : T | {}

 Γ, x:X ⊢ t2 : T2 | C
—————————————————————  X fresh                   (CT-AbsInf)
Γ ⊢ λx.t2 : X→T2 | C

 Γ ⊢ t1 : T1 | C1    Γ ⊢ t2 : T2 | C2
——————————————————————————————————————  X fresh  (CT-App)
Γ ⊢ t1 t2 : X | C1 ∪ C2 ∪ {T1 = T2→X}

       Γ ⊢ t1 : T1 | C
———————————————————————————————  X fresh         (CT-Fix)
Γ ⊢ fix t : X | C ∪ {T1 = X→X}

The side condition X fresh means that X is different from the type variables introduced anywhere else in the derivation. It’s a bit of informality that is actually perfectly safe when you implement the algorithm (Exercise 22.3.9, and below).

Here’s a example typing derivation for λf. f 0:

―――――――――――――――――― (CT-Var)  ――――――――――――――――――― (CT-Zero)
f:X1 ⊢ f : X1 | {}           f:X1 ⊢ 0 : Nat | {}
―――――――――――――――――――――――――――――――――――――――――――――――― (CT-App)
       f:X1 ⊢ f 0 : X2 | {X1 = Nat→X2}
     ――――――――――――――――――――――――――――――――――― (CT-AbsInf)
     ⊢ λf. f 0 : X1→X2 | {X1 = Nat→X2}

Implementing the algorithm

Here’s a pseudocode implementation of the typing algorithm.

function typecheck_helper(t, Γ)
    if t = x
        return Γ(x), {}
    else if t = λx.t2
        X = fresh()
        T2, C = typecheck_helper(t2, Γ ∪ {x:X})
        return X→T2, C
    else if t = t1 t2
        T1, C1 = typecheck_helper(t1, Γ)
        T2, C2 = typecheck_helper(t2, Γ)
        X = fresh()
        return X, C1 ∪ C2 ∪ {T1 = T2→X}
    else if t = fix t1
        T1, C1 = typecheck_helper(t1, Γ)
        X = fresh()
        return X, C1 ∪ {T1 = X→X}
        

The function fresh() returns a new type variable that has never been used before.

The unification algorithm in Figure 22-2 might also be easier to read as imperative pseudocode:

function unify(T0, C)
    while C is not empty
        pop a constraint S=T from C
        if S = T
            do nothing
        else if S = X and X ∉ FV(T)
            T0 = [X↦T]T0
            C = [X↦T]C
        else if T = X and X ∉ FV(S)
            T0 = [X↦S]T0
            C = [X↦S]C
        else if S = S1→S2 and T = T1→T2
            C = C ∪ {S1=T1, S2=T2}
        else
            fail
    return T0

Then the top-level reconstruction function is:

function typecheck(t)
    T, C = typecheck_helper(t, {})
    return unify(T, C)

The operations T0 = [X↦T]T0 and the like are expensive and can be made more efficient if we don’t actually perform these substitutions, but maintain a table that says what each type variable stands for, e.g.,

Type variable	Stands for
X1	Nat→X2
X2	X3
X3	X4

This can be thought of as a union-find data structure, where each set has one or more type variables and at most one type that isn’t a type variable. This data structure can be implemented so that querying and updating are almost linear time.