References and Mutable State

Everything so far in the pure fragment of the language had a comforting property: an expression's value depended only on its subexpressions. Evaluate 2+3 here or there, now or later, and you always get 5. The moment we add mutable state — a cell you can write into and read back — that property shatters. !r can be 0 on one line and 99 on the next, with the very same syntax, because someone assigned to r in between. To model this honestly we must thread an extra object through every evaluation: the store.

This lesson introduces the three reference operations — ref e (allocate a fresh cell), !e (read it), and e₁ := e₂ (write it) — and gives them a precise operational and typing semantics. The surprise, and the deep lesson, is that references break naive type safety. Keeping a stateful language sound needs a genuinely new idea: a store typing \Sigma that runs alongside the value store \sigma. Miss it and cyclic stores make the type-checker loop forever.

The store: \sigma

A reference cell is not a value — it is a name for a place. That place lives in the store. Formally, introduce a countable set of locations \ell \in \mathit{Loc}, and let the store \sigma be a finite partial map from locations to values:

\sigma : \mathit{Loc} \rightharpoonup \mathit{Value}

A location \ell is itself a perfectly good value (the runtime representation of a pointer). Evaluation is now a relation on configurations \langle e, \sigma \rangle — an expression paired with the current store — and the three operations do exactly what their names say. We write \sigma[\ell \mapsto v] for the store that agrees with \sigma everywhere except at \ell, where it yields v:

\dfrac{\ell \notin \mathrm{dom}(\sigma)}{\langle \mathsf{ref}\,v,\ \sigma\rangle \longrightarrow \langle \ell,\ \sigma[\ell \mapsto v]\rangle} \qquad \langle\,!\ell,\ \sigma\rangle \longrightarrow \langle \sigma(\ell),\ \sigma\rangle \qquad \langle \ell := v,\ \sigma\rangle \longrightarrow \langle \mathsf{unit},\ \sigma[\ell \mapsto v]\rangle

ref v allocates: pick a fresh location not yet in the store, install v there, and hand back the location. !ℓ dereferences: look up the current contents. ℓ := v updates: overwrite the contents and return \mathsf{unit} — assignment is done for its effect, not its value. The store is the only thing that changes; the location handed out by ref never moves.

Aliasing: two names, one cell

Because a location is a value, you can copy it. Two variables can then hold the same location — they are aliases — and a write through one is instantly visible through the other. This is the single most important, and most treacherous, consequence of mutable state. Watch it happen in the heap:

In pseudocode: x = ref 0; y = x; x := 99; !y yields 99, not 0. The assignment y = x did not copy the cell; it copied the arrow. This is why reasoning about imperative programs is hard — a function handed a reference can change state that its caller thought was private, and two references you believe are distinct may secretly point at one place. Every data-race, every "spooky action at a distance" bug, is aliasing biting.

Typing references, and why \Sigma is forced on us

Give references a type constructor: if a cell holds a T, the reference to it has type \mathtt{Ref}\,T. The three operation rules are clean:

\dfrac{\Gamma \mid \Sigma \vdash e : T}{\Gamma \mid \Sigma \vdash \mathsf{ref}\,e : \mathtt{Ref}\,T} \qquad \dfrac{\Gamma \mid \Sigma \vdash e : \mathtt{Ref}\,T}{\Gamma \mid \Sigma \vdash\ !e : T} \qquad \dfrac{\Gamma \mid \Sigma \vdash e_1 : \mathtt{Ref}\,T \qquad \Gamma \mid \Sigma \vdash e_2 : T} {\Gamma \mid \Sigma \vdash e_1 := e_2 : \mathtt{Unit}}

But now: what is the type of a bare location \ell? During evaluation the store contains actual locations, and to prove type safety (that a well-typed program never gets stuck) we must be able to type them. The naive idea — "the type of \ell is \mathtt{Ref}\,T where T is the type of \sigma(\ell)" — fails. If a cell holds a value that mentions its own location (a cyclic store, easy to build: a cell holding a function that reads that same cell), typing \ell would require typing \sigma(\ell), which requires typing \ell again — the checker diverges.

The fix is Harper and Tofte's store typing \Sigma: a finite map from locations to types, fixed separately from the store's contents. A location is typed by looking it up in \Sigma, not by inspecting the value inside it:

\dfrac{\Sigma(\ell) = T}{\Gamma \mid \Sigma \vdash \ell : \mathtt{Ref}\,T}

The subtlety in that theorem is \Sigma' \supseteq \Sigma: allocation grows the store typing. Because \Sigma only ever gets bigger, and a location's type in it never changes, the cyclic-store paradox evaporates — you type \ell by a table lookup that bottoms out immediately.

A store-based evaluator

Here is a working interpreter for a tiny imperative language with ref/!/:=, threading an explicit store — a Map from numeric locations to values. It demonstrates allocation, update, and — crucially — aliasing: two bindings to one location, where a write through the first is seen through the second. Press Run:

// Values: a number, unit, or a LOCATION (a reference cell's address). type Value = | { tag: "num"; n: number } | { tag: "unit" } | { tag: "loc"; addr: number }; // The store σ : Loc ⇀ Value, plus a fresh-location counter. class Store { private cells = new Map<number, Value>(); private next = 0; alloc(v: Value): Value { // ref v => fresh ℓ, σ[ℓ ↦ v] const addr = this.next++; this.cells.set(addr, v); return { tag: "loc", addr }; } read(loc: Value): Value { // !ℓ => σ(ℓ) if (loc.tag !== "loc") throw new Error("deref of non-location"); return this.cells.get(loc.addr)!; } write(loc: Value, v: Value): Value { // ℓ := v => σ[ℓ ↦ v], returns unit if (loc.tag !== "loc") throw new Error("assign to non-location"); this.cells.set(loc.addr, v); return { tag: "unit" }; } } const num = (n: number): Value => ({ tag: "num", n }); const σ = new Store(); // x = ref 0; y = x (ALIAS: y holds the SAME location, not a copy of the cell) const x = σ.alloc(num(0)); const y = x; console.log("after y = x, !y =", (σ.read(y) as { n: number }).n); // 0 // x := 99 — write through x... σ.write(x, num(99)); // ...and read it back through y. Aliasing means y sees the change. console.log("after x := 99, !y =", (σ.read(y) as { n: number }).n); // 99 // A genuinely fresh cell is independent. const z = σ.alloc(num(7)); σ.write(z, num(123)); console.log("!x =", (σ.read(x) as { n: number }).n, " !z =", (σ.read(z) as { n: number }).n); // 99 123

The line const y = x is the whole point: it copies a { tag: "loc", addr } — an address — so x and y denote one cell. That single fact is what the store model exists to make precise, and what the store typing exists to keep sound.

In pure ML, let id = fun x -> x gets the polymorphic type \forall\alpha.\ \alpha \to \alpha and can be used at many types at once. You might hope a reference could be polymorphic too — but it cannot, and the reason is a famous soundness hole. If let r = ref [] were given type \forall\alpha.\ \mathtt{Ref}(\mathtt{List}\,\alpha), you could store a list of ints into r at type \alpha=\mathtt{int} and then read it back as a list of strings at \alpha=\mathtt{string} — a type error the checker waved through. Early ML had exactly this bug. The cure is the value restriction: only syntactic values (not general expressions like ref []) may be generalised. It is a slightly blunt rule that occasionally annoys, but it is the price of having both mutation and Hindley–Milner polymorphism in one sound language.

The tempting shortcut — "to type a location, just look at what's stored in it" — breaks type safety, and not in a rare corner. A single cell that holds a function closing over that same cell makes the store cyclic, and the naive rule sends the type-checker into an infinite regress: typing \ell demands typing \sigma(\ell) demands typing \ell. The store typing \Sigma exists precisely to cut this knot: \ell's type is declared in \Sigma and read off by lookup, independent of the — possibly self-referential — value currently inside the cell.

A second gotcha: \Sigma only ever grows, and a location keeps its type for life. You never "retype" a cell — assignment ℓ := v requires v to have the cell's existing type \Sigma(\ell). That is what makes the preservation proof go through, and why you cannot store an int in a cell and later an int → int.