13.5 Safety

---

13.5 Safety

Our final job in this chapter is to check that standard type safety properties continue to hold for the calculus with references. The progress theorem ("well-typed terms are not stuck") can be stated and proved almost as before (cf. 13.5.7); we just need to add a few straightforward cases to the proof, dealing with the new constructs. The preservation theorem is a bit more interesting, so let's look at it first.

Since we have extended both the evaluation relation (with initial and final stores) and the typing relation (with a store typing), we need to change the statement of preservation to include these parameters. Clearly, though, we cannot just add stores and store typings without saying anything about how they are related.

• If Г | Σ ⊢ t : T and t | μ → t′ | μ′, then Г | Σ ⊢ t′ : T. (Wrong!)

If we typecheck with respect to some set of assumptions about the types of the values in the store and then evaluate with respect to a store that violates these assumptions, the result will be disaster. The following requirement expresses the constraint we need.

13.5.1 Definition

A store μ is said to be well typed with respect to a typing context Г and a store typing Σ, written Г | Σ ⊢ μ, if dom(μ) = dom(Σ) and Г | Σ ⊢ μ(l) : Σ (l) for every l Î dom(μ).

Intuitively, a store μ is consistent with a store typing Σ if every value in the store has the type predicted by the store typing.

13.5.2 Exercise [⋆⋆]

Can you find a context Г, a store μ, and two different store typings Σ₁ and Σ₂ such that both Г | Σ₁ ⊢ μ and Г | Σ₂ ⊢ μ?

We can now state something closer to the desired preservation property:

If

      Г | Σ ⊢ t : T      t | μ → t′ | μ′      Г | Σ ⊢ μ      then Г | Σ ⊢ t′ : T.      (Less wrong.) 

This statement is fine for all of the evaluation rules except the allocation rule E-REFV. The problem is that this rule yields a store with a larger domain than the initial store, which falsifies the conclusion of the above statement: if μ′ includes a binding for a fresh location l, then l cannot be in the domain of Σ, and it will not be the case that t′ (which definitely mentions l) is typable under Σ.

Evidently, since the store can increase in size during evaluation, we need to allow the store typing to grow as well. This leads us to the final (correct) statement of the type preservation property:

13.5.3 Theorem [Preservation]

If

    Γ | Σ ⊢ t : T    Γ | Σ ⊢ μ    t | μ → t′ | μ′ 

then, for some Σ′ ⊇ Σ,

    Γ | Σ′ ⊢ t′ : T    Γ | Σ′ ⊢ μ′. 

Note that the preservation theorem merely asserts that there is some store typing Σ′ ⊇ Î (i.e., agreeing with Σ on the values of all the old locations) such that the new term t′ is well typed with respect to Σ′; it does not tell us exactly what Σ′ is. It is intuitively clear, of course, that Σ′ is either Σ or else it is exactly (μ, l ↦ T₁), where l is a newly allocated location (the new element of the domain of μ′) and T₁ is the type of the initial value bound to l in the extended store (μ, l ↦ v₁), but stating this explicitly would complicate the statement of the theorem without actually making it any more useful: the weaker version above is already in the right form (because its conclusion implies its hypothesis) to "turn the crank" repeatedly and conclude that every sequence of evaluation steps preserves well-typedness. Combining this with the progress property, we obtain the usual guarantee that "well-typed programs never go wrong."

To prove preservation, we need a few technical lemmas. The first is an easy extension of the standard substitution lemma (9.3.8).

13.5.4 Lemma [Substitution]

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

Proof: Just like Lemma 9.3.8.

The next states that replacing the contents of a cell in the store with a new value of appropriate type does not change the overall type of the store.

13.5.5 Lemma

If

    Г | Σ ⊢ μ    Σ(l) = T    Г | Σ ⊢ v : T then Г | Σ ⊢ [l ↦ v]μ. 

Proof: Immediate from the definition of Г | Σ ⊢ μ.

Finally, we need a kind of weakening lemma for stores, stating that, if a store is extended with a new location, the extended store still allows us to assign types to all the same terms as the original.

13.5.6 Lemma

If Г | Σ ⊢ t : T and Σ′ ⊇ Σ, then Г | Σ′ ⊢ t : T.

Proof: Easy induction.

Now we can prove the main preservation theorem.

Proof of 13.5.3: Straightforward induction on evaluation derivations, using the lemmas above and the inversion property of the typing rules (a straight-forward extension of 9.3.1).

The statement of the progress theorem (9.3.5) must also be extended to take stores and store typings into account:

13.5.7 Theorem [Progress]

Suppose t is a closed, well-typed term (that is, ø | Σ ⊢ t : T for some T and Σ). Then either t is a value or else, for any store μ such that ø | Σ ⊢ μ, there is some term t′ and store μ′ with t | μ → t′ | μ′.

Proof: Straightforward induction on typing derivations, following the pattern of 9.3.5. (The canonical forms lemma, 9.3.4, needs two additional cases stating that all values of type Ref T are locations and similarly for Unit.)

13.5.8 Exercise [Recommended, ⋆⋆⋆]

Is the evaluation relation in this chapter normalizing on well-typed terms? If so, prove it. If not, write a well-typed factorial function in the present calculus (extended with numbers and booleans).

---