13.4 Store Typings

< Free Open Study >

Having extended our syntax and evaluation rules to accommodate references, our last job is to write down typing rules for the new constructs-and, of course, to check that they are sound. Naturally, the key question is, "What is the type of a location?"

When we evaluate a term containing concrete locations, the type of the result depends on the contents of the store that we start with. For example, if we evaluate the term !l₂ in the store (l₁ ↦ unit, l₂ ↦ unit), the result is unit; if we evaluate the same term in the store (l₁ ↦ unit, l₂ ↦ λx:Unit.x), the result is λx:Unit.x. With respect to the former store, the location l₂ has type Unit, and with respect to the latter it has type Unit→Unit. This observation leads us immediately to a first attempt at a typing rule for locations:

That is, to find the type of a location l, we look up the current contents of l in the store and calculate the type T₁ of the contents. The type of the location is then Ref T₁.

Having begun in this way, we need to go a little further to reach a consistent state. In effect, by making the type of a term depend on the store, we have changed the typing relation from a three-place relation (between contexts, terms, and types) to a four-place relation (between contexts, stores, terms, and types). Since the store is, intuitively, part of the context in which we calculate the type of a term, let's write this four-place relation with the store to the left of the turnstile: Г | μ ⊢ t : T. Our rule for typing references now has the form

and all the rest of the typing rules in the system are extended similarly with stores. The other rules do not need to do anything interesting with their stores-just pass them from premise to conclusion.

However, there are two problems with this rule. First, typechecking is rather inefficient, since calculating the type of a location l involves calculating the type of the current contents v of l. If l appears many times in a term t, we will re-calculate the type of v many times in the course of constructing a typing derivation for t. Worse, if v itself contains locations, then we will have to recalculate their types each time they appear. For example, if the store contains

   (l₁ ↦ λx:Nat. 999,    l₂ ↦ λx:Nat. (!l₁) x,    l₃ ↦ λx:Nat. (!l₂) x,    l₄ ↦ λx:Nat. (!l₃) x,    l₅ ↦ λx:Nat. (!l₄) x),

then calculating the type of l₅ involves calculating those of l₄, l₃, l₂, and l₁.

Second, the proposed typing rule for locations may not allow us to derive anything at all, if the store contains a cycle. For example, there is no finite typing derivation for the location l₂ with respect to the store

   (l₁ ↦ λx:Nat. (!l₂) x,    l₂ ↦ λx:Nat. (!l₁) x),

since calculating a type for l₂ requires finding the type of l₁, which in turn involves l₁, etc. Cyclic reference structures do arise in practice (e.g., they can be used for building doubly linked lists), and we would like our type system to be able to deal with them.

13.4.1 Exercise [⋆]

Can you find a term whose evaluation will create this particular cyclic store?

Both of these problems arise from the fact that our proposed typing rule for locations requires us to recalculate the type of a location every time we mention it in a term. But this, intuitively, should not be necessary. After all, when a location is first created, we know the type of the initial value that we are storing into it. Moreover, although we may later store other values into this location, those other values will always have the same type as the initial one. In other words, we always have in mind a single, definite type for every location in the store, which is fixed when the location is allocated. These intended types can be collected together as a store typing-a finite function mapping locations to types. We'll use the metavariable Σ to range over such functions.

Suppose we are given a store typing Σ describing the store μ in which some term t will be evaluated. Then we can use Σ to calculate the type of the result of t without ever looking directly at μ. For example, if Σ is (l₁ ↦ Unit, l₂ ↦ Unit→Unit), then we may immediately infer that !l₂ has type Unit→Unit. More generally, the typing rule for locations can be reformulated in terms of store typings like this:

Typing is again a four-place relation, but it is parameterized on a store typing rather than a concrete store. The rest of the typing rules are analogously augmented with store typings.

Of course, these typing rules will accurately predict the results of evaluation only if the concrete store used during evaluation actually conforms to the store typing that we assume for purposes of typechecking. This proviso exactly parallels the situation with free variables in all the calculi we have seen up to this point: the substitution lemma (9.3.8) promises us that, if Г ⊢ t : T, then we can replace the free variables in t with values of the types listed in Г to obtain a closed term of type T, which, by the type preservation theorem (9.3.9) will evaluate to a final result of type T if it yields any result at all. We will see in §13.5 how to formalize an analogous intuition for stores and store typings.

Finally, note that, for purposes of typechecking the terms that programmers actually write, we do not need to do anything tricky to guess what store typing we should use. As we remarked above, concrete location constants arise only in terms that are the intermediate results of evaluation; they are not in the language that programmers write. Thus, we can simply typecheck the programmer's terms with respect to the empty store typing. As evaluation proceeds and new locations are created, we will always be able to see how to extend the store typing by looking at the type of the initial values being placed in newly allocated cells; this intuition is formalized in the statement of the type preservation theorem below (13.5.3).

Now that we have dealt with locations, the typing rules for the other new syntactic forms are quite straightforward. When we create a reference to a value of type T₁, the reference itself has type Ref T₁.

Notice that we do not need to extend the store typing here, since the name of the new location will not be determined until run time, while Σ records only the association between already-allocated storage cells and their types.

Conversely, if t₁ evaluates to a location of type Ref T₁₁, then dereferencing t₁ is guaranteed to yield a value of type T₁₁.

Finally, if t₁ denotes a cell of type Ref T₁₁, then we can store t₂ into this cell as long as the type of t₂ is also T₁₁:

Figure 13-1 summarizes the typing rules (and the syntax and evaluation rules, for easy reference) for the simply typed lambda-calculus with references.

< Free Open Study >