9.5 Erasure and Typability

---

9.5 Erasure and Typability

In Figure 9-1, we defined the evaluation relation directly on simply typed terms. Although type annotations play no role in evaluation—we don't do any sort of run-time checking to ensure that functions are applied to arguments of appropriate types—we do carry along these annotations inside of terms as we evaluate them.

Most compilers for full-scale programming languages actually avoid carrying annotations at run time: they are used during typechecking (and during code generation, in more sophisticated compilers), but do not appear in the compiled form of the program. In effect, programs are converted back to an untyped form before they are evaluated. This style of semantics can be formalized using an erasure function mapping simply typed terms into the corresponding untyped terms.

9.5.1 Definition

The erasure of a simply typed term t is defined as follows:

erase(x)	=	x
erase(λx:T1. t2)	=	λx. erase(t2)
erase(t1 t2)	=	erase(t1) erase(t2)

Of course, we expect that the two ways of presenting the semantics of the simply typed calculus actually coincide: it doesn't really matter whether we evaluate a typed term directly, or whether we erase it and evaluate the underlying untyped term. This expectation is formalized by the following theorem, summarized by the slogan "evaluation commutes with erasure" in the sense that these operations can be performed in either order—we reach the same term by evaluating and then erasing as we do by erasing and then evaluating:

9.5.2 Theorem

1. If t → t′ under the typed evaluation relation, then erase(t) → erase(t′).

2. If erase(t) → m′ under the typed evaluation relation, then there is a simply typed term t′ such that t → t′ and erase(t′) = m′.

Proof: Straightforward induction on evaluation derivations.

Since the "compilation" we are considering here is so straightforward, Theorem 9.5.2 is obvious to the point of triviality. For more interesting languages and more interesting compilers, however, it becomes a quite important property: it tells us that a "high-level" semantics, expressed directly in terms of the language that the programmer writes, coincides with an alternative, lower-level evaluation strategy actually used by an implementation of the language.

Another interesting question arising from the erasure function is: Given an untyped lambda-term m, can we find a simply typed term t that erases to m?

9.5.3 Definition

A term m in the untyped lambda-calculus is said to be typable in λ→ if there are some simply typed term t, type T, and context Г such that erase(t) = m and Г ⊢ t : T.

We will return to this point in more detail in Chapter 22, when we consider the closely related topic of type reconstruction for λ→.

---