ReferencesTyping Mutable References

Most real languages include impure features ("computational effects")...
  • mutable pointer structures
  • non-local control constructs (exceptions, continuations, etc.)
  • process synchronization and communication
  • etc.
Goal for this chapter: formalize pointers.

Definitions

In most real-world programming languages, the mechanisms of name binding and storage allocation are (intentionally) confused: every name refers to a mutable piece of storage.
Conceptually, it's cleaner to separate the two:
  • use the mechanisms we already have for name binding (abstraction, let);
  • introduce new, explicit operations for allocating, changing, and looking up the contents of references (pointers).

Syntax

The basic operations on references are allocation, dereferencing, and assignment.
  • To allocate a reference, we use the ref operator, providing an initial value for the new cell.
    For example, ref 5 creates a new cell containing the value 5, and reduces to a reference to that cell.
  • To read the current value of this cell, we use the dereferencing operator !.
    For example, !(ref 5) reduces to 5.
  • To change the value stored in a cell, we use the assignment operator.
    If r is a reference, r := 7 will store the value 7 in the cell referenced by r.

Types

If T is a type, then Ref T is the type of references to cells holding values of type T.
      T ::= Nat
          | Unit
          | T → T
          | Ref T

Terms

Besides the usual variables, abstractions, applications, terms related to natural numbers, and unit, we need four more sorts of terms in order to handle mutable references: 
      t ::= ...              Terms
          | ref t              allocation
          | !t                 dereference
          | t := t             assignment
          | l                  location

Typing (Preview)

Informally, the typing rules for allocation, dereferencing, and assignment will look like this:
Gamma |-- t1 ∈ T1 (T_Ref)  
Gamma |-- ref t1 ∈ Ref T1
Gamma |-- t1 ∈ Ref T1 (T_Deref)  
Gamma |-- !t1 ∈ T1
Gamma |-- t1 ∈ Ref T2
Gamma |-- t2 ∈ T2 (T_Assign)  
Gamma |-- t1 := t2 : Unit
The rule for locations will require a bit more machinery, and this will motivate some changes to the other rules; we'll come back to this later.

Values and Substitution

Besides abstractions, numbers, and the unit value, we have one new type of value: locations.
Inductive value : tm → Prop :=
  | v_abs : ∀ x T2 t1,
      value <{\x:T2, t1}>
  | v_nat : ∀ n : nat ,
      value <{ n }>
  | v_unit :
      value <{ unit }>
  | v_loc : ∀ l,
      value <{ loc l }>.

Extending substitution to handle the new syntax of terms is straightforward: substituting in a pointer leaves it unchanged.

Pragmatics

Side Effects and Sequencing

We can write (for example) 
       r:=succ(!r); !r
as an abbreviation for 
       (\x:Unit, !r) (r := succ(!r)).

References and Aliasing

It is important to bear in mind the difference between the reference that is bound to some variable r and the cell in the store that is pointed to by this reference.
If we make a copy of r, for example by binding its value to another variable s, what gets copied is only the reference, not the contents of the cell itself.
For example, after reducing 
      let r = ref 5 in
      let s = r in
      s := 82;
      (!r)+1
the cell referenced by r will contain the value 82, while the result of the whole expression will be 83. The references r and s are said to be aliases for the same cell.

The possibility of aliasing can make programs with references quite tricky to reason about. For example, the expression 
      r := 5; r := !s
assigns 5 to r and then immediately overwrites it with s's current value; this has exactly the same effect as the single assignment 
      r := !s
unless we happen to do it in a context where r and s are aliases for the same cell! 
      let r = ref 0 in
      let s = r in
      r := 5; r := !s

Shared State

Of course, aliasing is also a large part of what makes references useful. In particular, it allows us to set up "implicit communication channels" -- shared state -- between different parts of a program. For example, suppose we define a reference cell and two functions that manipulate its contents: 
      let c = ref 0 in
      let incc = \_:Unit, (c := succ (!c); !c) in
      let decc = \_:Unit, (c := pred (!c); !c) in
      ...
The Unit-abstractions ("thunks") are used here to prevent reduction until later.

Objects

We can go a step further and write a function that creates c, incc, and decc, packages incc and decc together into a record, and returns this record: 
      newcounter =
          \_:Unit,
             let c = ref 0 in
             let incc = \_:Unit, (c := succ (!c); !c) in
             let decc = \_:Unit, (c := pred (!c); !c) in
             {i=incc, d=decc}

Now, each time we call newcounter, we get a new record of functions that share access to the same storage cell c. The caller of newcounter can't get at this storage cell directly, but can affect it indirectly by calling the two functions. In other words, we've created a simple form of object. 
      let c1 = newcounter unit in
      let c2 = newcounter unit in
      // Note that we've allocated two separate storage cells now!
      let r1 = c1.i unit in
      let r2 = c2.i unit in
      r2  // yields 1, not 2!

References to Compound Types

A reference cell need not contain just a number: the primitives we've defined above allow us to create references to values of any type, including functions. For example, we can use references to functions to give an (inefficient) implementation of arrays of numbers, as follows.
Write NatArray for the type Ref (Nat→Nat).

To build a new array, we allocate a reference cell and fill it with a function that, when given an index, always returns 0. 
      newarray = \_:Unit, ref (\n:Nat,0)

To look up an element of an array, we simply apply the function to the desired index. 
      lookup = \a:NatArray, \n:Nat, (!a) n

The interesting part of the encoding is the update function. It takes an array, an index, and a new value to be stored at that index, and does its job by creating (and storing in the reference) a new function that, when it is asked for the value at this very index, returns the new value that was given to update, while on all other indices it passes the lookup to the function that was previously stored in the reference. 
      update = \a:NatArray, \m:Nat, \v:Nat,
                   let oldf = !a in
                   a := (\n:Nat, if equal m n then v else oldf n);

References to values containing other references can also be very useful, allowing us to define data structures such as mutable lists and trees.

Null References

One more difference between our references and C-style mutable variables: null pointers.
  • In C, a pointer variable can contain either a valid pointer into the heap or the special value NULL
  • A source of many errors and much tricky reasoning
    • (any pointer may potentially be "not there")
    • but occasionally useful
  • Null pointers are easy to implement here using references plus options (which can be built out of disjoint sum types) 
                Option T       =  Unit + T
            NullableRef T  =  Ref (Option T)

Garbage Collection

A last issue that we should mention before we move on with formalizing references is storage de-allocation. We have not provided any primitives for freeing reference cells when they are no longer needed. Instead, like many modern languages (including OCaml, Haskell, Java, etc.) we rely on the run-time system to perform garbage collection, automatically identifying and reusing cells that can no longer be reached by the program.

This is not just a question of taste in language design: it is extremely difficult to achieve type safety in the presence of an explicit deallocation operation. One reason for this is the familiar dangling reference problem: we allocate a cell holding a number, save a reference to it in some data structure, use it for a while, then deallocate it and allocate a new cell holding a boolean, possibly reusing the same storage. Now we can have two names for the same storage cell -- one with type Ref Nat and the other with type Ref Bool.

Operational Semantics

Locations

A reference names a location in the store (a.k.a. heap).
What is the store?
  • Concretely: An array of 8-bit bytes, indexed by 32-bit integers.
  • More abstractly: a list or array, of values
  • Even more abstractly: a partial function from locations to values.
We'll choose the middle way here: A store is a list of values, and a location is a natural-number index into this list.

Stores

A store is just a list of values. (This more concrete representation will be more convenient for proofs than the functional representation we used in Imp.)
Definition store := list tm.
We use store_lookup n st to retrieve the value of the reference cell at location n in the store st. Note that we must give a default value to nth in case we try looking up an index which is too large. (In fact, we will never actually do this, but proving that we don't will require a bit of work.)
Definition store_lookup (n:nat) (st:store) :=
  nth n st <{ unit }>.

To update the store, we use the replace function, which replaces the contents of a cell at a particular index.
Fixpoint replace {A:Type} (n:nat) (x:A) (l:list A) : list A :=
  match l with
  | nil ⇒ nil
  | h :: t ⇒
    match n with
    | O ⇒ x :: t
    | S n' ⇒ h :: replace n' x t
    end
  end.

Reduction

First, we augment existing reduction rules with stores:
value v2 (ST_AppAbs)  
(\x:T2,t1) v2 / st --> [x:=v2]t1 / st
t1 / st --> t1' / st' (ST_App1)  
t1 t2 / st --> t1' t2 / st'
value v1     t2 / st --> t2' / st' (ST_App2)  
v1 t2 / st --> v1 t2' / st'

Now we can give the rules for the new constructs:
   (ST_RefValue)  
ref v / st --> loc |st| / st,v
t1 / st --> t1' / st' (ST_Ref)  
ref t1 / st --> ref t1' / st'
l < |st| (ST_DerefLoc)  
!(loc l) / st --> lookup l st / st
t1 / st --> t1' / st' (ST_Deref)  
!t1 / st --> !t1' / st'
l < |st| (ST_Assign)  
loc l := v / st --> unit / replace l v st
t1 / st --> t1' / st' (ST_Assign1)  
t1 := t2 / st --> t1' := t2 / st'
t2 / st --> t2' / st' (ST_Assign2)  
v1 := t2 / st --> v1 := t2' / st'

Typing

The contexts assigning types to free variables are exactly the same as for the STLC: partial maps from identifiers to types.
Definition context := partial_map ty.

Store typings

Naturally, the key question is, "What is the type of a location?"
As a first try, observe that the type of a location is connected to the contents of the store [st].
Gamma |-- lookup l st : T1  
Gamma |-- loc l : Ref T1
But where does [st] come from?

We could try adding st to the judgment: Gamma; st |-- t : T, which gives us this rule:
Gamma; st |-- lookup l st : T1  
Gamma; st |-- loc l : Ref T1
But that means the whole store st, including all dynamically created values, is needed during typechecking. This does not seem like something we want.
Worse yet, it doesn't work at all for cyclic stores. For example, what is the type of location 0 in the following store? 
   [\x:Nat, (!(loc 1)) x, \x:Nat, (!(loc 0)) x]

Instead, we establish an invariant that the type of value stored in a location never changes.
This static representation of the store contents is called a store typing:
Definition store_ty := list ty.
Here we represent locations as indices into a list of types so the type at index i is the type of the values stored in cell i.
The store_Tlookup function retrieves the type at a particular index.
Definition store_Tlookup (n:nat) (ST:store_ty) :=
  nth n ST <{ Unit }>.

We can use the store typing ST to give a type to any location l like this:
l < |ST|  
Gamma; ST |-- loc l : Ref (store_Tlookup l ST)

The Typing Relation

l < |ST| (T_Loc)  
Gamma; ST |-- loc l : Ref (store_Tlookup l ST)
Gamma; ST |-- t1 : T1 (T_Ref)  
Gamma; ST |-- ref t1 : Ref T1
Gamma; ST |-- t1 : Ref T1 (T_Deref)  
Gamma; ST |-- !t1 : T1
Gamma; ST |-- t1 : Ref T2
Gamma; ST |-- t2 : T2 (T_Assign)  
Gamma; ST |-- t1 := t2 : Unit

Properties

Standard theorems...
  • Progress -- pretty much same as always
  • Preservation -- needs to be stated more carefully!

Well-Typed Stores

Evaulation and typing relations take more parameters now, so at a minumum we have to add these to the statement of preservation...
Theorem preservation_wrong1 : ∀ ST T t st t' st',
  empty ; ST |-- t \in T →
  t / st --> t' / st' →
  empty ; ST |-- t' \in T.
Abort.
Obviously wrong: no relation between assumed store typing and provided store!

We need a way of saying "this store satisfies the assumptions of that store typing"...
Definition store_well_typed (ST:store_ty) (st:store) :=
  length ST = length st ∧
  (∀ l, l < length st →
     empty; ST |-- { store_lookup l st } \in {store_Tlookup l ST }).
Informally, we will write ST |-- st for store_well_typed ST st.

We can now state something closer to the desired preservation property:
Theorem preservation_wrong2 : ∀ ST T t st t' st',
  empty ; ST |-- t \in T →
  t / st --> t' / st' →
  store_well_typed ST st →
  empty ; ST |-- t' \in T.
Abort.
This works... for all but one of the reduction rules!

Extending Store Typings

Intuition: Since the store can grow during reduction, we need to let the store typing grow too...
Inductive extends : store_ty → store_ty → Prop :=
  | extends_nil : ∀ ST',
      extends ST' nil
  | extends_cons : ∀ x ST' ST,
      extends ST' ST →
      extends (x::ST') (x::ST).

Preservation, Finally

We can now give the final, correct statement of the type preservation property:
Definition preservation_theorem := ∀ ST t t' T st st',
  empty ; ST |-- t \in T →
  store_well_typed ST st →
  t / st --> t' / st' →
  ∃ ST',
     extends ST' ST ∧
     empty ; ST' |-- t' \in T ∧
     store_well_typed ST' st'.
Note that this gives us just what we need to "turn the crank" when applying the theorem to multi-step reduction sequences.

Assignment Preserves Store Typing

Next, we must show 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. (This is needed for the ST_Assign rule.)
Lemma assign_pres_store_typing : ∀ ST st l t,
  l < length st →
  store_well_typed ST st →
  empty ; ST |-- t \in {store_Tlookup l ST} →
  store_well_typed ST (replace l t st).
Proof with auto.
  intros ST st l t Hlen HST Ht.
  inversion HST; subst.
  split. rewrite length_replace...
  intros l' Hl'.
  destruct (l' =? l) eqn: Heqll'.
  - (* l' = l *)
    apply eqb_eq in Heqll'; subst.
    rewrite lookup_replace_eq...
  - (* l' <> l *)
    apply eqb_neq in Heqll'.
    rewrite lookup_replace_neq...
    rewrite length_replace in Hl'.
    apply H0...
Qed.

Weakening for Stores

Finally, we need a lemma on store typings, stating that, if a store typing is extended with a new location, the extended one still allows us to assign the same types to the same terms as the original.
(The lemma is called store_weakening because it resembles the "weakening" lemmas found in proof theory, which show that adding a new assumption to some logical theory does not decrease the set of provable theorems.)
Lemma store_weakening : ∀ Gamma ST ST' t T,
  extends ST' ST →
  Gamma ; ST |-- t \in T →
  Gamma ; ST' |-- t \in T.
Proof with eauto.
  intros. induction H0; eauto.
  - (* T_Loc *)
    rewrite <- (extends_lookup _ _ ST')...
    apply T_Loc.
    eapply length_extends...
Qed.

We can use the store_weakening lemma to prove that if a store is well typed with respect to a store typing, then the store extended with a new term t will still be well typed with respect to the store typing extended with t's type.
Lemma store_well_typed_app : ∀ ST st t1 T1,
  store_well_typed ST st →
  empty ; ST |-- t1 \in T1 →
  store_well_typed (ST ++ T1::nil) (st ++ t1::nil).
Proof with auto.
  intros.
  unfold store_well_typed in ×.
  destruct H as [Hlen Hmatch].
  rewrite app_length, add_comm. simpl.
  rewrite app_length, add_comm. simpl.
  split...
  - (* types match. *)
    intros l Hl.
    unfold store_lookup, store_Tlookup.
    apply le_lt_eq_dec in Hl; destruct Hl as [Hlt | Heq].
    + (* l < length st *)
      apply <-Nat.succ_lt_mono in Hlt.
      rewrite !app_nth1...
      × apply store_weakening with ST. apply extends_app.
        apply Hmatch...
      × rewrite Hlen...
    + (* l = length st *)
      injection Heq as Heq; subst.
      rewrite app_nth2; try lia.
      rewrite <- Hlen.
      rewrite sub_diag. simpl.
      apply store_weakening with ST...
      { apply extends_app. }
      rewrite app_nth2; [|lia].
      rewrite sub_diag. simpl. assumption.
Qed.

Preservation!

Now that we've got everything set up right, the proof of preservation is actually quite straightforward.

Progress

As we've said, progress for this system is pretty easy to prove; the proof is very similar to the proof of progress for the STLC, with a few new cases for the new syntactic constructs.
Theorem progress : ∀ ST t T st,
  empty ; ST |-- t \in T →
  store_well_typed ST st →
  (value t ∨ ∃ t' st', t / st --> t' / st').
Proof with eauto.
  intros ST t T st Ht HST. remember empty as Gamma.
  induction Ht; subst; try solve_by_invert...
  - (* T_App *)
    right. destruct IHHt1 as [Ht1p | Ht1p]...
    + (* t1 is a value *)
      inversion Ht1p; subst; try solve_by_invert.
      destruct IHHt2 as [Ht2p | Ht2p]...
      × (* t2 steps *)
        destruct Ht2p as [t2' [st' Hstep]].
        ∃ <{ (\ x0 : T0, t0) t2' }>, st'...
    + (* t1 steps *)
      destruct Ht1p as [t1' [st' Hstep]].
      ∃ <{ t1' t2 }>, st'...
  - (* T_Succ *)
    right. destruct IHHt as [Ht1p | Ht1p]...
    + (* t1 is a value *)
      inversion Ht1p; subst; try solve [ inversion Ht ].
      × (* t1 is a const *)
        ∃ <{ {S n} }>, st...
    + (* t1 steps *)
      destruct Ht1p as [t1' [st' Hstep]].
      ∃ <{ succ t1' }>, st'...
  - (* T_Pred *)
    right. destruct IHHt as [Ht1p | Ht1p]...
    + (* t1 is a value *)
      inversion Ht1p; subst; try solve [inversion Ht ].
      × (* t1 is a const *)
        ∃ <{ {n - 1} }>, st...
    + (* t1 steps *)
      destruct Ht1p as [t1' [st' Hstep]].
      ∃ <{ pred t1' }>, st'...
  - (* T_Mult *)
    right. destruct IHHt1 as [Ht1p | Ht1p]...
    + (* t1 is a value *)
      inversion Ht1p; subst; try solve [inversion Ht1].
      destruct IHHt2 as [Ht2p | Ht2p]...
      × (* t2 is a value *)
        inversion Ht2p; subst; try solve [inversion Ht2].
        ∃ <{ {n × n0} }>, st...
      × (* t2 steps *)
        destruct Ht2p as [t2' [st' Hstep]].
        ∃ <{ n × t2' }>, st'...
    + (* t1 steps *)
      destruct Ht1p as [t1' [st' Hstep]].
      ∃ <{ t1' × t2 }>, st'...
  - (* T_If0 *)
    right. destruct IHHt1 as [Ht1p | Ht1p]...
    + (* t1 is a value *)
      inversion Ht1p; subst; try solve [inversion Ht1].
      destruct n.
      × (* n = 0 *) ∃ t2, st...
      × (* n = S n' *) ∃ t3, st...
    + (* t1 steps *)
      destruct Ht1p as [t1' [st' Hstep]].
      ∃ <{ if0 t1' then t2 else t3 }>, st'...
  - (* T_Ref *)
    right. destruct IHHt as [Ht1p | Ht1p]...
    + (* t1 steps *)
      destruct Ht1p as [t1' [st' Hstep]].
      ∃ <{ref t1'}>, st'...
  - (* T_Deref *)
    right. destruct IHHt as [Ht1p | Ht1p]...
    + (* t1 is a value *)
      inversion Ht1p; subst; try solve_by_invert.
      eexists. eexists. apply ST_DerefLoc...
      inversion Ht; subst. inversion HST; subst.
      rewrite <- H...
    + (* t1 steps *)
      destruct Ht1p as [t1' [st' Hstep]].
      ∃ <{ ! t1' }>, st'...
  - (* T_Assign *)
    right. destruct IHHt1 as [Ht1p|Ht1p]...
    + (* t1 is a value *)
      destruct IHHt2 as [Ht2p|Ht2p]...
      × (* t2 is a value *)
        inversion Ht1p; subst; try solve_by_invert.
        eexists. eexists. apply ST_Assign...
        inversion HST; subst. inversion Ht1; subst.
        rewrite H in H4...
      × (* t2 steps *)
        destruct Ht2p as [t2' [st' Hstep]].
        ∃ <{ t1 := t2' }>, st'...
    + (* t1 steps *)
      destruct Ht1p as [t1' [st' Hstep]].
      ∃ <{ t1' := t2 }>, st'...
Qed.

References and Nontermination

An important fact about the STLC (proved in chapter Norm) is that it is is normalizing -- that is, every well-typed term can be reduced to a value in a finite number of steps.
What about STLC + references? Surprisingly, adding references causes us to lose the normalization property: there exist well-typed terms in the STLC + references which can continue to reduce forever, without ever reaching a normal form!

How can we construct such a term? The main idea is to make a function which calls itself. We first make a function which calls another function stored in a reference cell; the trick is that we then smuggle in a reference to itself! 
   (\r:Ref (Unit -> Unit),
        r := (\x:Unit,(!r) unit); (!r) unit)
   (ref (\x:Unit,unit))