9.3 Properties of Typing

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]

1. If v is a value of type Bool , then v is either true or false .

2. 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.

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.

t = λy:T

2

.t

1

T = T

2



T

1

, x:S, y:T

2


⊢

t

1

: T

1

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 ₁ .

t = t

1

t

2

, x:S

⊢

t

1

: T

2



T

1

, x:S

⊢

t

2

: T

2

T = T

1

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 .

t = true T = Bool

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

t = false T = Bool

Similar.

t = if t

1

then t

2

else t

3

, x:S

⊢

t

1

: Bool , x:S

⊢

t

2

: T , x:S

⊢

t

3

: T

Three uses of the induction hypothesis yield

⊢

[x

↦

s]t

1

: Bool

⊢

[x

↦

s]t

2

: T

⊢

[x

↦

s]t

3

: 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 ?