Uniqueness Types and Destructive Update

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Suppose a list cell is consumed exactly once. May a program overwrite the cell? Not yet. A hidden pointer may still reach it. Affine use controls the future use of one name; destructive update needs a statement about every name that can reach the same node. The system in this chapter obtains that statement by typing graphs rather than pretending that source terms are trees.

The graph is therefore the primary object. Conventional typing fixes the types at its node interfaces; uniqueness attributes then constrain the number of references reaching those interfaces. A bounded overwrite becomes admissible only when those two facts meet at the rewritten node.

A term denotes a rooted graph

Let constructors and defined symbols have fixed arities. Expressions and constructor patterns are Patterns are left-linear. In a nonrecursive let, $x\notin \mathsf{FV}(E)$. Constructor symbols build data; defined symbols are roots of graph-rewrite rules. In the frozen translation, a case occurs only at the top of a function definition and scrutinizes one argument. Nested cases are expressed by auxiliary functions; there is no case-labelled graph node.

The denotation $[[E{]]}_{\mathsf{g}}$ is built compositionally: Here $[[E_i{]]}_{\mathsf{g}}=⟨r_i\mid G_i⟩$, the component node sets have first been made disjoint, and $r$ is fresh. A recursive let performs the indicated simultaneous root substitution $[\overrightarrow{x}:=\overrightarrow{r}]$. These clauses interpret case-free expressions. Alpha-renaming makes the displayed unions capture-free.

The distinction between copying syntax and sharing a root is now visible: $$\mathsf{let}x=C\mathsf{in}P(x,x)\text{⧸}{\simeq }_{\mathsf{g}}P(C,C).$$ The graph on the left has one $C$-node with two incoming edges; the graph on the right has two $C$-nodes.

A case-free function equation $f(\overrightarrow{x})=E$ induces a rule whose left interface is $f(\overrightarrow{x})$ and whose right graph is $[[E{]]}_{\mathsf{g}}$. A definition $f(x,\overrightarrow{y})=\mathsf{case}x\mathsf{of}\{P_i\mapsto E_i\}$ induces one rule with left interface $f(P_i,\overrightarrow{y})$ and right graph $[[E_i{]]}_{\mathsf{g}}$ per alternative. We write $g{⟶}_{\mathsf{g}}{g}^{\prime }$ for one such graph rewrite and ${⟶}_{\mathsf{g}}^{\ast }$ for its reflexive transitive closure. Expression reduction is not a second semantics: $$E{⟼}_{\mathsf{g}}{E}^{\prime }⟺[[E{]]}_{\mathsf{g}}{⟶}_{\mathsf{g}}[[E^{\prime }{]]}_{\mathsf{g}}.$$ The graph step on the right therefore determines reduction when sharing or cycles matter.

Conventional typing before uniqueness

Conventional types and symbol schemes are $$\sigma ,\tau ::=\alpha \mid T(\overrightarrow{\sigma })\mid \sigma \to \tau ,S:\overrightarrow{\sigma }\Rightarrow \tau .$$ A basis $B$ maps variables to types. Besides variable and symbol application, the expression rules provide sharing, simultaneous cycles, and pattern matching. The sharing rule is the representative one: $$\frac{B⊢E:\sigma B,x:\sigma ⊢E^{\prime }:\tau }{B⊢\mathsf{let}x=E\mathsf{in}{E}^{\prime }:\tau }\mathrm{Share}.$$ The cycle rule types all right-hand sides under the same assumptions for the recursive roots. In a case rule, constructor arguments extend the basis of the corresponding branch.

Proof of Proposition 47.4 — Term–graph soundness and completeness

Proof. For soundness, induct on the expression derivation. A symbol application adds one equation whose incident types are the selected scheme instance. Sharing identifies the variable node with the root of the bound expression; the two premises assign the same $\sigma$ to that interface. The cycle case performs all root identifications simultaneously. Pattern matching uses the constructor instance to type each fresh pattern variable.

For completeness, decompose the graph denotation by the outer expression constructor. Restrict its node assignment to the component graphs. At a shared or recursive interface the restrictions agree because they are restrictions of one assignment. The induction hypotheses therefore rebuild the corresponding source rule. ◻

Proof of Theorem 47.5 — Conventional subject reduction

Proof. By proposition 47.4, type $[[E{]]}_{\mathsf{g}}$. For a root rewrite, the declared type of a function rule makes its left and right interface assignments coincide; substituting the matched nodes therefore types the replacement graph at the old root type. An internal rewrite changes one equation subgraph and preserves the enclosing assignment. Transfer the result back to $E^{\prime }$ with completeness. ◻

Equation generation and the principal conventional type

Assign a fresh type variable to each expression occurrence and graph interface. A symbol occurrence contributes equations equating its incident variables with one fresh instance of its scheme. Sharing contributes an equality between the bound root and every occurrence of the bound variable; a cycle contributes the simultaneous interface equalities; a pattern contributes the constructor equations.

Proof of Lemma 47.7 — Exact equation generation

Proof. Induct on $E$. Each generated equation is precisely an interface equality in the corresponding typing rule. The only nonlocal-looking cases are sharing and cycles; graph-denotation construction identifies exactly those roots, so no additional equality is needed and none may be removed. ◻

Proof of Theorem 47.8 — Principal conventional typing

Proof. Existence and exactness are lemma 47.7. The factorization property is the most-general-unifier theorem applied to the finite first-order equation set. ◻

Attributes describe aliasing

Every node of a type carries one of two attributes: $$a::=\mathsf{u}\mid \mathsf{m},\mathsf{u}\le \mathsf{m}.$$ $\mathsf{u}$ promises a single incoming reference to the represented object. $\mathsf{m}$ makes no such promise. The order permits forgetting uniqueness, never manufacturing it.

For lists, a useful scheme is $$\mathsf{Cons}:({\alpha }^a,{\mathsf{List}}^b({\alpha }^a))\Rightarrow {\mathsf{List}}^b({\alpha }^a)\mid b\le a.$$ A unique spine can contain shared elements: taking $b=\mathsf{u}$ and $a=\mathsf{m}$ satisfies the inequality. The reverse choice would let a shared spine smuggle a unique element through duplication and is rejected.

The uniqueness judgment has the same surface shape $B⊢E:\sigma$, but its structural rules are controlled: $$\frac{B,y:[\sigma ],z:[\sigma ]⊢E:\tau }{B,x:\sigma ⊢E[y:=x,z:=x]:\tau }\mathrm{Contr}\frac{B⊢E:\sigma \sigma \le \tau }{B⊢E:\tau }\mathrm{Sub}.$$ Weakening discards an assumption. Context splitting in symbol application keeps unique assumptions in one premise; shared assumptions may be copied only through contraction after correction. The cycle rule corrects every recursive variable whose root acquires more than one incoming reference.

Proof of Lemma 47.11 — Contraction matches graph sharing

Proof. After substitution the two variable roots are one node with at least two incoming references. The graph condition therefore checks $[\sigma ]$, which is the type assigned to both $y$ and $z$ in the premise. Conversely, splitting the two edges gives the two corrected assumptions required by the premise. ◻

Proof of Theorem 47.12 — Uniqueness soundness and graph completeness

Proof. Soundness is induction on the attributed typing derivation. The structural case absent from conventional typing is lemma 47.11. Subsumption composes the local inequalities. Cycle correction accounts for incoming recursive edges.

Completeness cannot in general recover the same syntax, because one graph has many let presentations. Traverse a spanning presentation of the typed graph, insert a let at every node with multiple incoming references, and use contraction with its corrected type. Present strongly connected components by simultaneous $\mathsf{letrec}$. The reconstructed expression denotes the original graph and the local graph inequalities supply its rule premises. ◻

Proof of Theorem 47.13 — Uniqueness subject reduction

Proof. Transfer the source derivation to a graph typing by theorem 47.12. A well-typed graph-rewrite rule has the same attributed interface at its left and right roots. Substitution of the matched graph for pattern variables preserves every local reference condition; if the replacement increases a reference count, its rule typing has already corrected that interface. Context closure preserves the assignment. Graph completeness then returns a typed presentation $E^{″}$. It need not be the parser’s chosen $E^{\prime }$, which is why graph equivalence is part of the conclusion. ◻

Polymorphic attributes and the exact principal result

Replace concrete attributes by variables $a,b,\dots$, and attach a finite inequality environment $\mathrm{\Phi }$ to a symbol scheme. Its reflexive-transitive closure is consistent exactly when it does not derive $\mathsf{m}\le \mathsf{u}$. Typing generates ordinary type equations and attribute inequalities separately.

Proof of Lemma 47.15 — Effective closure

Proof. Regard inequalities as edges in a finite graph whose two constants are $\mathsf{u}$ and $\mathsf{m}$. Compute reachability. The problem is inconsistent exactly when reachability contains the forbidden edge $\mathsf{m}\le \mathsf{u}$. Otherwise the reachability relation is the least closed constraint environment. ◻

Proof of Theorem 47.16 — Principal attribution, relative to a conventional solution

Proof. Every rule contributes only inequalities between its fresh variables and constants. Closure adds exactly their logical consequences. Hence any solution of the generated constraints is a solution of the closure, while the identity symbolic assignment together with that closure is itself a solution. Instantiating its variables produces every concrete attribution. ◻

The qualifier “relative to a conventional solution” cannot be dropped.

Proof of Proposition 47.17 — No claimed global principal uniqueness type

Proof. The higher-order subtype restriction treats type variables differently from their later structured instances. Consequently the source exhibits a most general conventional solution whose lift fails while a proper instance lifts. Attributability therefore need not reflect backward from an instance to its generalization. The effective strategy that attributes only the principal conventional type is sound when it succeeds but may reject an expression whose conventional instance is attributable. ◻

What destructive update is licensed

An implementation may reuse a constructor node only when the redex interface types that node uniquely and the rewrite preserves its constructor layout. This is an update-eligibility theorem, not a semantics of arbitrary machine writes.

The first two conditions exclude hidden aliases; the last two bound what “in-place” means. Eligibility does not change the source rewrite relation. Because the graph denotation retains garbage equations, allocation and overwrite are compared below only at the reachable rewritten interface, not by the full relation ${\simeq }_{\mathsf{g}}$.

Proof of Theorem 47.19 — Eligible overwrite preserves the typed graph interface

Proof. There is one incoming reference, so redirection has no other observer. The layout condition makes the overwritten equation well formed, and the edge condition supplies exactly the local premises of definition 47.10. All equations outside the node are unchanged. Both implementations therefore have isomorphic reachable labelled graphs after forgetting physical node identities. ◻

In-situ quicksort.

The 1994 application represents a list segment by a unique spine, while its elements may remain shared. Partition consumes one spine cell at a time and relinks that cell onto one of two accumulator spines. Recursion sorts the two unique partitions; concatenation relinks their spines. No step needs to copy an element or mutate through a shared spine.

For example, after consuming $3::1::4::2::[]$ around pivot $3$, the old cells can be relinked into $1::2::[]$ and $4::[]$. The source result is the pure sorted list $1::2::3::4::[]$. The bounded criterion licenses physical node reuse; it does not identify full graph denotations that differ by retained garbage.

The provenance boundary.

The destructive-update and in-situ quicksort application comes from the 1994 system, which explicitly omits the preservation proof. The graph-semantic soundness and preservation results used here belong to the later 1996 Barendsen–Smetsers system. We use the later theorem only after translating the application’s update eligibility into its frozen graph interface; we do not transfer a theorem to an unspecified compiler or cost model.

Affinity now has a precise contrast. An affine variable may be used at most once syntactically. A unique graph node has one incoming reference semantically. Either property can be useful, but only the second proves the absence of a hidden alias needed by definition 47.18.

Frozen boundary and seminar problems

The proved core contains the selected graph-denotation language, conventional typing, attributed uniqueness typing, graph rewriting, principal conventional inference, and principal attribution relative to a fixed conventional solution. The quicksort application is bounded by definition 47.18. Arrays, concurrency, exceptions, foreign calls, allocator costs, and observational equivalence for a concrete compiler need additional semantics and proofs.

Suggested first pass.

Begin with exercise 47.1, exercise 47.2, exercise 47.4, exercise 47.6. Continue with exercise 47.7. The practical project is an optional second pass.

None of these problems is a prerequisite for a later chapter.

Exercise 47.7¶

★★★ Write the root-rewrite case of theorem 47.13 in full. Name the interface substitution, show how every increase in reference count invokes correction, and explain why the conclusion is graph-equivalent rather than syntactically identical to the reduct.

Referenced from 4 locations

• Uniqueness Types and Destructive Update
• ch:ownership-borrowing: ch:ownership-borrowing

Exercise 47.8¶

★★★ Design a two-phase inference procedure that first enumerates conventional instances and then solves attribute constraints. Prove soundness of each reported result. Explain why termination of an unrestricted enumeration does not follow from theorem 47.8.

Referenced from 3 locations

• Uniqueness Types and Destructive Update
• ch:ownership-borrowing: ch:ownership-borrowing

Exercise 47.9¶

★★★ Practical project.uniqueness-eligibility-checker Implement in Kappa the finite attribute preorder, a reference-count check, and the four conditions of definition 47.18. The observable corpus must accept one unique use, reject duplicated unique use, accept duplicated shared use, accept relinking a unique list spine, reject relinking a shared spine, and reject a constraint closure containing $\mathsf{m}\le \mathsf{u}$. Mutate the inequality direction in the $\mathsf{Cons}$ constraint; an inline oracle must fail. State why these executions do not prove theorem 47.13.

Referenced from 4 locations

• Uniqueness Types and Destructive Update
• Object calculus checker and evaluator
• ch:uniqueness-types: uniqueness eligibility

Sources.

The frozen graph language, conventional and uniqueness systems, and their metatheory are Definitions 3.1–3.7, Propositions 5.7–5.19, Theorem 5.20, and Theorems 7.13, 7.20, 7.23–7.24, 8.11–8.13, and 8.21 of Barendsen and Smetsers [BS96]. The destructive-update and in-situ-quicksort application is [SBvEP94]; its omitted preservation argument is not silently supplied by that paper. Later simplifications of uniqueness typing [dVPA08] are comparisons only and own no theorem stated in this chapter.