Chapter 22: Type Reconstruction

---

The typechecking algorithms for the calculi we have seen so far all depend on explicit type annotations-in particular, they require that lambda-abstractions be annotated with their argument types. In this chapter, we develop a more powerful type reconstruction algorithm, capable of calculating a principal type for a term in which some or all of these annotations are left unspecified. Related algorithms lie at the heart of languages like ML and Haskell.

Combining type reconstruction with other language features is often a somewhat delicate matter. In particular, both records and subtyping pose significant challenges. To keep things simple, we consider type reconstruction here only for simple types; §22.8 gives some starting points for further reading on other combinations.

22.1 Type Variables and Substitutions

In some of the calculi in previous chapters, we have assumed that the set of types includes an infinite collection of uninterpreted base types (§11.1). Unlike interpreted base types such as Bool and Nat, these types come with no operations for introducing or eliminating terms; intuitively, they are just placeholders for some particular types whose exact identities we do not care about. In this chapter, we will be asking questions like "if we instantiate the placeholder X in the term t with the concrete type Bool, do we obtain a typable term?" In other words, we will treat our uninterpreted base types as type variables, which can be substituted or instantiated with other types.

For the technical development in this chapter, it is convenient to separate the operation of substituting types for type variables into two parts: describing a mapping σ from type variables to types, called a type substitution, and ^[1]applying this mapping to a particular type T to obtain an instance σT. For example, we might define σ = [X ↦ Bool] and then apply σ to the type X→X to obtain σ(X→X) = Bool→Bool.

22.1.1 Definition

Formally, a type substitution (or just substitution, when it's clear that we're talking about types) is a finite mapping from type variables to types. For example, we write [X ↦ T, Y ↦ U] for the substitution that associates X with T and Y with U. We write dom(σ) for the set of type variables appearing on the left-hand sides of pairs in σ, and range(σ) for the set of types appearing on the right-hand sides. Note that the same variable may occur in both the domain and the range of a substitution. Like term substitutions, the intention in such cases is that all the clauses of the substitution are applied simultaneously; for example, [X ↦ Bool, Y ↦ X→X] maps X to Bool and Y to X→X, not Bool→Bool.

Application of a substitution to a type is defined in the obvious way:

•  

  σ(X)	=
  σ(Nat)	=	Nat
  σ(Bool)	=	Bool
  σ(T1→T2	=	σT1 → σT2

Note that we do not need to make any special provisions to avoid variable capture during type substitution, because there are no constructs in the language of type expressions that bind type variables. (We'll get to these in Chapter 23.)

Type substitution is extended pointwise to contexts by defining

 σ(x1:T1,...,xn:Tn) = (x1:σT1,...,xn:σTn). 

Similarly, a substitution is applied to a term t by applying it to all types appearing in annotations in t.

If σ and γ are substitutions, we write σ ∘ γ for the substitution formed by composing them as follows:

Note that (σ ∘ γ)S = σ(γS).

A crucial property of type substitutions is that they preserve the validity of typing statements: if a term involving variables is well typed, then so are all of its substitution instances.

22.1.2 Theorem [Preservation of Typing Under Type Substitution]

If σ is any type substitution and Г ⊢ t : T, then σГ ⊢ σt : σ T.

Proof: Straightforward induction on typing derivations.

^[1]The system studied in this chapter is the simply typed lambda-calculus (Figure 9-1) with booleans (8-1), numbers (8-2), and an infinite collection of base types (11-1). The corresponding OCaml implementations are recon and fullrecon.

---