9.3 Properties of Typing

< Free Open Study >

As in Chapter 8, we need to develop a few basic lemmas before we can prove type safety. Most of these are similar to what we saw before-we just need to add contexts to the typing relation and add clauses to each proof for λ-abstractions, applications, and variables. The only significant new requirement is a substitution lemma for the typing relation (Lemma 9.3.8).

First off, an inversion lemma records a collection of observations about how typing derivations are built: the clause for each syntactic form tells us "if a term of this form is well typed, then its subterms must have types of these forms..."

9.3.1 Lemma [Inversion of the Typing Relation]

If Г ⊢ x : R, then x:R Î Г.
If Г ⊢ λx:T₁. t₂ : R, then R = T₁→R₂ for some R₂ with Г, x:T₁⊢ t₂ : R₂.
If Г ⊢ t₁ t₂ : R, then there is some type T₁₁ such that Г ⊢ t₁ : T₁₁→R and Г ⊢ t₂ : T₁₁.
If Г ⊢ true : R, then R = Bool.
If Г ⊢ false : R, then R = Bool.
If Г ⊢ if t₁ then t₂ else t₃ : R, then Г ⊢ t₁ : Bool and Г ⊢ t₂, t₃ : R.

Proof: Immediate from the definition of the typing relation.

9.3.2 Exercise [Recommended, ⋆⋆⋆]

Is there any context Г and type T such that Г ⊢ x x : T? If so, give Г and T and show a typing derivation for Г ⊢ x x : T; if not, prove it.

In §9.2, we chose an explicitly typed presentation of the calculus to simplify the job of typechecking. This involved adding type annotations to bound variables in function abstractions, but nowhere else. In what sense is this "enough"? One answer is provided by the "uniqueness of types" theorem, which tells us that well-typed terms are in one-to-one correspondence with their typing derivations: the typing derivation can be recovered uniquely from the term (and, of course, vice versa). In fact, the correspondence is so straight-forward that, in a sense, there is little difference between the term and the derivation.

9.3.3 Theorem [Uniqueness of Types]

In a given typing context Г, a term t (with free variables all in the domain of Г) has at most one type. That is, if a term is typable, then its type is unique. Moreover, there is just one derivation of this typing built from the inference rules that generate the typing relation.

Proof: Exercise. The proof is actually so direct that there is almost nothing to say; but writing out some of the details is good practice in "setting up" proofs about the typing relation.

For many of the type systems that we will see later in the book, this simple correspondence between terms and derivations will not hold: a single term will be assigned many types, and each of these will be justified by many typing derivations. In these systems, there will often be significant work involved in showing that typing derivations can be recovered effectively from terms.

Next, a canonical forms lemma tells us the possible shapes of values of various types.

9.3.4 Lemma [Canonical Forms]

If v is a value of type Bool, then v is either true or false.
If v is a value of type T₁→T₂, then v = λx:T₁.t₂.

Proof: Straightforward. (Similar to the proof of the canonical forms lemma for arithmetic expressions, 8.3.1.)

Using the canonical forms lemma, we can prove a progress theorem analogous to Theorem 8.3.2. The statement of the theorem needs one small change: we are interested only in closed terms, with no free variables. For open terms, the progress theorem actually fails: a term like f true is a normal form, but not a value. However, this failure does not represent a defect in the language, since complete programs-which are the terms we actually care about evaluating-are always closed.

9.3.5 Theorem [Progress]

Suppose t is a closed, well-typed term (that is, ⊢ t : T for some T). Then either t is a value or else there is some t′ with t → t′.

Proof: Straightforward induction on typing derivations. The cases for boolean constants and conditions are exactly the same as in the proof of progress for typed arithmetic expressions (8.3.2). The variable case cannot occur (because t is closed). The abstraction case is immediate, since abstractions are values.

The only interesting case is the one for application, where t = t₁ t₂ with ⊢ t₁ : T₁₁→T₁₂ and ⊢ t₂ : T₁₁. By the induction hypothesis, either t₁ is a value or else it can make a step of evaluation, and likewise t₂. If t₁ can take a step, then rule E-APP1 applies to t. If t₁ is a value and t₂ can take a step, then rule E-APP2 applies. Finally, if both t₁ and t₂ are values, then the canonical forms lemma tells us that t₁ has the form λx:T₁₁.t₁₂, and so rule E-APPABS applies to t.

Our next job is to prove that evaluation preserves types. We begin by stating a couple of "structural lemmas" for the typing relation. These are not particularly interesting in themselves, but will permit us to perform some useful manipulations of typing derivations in later proofs.

The first structural lemma tells us that we may permute the elements of a context, as convenient, without changing the set of typing statements that can be derived under it. Recall (from page 101) that all the bindings in a context must have distinct names, and that, whenever we add a binding to a context, we tacitly assume that the bound name is different from all the names already bound (using Convention 5.3.4 to rename the new one if needed).

9.3.6 Lemma [Permutation]

If Г ⊢ t : T and Δ is a permutation of Г, then Δ ⊢ t : T. Moreover, the latter derivation has the same depth as the former.

Proof: Straightforward induction on typing derivations.

9.3.7 Lemma [Weakening]

If Г ⊢ t : T and x ∉ dom(Г), then Г, x:S ⊢ t : T. Moreover, the latter derivation has the same depth as the former.

Proof: Straightforward induction on typing derivations.

Using these technical lemmas, we can prove a crucial property of the typing relation: that well-typedness is preserved when variables are substituted with terms of appropriate types. Similar lemmas play such a ubiquitous role in the safety proofs of programming languages that it is often called just "the substitution lemma."

9.3.8 Lemma [Preservation of Types Under Substitution]

If Г, x:S ⊢ t : T and Г ⊢ s : S, then Г ⊢ [x ↦ s]t : T.

Proof: By induction on a derivation of the statement Г, x:S ⊢ t : T. For a given derivation, we proceed by cases on the final typing rule used in the proof.^[3] The most interesting cases are the ones for variables and abstractions.

Case T-VAR:

t = z

with z:T Î (Г, x:S)

There are two sub-cases to consider, depending on whether z is x or another variable. If z = x, then [x ↦ s]z = s. The required result is then Г ⊢ s : S, which is among the assumptions of the lemma. Otherwise, [x ↦ s]z = z, and the desired result is immediate.

Case T-ABS:

 t = λy:T₂.t₁ T = T₂→T₁ Г, x:S, y:T₂ ⊢ t₁ : T₁

By convention 5.3.4, we may assume x ≠ y and y Г FV(s). Using permutation on the given subderivation, we obtain ∉, y:T₂, x:S ⊢ t₁ : T₁. Using weakening on the other given derivation (Г ⊢ s : S), we obtain Г, y:T₂ ⊢ s : S. Now, by the induction hypothesis, Г, y:T₂ ⊢ [x ↦ s]t₁ : T₁. By T-ABS, Г ⊢ λy:T₂. [x ↦ s]t₁ : T₂→T₁. But this is precisely the needed result, since, by the definition of substitution, [x ↦ s]t = λy:T₁. [x ↦ s]t₁.

Case T-APP:

 t = t₁ t₂ Г, x:S ⊢ t₁ : T₂→T₁ Г, x:S ⊢ t₂ : T₂ T = T₁

By the induction hypothesis, Г ⊢ [x ↦ s]t₁ : T₂→T₁ and Г ⊢ [x ↦ s]t₂ : T₂. By T-APP, Г ⊢ [x ↦ s]t₁ [x ↦ s]t₂ : T, i.e., Г ⊢ [x ↦ s](t₁ t₂) : T.

Case T-TRUE:

 t = true T = Bool

Then [x ↦ s]t = true, and the desired result, Г ⊢ [x ↦ s]t : T, is immediate.

Case T-FALSE:

 t = false T = Bool

Similar.

Case T-IF:

 t = if t₁ then t₂ else t₃ Г, x:S ⊢ t₁ : Bool Г, x:S ⊢ t₂ : T Г, x:S ⊢ t₃ : T

Three uses of the induction hypothesis yield

   Г ⊢ [x ↦ s]t₁ : Bool   Г ⊢ [x ↦ s]t₂ : T   Г ⊢ [x ↦ s]t₃ : T,

from which the result follows by T-IF.

Using the substitution lemma, we can prove the other half of the type safety property-that evaluation preserves well-typedness.

9.3.9 Theorem [Preservation]

If Г ⊢ t : T and t → t′, then Г ⊢ t′ : T.

Proof: Exercise [Recommended, ⋆⋆⋆]. The structure is very similar to the proof of the type preservation theorem for arithmetic expressions (8.3.3), except for the use of the substitution lemma.

9.3.10 Exercise [Recommended, ⋆⋆⋆]

In Exercise 8.3.6 we investigated the subject expansion property for our simple calculus of typed arithmetic expressions. Does it hold for the "functional part" of the simply typed lambda-calculus? That is, suppose t does not contain any conditional expressions. Do t → t′ and Г ⊢ t′ : T imply Г ⊢ t : T?

^[3]Or, equivalently, by cases on the possible shapes of t, since for each syntactic constructor there is exactly one typing rule.

< Free Open Study >