In this chapter, we develop the fundamental theory of the Simply Typed Lambda Calculus — in particular, the type safety theorem.

Progress

As before, the progress theorem tells us that closed, well-typed terms are not stuck: either a well-typed term is a value, or it can take an evaluation step. The proof is a relatively straightforward extension of the progress proof we saw in the Types chapter.

Preservation

The other half of the type soundness property is the preservation of types during reduction. For this, we need to develop some technical machinery for reasoning about variables and substitution. Working from top to bottom (the high-level property we are actually interested in to the lowest-level technical lemmas that are needed by various cases of the more interesting proofs), the story goes like this:

• The preservation theorem is proved by induction on a typing derivation, pretty much as we did in the Types chapter. The one case that is significantly different is the one for the ST_AppAbs rule, which is defined using the substitution operation. To see that this step preserves typing, we need to know that the substitution itself does. So we prove a...
• substitution lemma, stating that substituting a (closed) term s for a variable x in a term t preserves the type of t. The proof goes by induction on the form of t and requires looking at all the different cases in the definition of substitition. This time, the tricky cases are the ones for variables and for function abstractions. In both cases, we discover that we need to take a term s that has been shown to be well-typed in some context Γ and consider the same term s in a slightly different context Γ'. For this we prove a...
• context invariance lemma, showing that typing is preserved under "inessential changes" to the context Γ — in particular, changes that do not affect any of the free variables of the term. For this, we need a careful definition of
• the free variables of a term — i.e., the variables occuring in the term that are not in the scope of a function abstraction that binds them.

Free Occurrences

A variable x appears free in a term t if t contains some occurrence of x that is not under an abstraction labeled x. For example:

• y appears free, but x does not, in λx:T→U. x y
• both x and y appear free in (λx:T→U. x y) x
• no variables appear free in λx:T→U. λy:T. x y

A term in which no variables appear free is said to be closed.

Substitution

We first need a technical lemma connecting free variables and typing contexts. If a variable x appears free in a term t, and if we know t is well typed in context Γ, then it must be the case that Γ assigns a type to x.

Next, we'll need the fact that any term t which is well typed in the empty context is closed — that is, it has no free variables.

Sometimes, when we have a proof Γ ⊢ t : T, we will need to replace Γ by a different context Γ'. When is it safe to do this? Intuitively, it must at least be the case that Γ' assigns the same types as Γ to all the variables that appear free in t. In fact, this is the only condition that is needed.

Now we come to the conceptual heart of the proof that reduction preserves types — namely, the observation that substitution preserves types. Formally, the so-called Substitution Lemma says this: suppose we have a term t with a free variable x, and suppose we've been able to assign a type T to t under the assumption that x has some type U. Also, suppose that we have some other term v and that we've shown that v has type U. Then, since v satisfies the assumption we made about x when typing t, we should be able to substitute v for each of the occurrences of x in t and obtain a new term that still has type T. Lemma: If Γ,x:U ⊢ t ∈ T and ⊢ v ∈ U, then Γ ⊢ [x:=v]t ∈ T.

The substitution lemma can be viewed as a kind of "commutation" property. Intuitively, it says that substitution and typing can be done in either order: we can either assign types to the terms t and v separately (under suitable contexts) and then combine them using substitution, or we can substitute first and then assign a type to [x:=v] t — the result is the same either way.

Main Theorem

We now have the tools we need to prove preservation: if a closed term t has type T, and takes an evaluation step to t', then t' is also a closed term with type T. In other words, the small-step evaluation relation preserves types.