Mutation and References

A let binds a name to a value, and the binding does not change: within its scope the name denotes that one value, and Part III built the environment so that looking the name up always finds it. A program that only binds and reads can compute a result, but it has no way to express a quantity that changes over time while the name that refers to it stays put — a counter that climbs, a running total a loop adds into, a balance that a deposit raises. Each of those is one thing, referred to by one name, holding a different value at a later moment than it held before.

The environment cannot supply that on its own. It maps a name to a value once, when the name is bound, and a later read of the name returns the same value; rebinding the name with a second let creates a new, separately scoped binding rather than altering the first. What changes over time has to live somewhere the environment points at rather than somewhere it is — a cell whose contents a program can overwrite, with the name holding the cell rather than the contents. This chapter introduces that cell. It is the mutation the previous chapter named as Bridger’s one built-in effect; here are the forms that create a cell, read it, and write it, and the addition to the evaluation judgment that lets a written value be read back later.

Origins of mutable cells

Two traditions answer the question of what a name denotes, and they place mutation differently.

In Fortran, Algol 60, and their descendants C and Java, a variable is a mutable cell, and the name and the cell are the same thing. Writing x = x + 1 reads the cell the name x denotes, adds one, and stores the result back into that same cell; the name does not acquire a new binding, the cell it has always named has the value it contains overwritten. Assignment to a variable is the primitive action, and every variable is a memory cell a program can read or write.

The functional tradition places it elsewhere. In Lisp and in Landin’s ISWIM, the reading of let the book took in Part III treats a binding as a fixed association between a name and a value; a name, once bound, denotes its value for the extent of its scope and is never modified. A language built only from that has no mutation at all. Standard ML reconciled the two by keeping the binding immutable and adding a separate kind of value — a reference cell, a box allocated on demand, whose contents a program may read and overwrite while the binding that holds the box stays fixed. Mutation moves out of the binding and into a value the binding refers to. Bridger follows that split: a let binds once and for all, and a program that needs a value to change asks for a cell and mutates the cell.

The store

A cell needs somewhere to live. The environment already maps names to values and does not change an existing entry, so the cells go in a second map, the store, written $\sigma$: a finite map from locations to values. A location, written $\ell$, is the identity of one allocated cell — a value in its own right, the thing a name holds when it refers to a cell. The environment maps a name to a value; the store maps a location to a value; and a name bound to a cell is a name the environment maps to a location that the store, in turn, maps to the cell’s current contents.

The store changes as a program runs, so evaluation has to carry it. The judgment grew in Part III from $e\Downarrow v$ to $\rho ⊢e\Downarrow v$ when names arrived; it grows again here to thread the store through the evaluation, taking one store in and handing one store out:

$$\rho ⊢⟨e,\sigma ⟩\Downarrow ⟨v,{\sigma }^{\prime }⟩$$

read as: in environment $\rho$, evaluating $e$ against the store $\sigma$ yields the value $v$ and leaves the store ${\sigma }^{\prime }$. The environment goes in but does not come back — evaluating an expression cannot change what a name is bound to — while the store goes in and comes out, because evaluating an expression can change what a cell holds. (The reference’s full judgment threads one more component, the relation database $\Delta$ of Part VII, and carries the extra outcome a return produces; this part uses the env-and-store slice.)

Every rule now threads the store, and the threading fixes the order in which subexpressions run. A form with two operands evaluates the first against the incoming store, then the second against the store the first handed out, then combines the results — left to right, each step’s output store the next step’s input:

$$\frac{\rho ⊢⟨e_1,\sigma ⟩\Downarrow ⟨v_1,{\sigma }_1⟩\rho ⊢⟨e_2,{\sigma }_1⟩\Downarrow ⟨v_2,{\sigma }_2⟩v_1,v_2\in \mathbb{Z}}{\rho ⊢⟨e_1+e_2,\sigma ⟩\Downarrow ⟨v_1+v_2,{\sigma }_2⟩}(\text{E-Add})$$

Addition takes the store in and passes it along unchanged in the sense that it writes nothing of its own, but it still threads it: if evaluating $e_1$ allocates a cell, $e_2$ evaluates against the store that already holds it. Part II left the order of +’s operands open, observing that it could be fixed once effects existed; the threaded store is what fixes it. Most forms are like +: they thread the store to pin down order and hand it back untouched. Three forms change it.

Creating, reading, and writing a cell

Bridger writes the three operations as ref e, deref e, and e1 := e2.

ref e allocates a fresh cell holding the value of e, and the cell — its location — is the value the form returns. The rule evaluates e, picks a location not already in use, and extends the store so that the new location maps to the value:

$$\frac{\rho ⊢⟨e,\sigma ⟩\Downarrow ⟨v,{\sigma }_1⟩\ell \notin \mathrm{dom}({\sigma }_1)}{\rho ⊢⟨\text{ref}e,\sigma ⟩\Downarrow ⟨\ell ,{\sigma }_1[\ell \mapsto v]⟩}(\text{E-Ref})$$

The value handed back is $\ell$, the location, not $v$; a program keeps the cell by binding the location to a name, let counter = ref 0.

deref e reads a cell. It evaluates e to a location and returns what the store maps that location to, leaving the store as it found it:

$$\frac{\rho ⊢⟨e,\sigma ⟩\Downarrow ⟨\ell ,{\sigma }_1⟩\ell \in \mathrm{dom}({\sigma }_1)}{\rho ⊢⟨\text{deref}e,\sigma ⟩\Downarrow ⟨{\sigma }_1(\ell ),{\sigma }_1⟩}(\text{E-Deref})$$

e1 := e2 overwrites a cell. It evaluates e1 to the location to write, then e2 to the value to store there, then updates the store at that location and returns () — assignment is an effect, and its value is the unit that reports only that the effect happened, exactly as the previous chapter described for the effectful forms:

$$\frac{\rho ⊢⟨e_1,\sigma ⟩\Downarrow ⟨\ell ,{\sigma }_1⟩\rho ⊢⟨e_2,{\sigma }_1⟩\Downarrow ⟨v,{\sigma }_2⟩\ell \in \mathrm{dom}({\sigma }_2)}{\rho ⊢⟨e_1:=e_2,\sigma ⟩\Downarrow ⟨(),{\sigma }_2[\ell \mapsto v]⟩}(\text{E-Assign})$$

The order is the cell first, then the value written into it. It is visible when both sides have effects of their own: in (f()) := (g()), f runs before g, because e1 is evaluated against the incoming store and e2 against the store e1 produced. A cell together with these three forms is enough to count:

let counter = ref 0;
counter := deref counter + 1;
deref counter                  // 1

ref 0 allocates a cell holding 0 and binds counter to its location. The assignment reads the cell (deref counter is 0), adds one, and writes 1 back into the same cell; the location counter holds has not changed, its contents have. The trailing deref counter reads the cell again and finds 1. This is the shape a while loop repeats to accumulate a result across its iterations, which is why the cell arrives before the loop that needs it.

A location is a value like any other, so it can be read from a cell, passed to a function, or returned — and two names can end up holding the same location:

let a = ref 0;
let b = a;                     // b holds the same location as a
a := 1;
deref b                        // 1

let b = a binds b to the value a holds, which is a location, so a and b name one cell. Writing through a changes the cell both refer to, and reading through b finds the new value. This is aliasing: two names for one mutable cell, so that a write reached by one name is observed through the other. It follows directly from a name holding the location rather than the contents, and it is what makes shared mutable state — and structures that point at each other — expressible. It is also what makes a program with mutation harder to reason about than one without, since a write here can be a change seen there; Part V returns to the style that keeps mutation scarce for that reason.

Building it

The store is a piece of interpreter state beside the environment. The provided runtime supplies it as a Store with three operations — allocate a cell and get back its location, read a location, and write a location — and a location is a small handle that a Value can carry:

Value::Ref(Loc)                // a value that is a location in the store

impl Store {
    fn alloc(&mut self, v: Value) -> Loc;   // E-Ref: fresh cell, gives its location
    fn read(&self, l: &Loc) -> Value;       // E-Deref: the cell's contents
    fn write(&mut self, l: &Loc, v: Value); // E-Assign: overwrite the cell
}

The three forms are three arms of eval_expr. ref e evaluates e and calls alloc, returning Value::Ref of the location. deref e evaluates e to a Value::Ref(l) and returns store.read(&l). e1 := e2 evaluates e1 to a Value::Ref(l), then e2 to a value, calls store.write(&l, v), and returns Value::Unit; a deref or := whose operand is not a location is a runtime type error, the store’s stuck case. The rules thread a store in and a store out; the interpreter instead keeps the one store on the interpreter and mutates it in place, so alloc and write are the step from $\sigma$ to ${\sigma }^{\prime }$ — the threading made physical. A cell, once allocated, is never reclaimed: the store only grows, matching E-Ref, which always takes a fresh location and never reuses one. When the store is read back as a space cost, that choice returns as a subject in Part X.

The surface form ref x = e is not a new binding. It reads as let x = ref e: allocate a cell for e and bind x to its location. It earns its own keyword because binding a name to a fresh cell is the common case and ref x = 0 says it more plainly than let x = ref 0, but the parser expands it to the let and the evaluator sees only the two forms it already has.

The type a reference carries, written ref<τ> for a cell holding values of type τ, and the rules that keep deref and := from being applied to a non-location before the program runs, are the subject of the type checker in Part VI. The evaluator here admits any location where one is required and reaches its stuck case at runtime when handed something else.

The design space

The three languages that keep the Algol boundary of the previous chapter also keep the variable-as-cell model. In C, Java, and Python a plain variable is mutable: x = e reassigns the name, and there is no separate word to allocate a cell or to read one, because every variable already is one. What Bridger writes as ref/deref/:= is, in those languages, the unmarked default state of every name. Aliasing is present there too, carried by pointers or object references, and it is likewise implicit — two variables may refer to one object with nothing in the syntax to say so.

ML draws the line where Bridger does: a binding is immutable, a reference cell is a separate value created by ref and reached by an explicit read and write, and a mutation site is visible in the program as one of those operations. The cost is the two extra words, ref and deref, on every use of a cell; what they buy is that a name not bound to a ref cannot be assigned into at all, so the places a program mutates are exactly the places those words appear.

Rust marks mutation on the binding but restricts the sharing. A let is immutable and let mut makes a rebindable variable, closer to the variable-as-cell model; sharing goes through borrows, & and &mut, and the compiler’s rules forbid a mutable borrow to coexist with any other borrow of the same value, so the aliasing that Bridger and ML permit freely is the case Rust’s borrow checker exists to rule out. Bridger takes ML’s first-class cell rather than Rust’s borrowing because a cell that is an ordinary value needs no second discipline layered over the language — one immutable let binds cells and non-cells alike, and a location is passed, stored, and compared like any other value. What that leaves on the table is the compiler-checked guarantee against data races and aliased writes that Rust’s rules provide; Bridger permits the aliasing and asks the programmer to manage it.

Across the three, the decision is where a program says “this can change”: on every variable by default, on a binding marked mut, or on a value obtained through ref. Bridger’s answer keeps the binding immutable and names the cell, so that the environment of Part III is left exactly as it was and everything that changes over time lives in the store.

Further reading

Reference cells and the store: The Definition of Standard ML (Robin Milner, Mads Tofte, Robert Harper, and David MacQueen, revised edition, 1997) gives the reference cell — ref, !, and := — its formal semantics over a store, the model Bridger’s cell follows. Benjamin Pierce’s Types and Programming Languages (2002) devotes its chapter “References” to building mutable cells on top of a pure calculus: the store as a map from locations to values, the evaluation relation threaded through it, and the typing of Ref T, in the same order this part and Part VI take them. The variable-as-cell model, for contrast, is described in the “References” and ownership chapters of The Rust Programming Language, where mutability is a property of a binding and a borrow rather than a value, and the borrow checker rules out the aliased writes the store model here permits.

Concept checks