Acar, Blelloch & Harper (2002) -- Adaptive Functional Programming

Paper Summary

Acar, Blelloch, and Harper observe that many computations are run repeatedly on inputs that differ only slightly from one run to the next, yet conventional functional programs throw away the previous result and recompute from scratch. They define an adaptive computation as one that maintains the relationship between its input and output as the input changes (Abstract, p1; S1, p3), re-evaluating only the portions of the program actually affected by a change. When input changes produce small output changes, reusing the prior computation yields the new output far faster than full re-evaluation — the headline result is that an adaptive Quicksort updates its sorted output in expected O(log n) time when the input list is extended by one key, a linear-factor improvement over the O(n log n) re-sort (Abstract, p1; S1, p3; Theorem 2, S4.8, p12).

The proposed mechanism extends any purely-functional call-by-value language with a small set of primitives, built on the idea of a modifiable reference (or modifiable): a write-once reference cell that holds the value of an expression whose value may change as a direct or indirect result of input changes (S1, p3). An expression whose value can change is changeable and must store its value in a modifiable; an expression that cannot is stable and is not associated with any modifiable (S1, p3). Any expression that depends on a changeable value must express that dependence by explicitly reading the modifiable: this establishes a data dependency between the reader (the depending expression) and the writer (the expression that determines the modifiable’s value). Because what is read may change, a reader is itself changeable — changeability is contagious: once an aspect is made changeable, everything depending on it becomes changeable too (S1, p3; S4 intro, p4). The programmer controls the extent of adaptivity by choosing which data goes into modifiables (e.g. make only list “tails” changeable so the list adapts to insertions/deletions but not element edits) (S4 intro, p4).

The ML library (Figure 1, p6) is just five operations plus the changeable type and the 'a mod/'a dest source/destination split. mod : ('a*'a->bool) -> ('a dest -> changeable) -> 'a mod creates a modifiable, running an initializer in destination-passing style that must end by writing the new modifiable’s destination; it takes a conservative comparison function (returns false when values differ, may return either when equal) that change propagation later uses to suppress unnecessary work (S4.1, p6). read : 'a mod * ('a -> changeable) -> changeable accesses a modifiable’s contents and applies a reader; every read is itself changeable. write : 'a dest * 'a -> changeable stores a value in the target destination. Three meta-operations drive adaptivity (S4.1, p6; S4.3, p7): init resets the library, change : 'a mod * 'a -> unit overwrites an input modifiable’s value, and propagate : unit -> unit adapts the output to all changes made since the last propagate. Quicksort is made adaptive (Figure 2, p7) by two mechanical steps: (1) place the changeable parts of the data (here list tails) into modifiables, and (2) make every read explicit and route every dependent result into another modifiable (S4.2, p7).

The data structure that makes change propagation efficient is the augmented dependency graph (adg) (S4.4, p8): a DAG in which each node is a modifiable (created by mod) carrying a value and a time stamp, and each edge is a read (created by read) carrying the reader closure and a time stamp, directed from the source modifiable being read to the target modifiable the reader finishes by writing. A node with no incoming edge is an input (S4.4, p8). Beyond the raw read-to-write dependencies, two extra relations are essential (S1, p4): the evaluation order of reads, and the containment hierarchy — which reads occur within the dynamic scope of which other reads. Both are encoded with time stamps drawn from a totally-ordered range: each expression evaluates in a time range (ts, te) and allocates stamps sequentially within it; a read’s edge gets a start time (stamped before its reader runs) and the read’s target node gets the edge’s stop time, so the (start, stop) time span of an edge captures exactly the reads dynamically contained within it — read Ra is contained in Rb iff Ra’s start time falls inside Rb’s time span (S4.4, p8-9). Containment is what lets the algorithm find and delete reads rendered obsolete when a re-evaluated conditional takes a different branch (S1, p4).

The change-propagation algorithm (Figure 5, p10; S4.5, p9) is given an adg and a set of changed input modifiables. It maintains a priority queue of invalidated edges, prioritized by start time, seeded with the out-edges of every changed input. Each iteration deleteMins the earliest invalidated edge e (the “edge update”), reads off its time span (Ts, Te), deletes every node and edge whose stamp falls strictly within that span from both the graph and the queue (these are the obsolete reads contained in e, which must not be re-run — re-running an obsolete reader on changed input could wrongly write, wrongly raise, or diverge), then re-evaluates e’s reader in the recovered time span, splicing the freshly created reads/nodes back in. Finally it applies the conservative comparison: if the target’s value actually changed, the target’s out-edges are added to the queue so the change propagates onward (Figure 5 lines 9-12, p10; S4.5, p9-10). Processing in start-time order guarantees each reader re-runs in the same relative order as the initial evaluation and that the trace is traversed once (S4.5; S7, p29). The key efficiency move is that obsolete-edge deletion is done lazily in the ML implementation: an edge’s stamp is marked invalid (spliced out of the ordered list) and only physically removed when next encountered (isSplicedOut/spliceOut, Figure 7-8, p13-15; S4.9).

Efficiency rests on three standard data structures (S4.6, p11): adjacency-list adg with doubly-linked edge lists (constant-time edge/node insert, delete, find-outgoing), a time-ordered doubly-linked edge list, a logarithmic balanced-tree priority queue, and — crucially — an order-maintenance structure for the time stamps. Representing stamps as reals fails because arbitrarily many stamps may be inserted between two fixed ones; instead the Dietz-Sleator Order-Maintenance Algorithm (ref [4]) supports compare / insert-after / delete / find-next on stamps in (amortized or worst-case) constant time (S4.6, p11-12). The complexity result (Theorem 1, S4.7, p12) bounds a propagate step by O( Σ_{e∈Iu}(|e| + ||e||) + |I| log q ), where I is the set of invalidated edges, Iu ⊆ I those actually updated (the rest become obsolete and are deleted unrun), |e| is the reader re-evaluation cost, ||e|| the number of stamps created during e’s initial evaluation, and q the max priority-queue size — i.e. cost is proportional to the affected part of the computation, not the whole. The whole ML library is under 100 lines of Standard ML (S3, p5; S4.9, p13).

The second half of the paper establishes soundness formally. AFL is a small purely-functional call-by-value language with adaptivity primitives mod, read, write and implicit destination-passing (S5, p16; abstract syntax Figure 9, p17). AFL’s modal type system (inspired by Pfenning-Davies modal logic, ref [12]) splits expressions into two modes — stable (Λ;Γ ⊢s e:τ) and changeable (Λ;Γ ⊢c e:τ) — and adds two function arrows (stable →s, changeable →c) and the modifiable type τ mod (S5.1-5.2, p16-19; Figures 10-11). The static semantics statically enforces the four invariants that the ML library could only check at run time (S6, p21): (1) each modifiable is written exactly once; (2) no modifiable is read before written; (3) dependencies are never lost (anything depending on a modifiable is itself placed in a modifiable); (4) the store is acyclic. The dynamic semantics is a store-passing evaluation relation (Figures 12-13, p20-21) that, instead of an adg, emits a trace — a finite record of the adaptive structure (S5.3, p19). Traces have the grammar Ts ::= ε | <Tc>_{l:τ} | Ts;Ts (stable: modifiable allocations) and Tc ::= Wτ | R^{x.e}_l(Tc) | Ts;Tc (changeable: a write, a read recording location l, context x.e, and the nested sub-trace Tc of everything in that read’s scope, or a let-sequence) (S5.3, p19). The adg is explicitly “an efficient representation of traces”: left-to-right stamps recover the time order, and the containment hierarchy is directly the syntactic nesting of R^{x.e}_l(Tc) (S5.3, p20). Type safety is proved via type preservation (Theorem 6, S6.3, p24-27) plus canonical forms (Lemma 7, S6.4, p28); store typings carry a linear order on locations that guarantees acyclicity (S6.1, p22).

Finally the paper re-presents change propagation as a formal algorithm over traces and proves it correct (S7, p28-43). An input change is a difference store δ; modifying σ by δ is σ ⊕ δ (Definition 9, p28). The algorithm is two judgements — stable σ, Ts, C ⇓p_s σ', Ts', C' and changeable σ, l←Tc, C ⇓p_c σ', Tc', C' — carrying a changed set C of locations (Figure 15, p29). Each propagation rule mimics the AFL evaluation rule that originally produced that trace, so the trace is scanned exactly once in generation order (S7, p29). The decisive rule is read (Figure 15, p29; S7, p30): if the read location l ∈ C (changed), the read’s body is re-evaluated with the new value, yielding a revised sub-trace that “repairs”/splices the old one in place, and the read’s target is added to C so downstream reads will in turn re-evaluate; if l ∉ C, the read is skipped and propagation continues into the rest of the trace, because re-evaluation would reproduce identical store/trace effects already present. A purely-functional version scans the whole trace (O(trace size)), but replacing re-evaluated reads’ sub-traces in place (the adg approach) lets the rest be skipped (S7, p30). Change propagation also preserves typing (Theorem 10, S7.1, p30-32). Correctness (Theorem 18, S7.2, p42; via the generalized Change-Propagation Lemma 17, p35) states: initial evaluation followed by change propagation yields the same value, trace, and store as a complete from-scratch re-evaluation on the changed input — equal up to a partial bijection on locations B (since fresh location names need not coincide; locations are not user-visible) (Definition 11, p33; Figure 16, p32). The discussion (S8, p43) notes variants (implicit write; a fused modrw = mod(fn d => read x (fn x' => write(d,f x'))) insufficient for Quicksort), that the purely-functional requirement is really a persistence requirement on reader closures’ environments, that benign side effects (print/counters/lazy memoization) do not affect correctness, and that the motivating application is kinetic data structures in computational geometry (refs [2]).

Key Concepts

Adaptivity = maintain input→output under change (Abstract, p1; S1, p3). An adaptive program responds to input changes by updating its output while re-evaluating only the affected portions. Useful precisely when small input changes cause small output changes; in the limit it degrades to full recomputation.
Modifiable reference (S1, p3; S4.1, p6). A write-once cell holding the value of a possibly-changing expression. Two handles: a source 'a mod (read-only after write) and a destination 'a dest (write-only until written). Changeable expressions run in destination-passing style and must “end with a write” to their target.
Stable vs changeable (S1, p3; S5 modal types, p16). Stable = value insensitive to input changes (ordinary FP, not in a modifiable); changeable = value may be affected, must be stored in a modifiable, must be reached via explicit read. Changeability is contagious: any reader of a changeable value is itself changeable.
read/write/mod primitives (Figure 1, p6). mod cmp init allocates and initializes a modifiable; read src reader records a dependency and applies the reader; write dest v stores to the target. The conservative comparison cmp (false ⇒ definitely different) lets propagation cut off unchanged values.
Reader/writer dependency (S1, p3-4). A read creates a directed dependency from the modifiable read (source/writer) to the reader expression, whose own result lands in another modifiable (its target). Recording these dependencies during the initial run is what enables later adaptation.
Augmented Dependency Graph (adg) (S4.4, p8). A DAG: node = modifiable (value + time stamp), edge = read (reader closure + time stamp), directed source→target. Inputs = nodes with no in-edges. mod adds a node; read adds an edge.
Time stamps + evaluation order + containment hierarchy (S1, p4; S4.4, p8-9). Beyond who-depends-on-whom, the adg records (a) the order reads were evaluated and (b) which reads are dynamically nested inside which. Edge (start,stop) time span = the read’s scope; Ra contained in Rb ⇔ Ra.start ∈ Rb’s span. Order ⇒ re-evaluate in original order; containment ⇒ identify and delete obsolete reads.
Order-maintenance for stamps (S4.6, p11-12; Dietz-Sleator [4]). Stamps cannot be reals (unbounded insertions between two fixed stamps). The Order-Maintenance structure supports compare / insert-after / delete / find-next in (amortized or worst-case) constant time, giving constant-time stamp operations.
Change-propagation algorithm (Figure 5, p10; S4.5, p9-10). Priority queue of invalidated edges keyed by start time, seeded with changed inputs’ out-edges. Per edge update: delete the contained (obsolete) nodes/edges in its time span from graph and queue; re-evaluate the reader in that span (splicing in new reads); if the conservative comparison says the target changed, enqueue the target’s out-edges.
Obsolete-read deletion = splice (S4.5, p10; S4.9, p13-14). Reads contained within an updated edge are spliced out (their stamps marked invalid via spliceOut/isSplicedOut, lazily reclaimed). This prevents re-running readers whose dynamic scope no longer exists (a conditional took a different branch) — which could wrongly write, wrongly raise, or diverge.
Cost ∝ affected work (Theorem 1, S4.7, p12). O( Σ_{e∈Iu}(|e|+||e||) + |I| log q ): reader re-evaluation + stamp churn over updated edges Iu, plus log-factor queue maintenance over all invalidated edges I. Proportional to the change-affected subcomputation, not the whole program. Yields expected O(log n) adaptive Quicksort under one-key extension (Theorem 2, S4.8, p12).
AFL + modal type system (S5, p16; Figures 9-11, p17-19). A purely-functional CBV core with mod/read/write, implicit destination passing, modifiable type τ mod, and stable/changeable modes + arrows. Static typing enforces (at compile time) the four invariants the library checks at run time: write-once, read-after-write, no-lost-dependency, acyclic store (S6, p21).
Trace (S5.3, p19-20). The dynamic-semantics counterpart of the adg: Ts ::= ε | <Tc>_{l:τ} | Ts;Ts, Tc ::= Wτ | R^{x.e}_l(Tc) | Ts;Tc. A read trace R^{x.e}_l(Tc) records the location read, the use-context, and the syntactically nested sub-trace = its containment scope. The adg is “an efficient representation of traces.”
Formal change propagation over traces (Figure 15, p29; S7). Two judgements with a changed set C. Each rule mimics the evaluation rule that produced the trace (single scan, original order). Read rule: l∈C ⇒ re-evaluate, splice-repair the sub-trace, add target to C; l∉C ⇒ skip (effects already present).
Correctness up to partial bijection (Theorem 18, S7.2, p42; Lemma 17, p35; Definition 11, p33). Initial-eval-then-propagate produces the same value/trace/store as full re-evaluation on the changed input, modulo a partial bijection B on locations (location names are not user-visible). Change propagation also preserves store typing (Theorem 10, p30).
Purity = persistence of reader closures (S8, p43). The real requirement is not “no side effects” but that each edge’s stored reader closure (code + environment) cannot be mutated. Benign side effects (print, counters, lazy memoization) are harmless; the technique is expected to extend to lazy languages and to imperative settings with persistent data.

Implementation Mapping

Current Usage in Gen Ecosystem

gen-rebuild (Foundational — the formal model `override`/`restabilize` realize)

gen-rebuild is the rebuilder of the Mokhov framework — the component that decides what must be recomputed when an input changes and reuses everything else. Acar’s AFL is the canonical formal model for that decision: change propagation is the rebuild step expressed as an algorithm with a proof. The correspondence is direct:

adg / trace = gen-rebuild’s dependency record. Acar’s node = modifiable = a (key, value) entry in gen-rebuild’s flat relocatable store; Acar’s edge = read = a recorded dependency (source-key → consumer-key) tagged with the consumer’s re-eval closure. The store-plus-dependency-record that override operates over is the adg (S4.4, p8).
override = change propagation seeded from a changed input (Figure 5, p10). override recomputes the reverse-dependency cone of a changed key and reuses the rest. Acar grounds the cone exactly: it is the set of edges reachable by the queue starting from the changed input’s out-edges, walked in time order, with the conservative-comparison early-cutoff pruning branches whose value did not actually change (Figure 5 lines 10-12). The “reuse rest from a flat store” is Acar’s “skip reads not in the changed set” (S7 read rule, l∉C, p30).
override’s splice semantics = obsolete-edge deletion + reader re-eval (S4.5, p10; S7 read rule, p30). When a recomputed node takes a different control path, the reads dynamically contained in it become obsolete and are spliced out before the new sub-computation is spliced in. This is the precise semantics of replacing one node’s reverse-cone subtree: not “recompute the whole cone” but “delete the contained sub-trace, re-run the reader, graft the fresh sub-trace.” gen-rebuild’s override currently cites this only indirectly (via Mokhov S7.2); Acar S4.5 + S7 is its direct ground.
restabilize = propagate to a fixed point (S4.3 propagate, p7; S7). restabilize runs incremental recomputation until the system is consistent again. Acar’s propagate is exactly that driver: drain the priority queue, where each target whose value changed re-enqueues its out-edges, terminating when the queue empties (quiescence = re-stabilized). The “incremental fixpoint” is the queue-drain of Figure 5.
dirtySet minimality = invalidated set I / updated set Iu (Theorem 1, S4.7, p12). Acar formally distinguishes I (invalidated edges, enqueued) from Iu ⊆ I (edges actually updated; the rest go obsolete and are deleted unrun). gen-rebuild’s dirtySet minimality claim is grounded by this distinction and by the cost bound O(Σ_{Iu}(|e|+||e||)+|I|log q): the minimal dirty set is the affected reverse-cone, minus obsolete reads, minus branches cut off by the conservative comparison. Acar is the proof that this set is both necessary (Theorem 18 correctness) and sufficient (Theorem 1 cost).
earlyCutoff = conservative comparison function (S4.1 cmp, p6; Figure 5 line 10, p10). The Mokhov-named “early cutoff” rebuilder strategy is, in Acar’s model, the cmp passed to mod: after re-evaluating a reader, if cmp(new,old) says unchanged, the target’s out-edges are not enqueued, so propagation stops. gen-rebuild’s earlyCutoff is this branch verbatim.
support / why / affected provenance = adg reachability queries. affected = the set of edges reached from a changed input (the seed-and-walk of Figure 5) = forward reachability in the adg. support/why = the in-edges/source modifiables a value’s edge depends on = backward reachability. Acar’s adg is the provenance graph these three queries read.
verify / constructive / deepConstructive are Mokhov-domain strategies (trace verification vs value-storing) not directly in Acar’s scope; Acar contributes the change-propagation axis (suspending-scheduler-driven re-execution), which is orthogonal and complementary to the trace-storage axis.

gen-scope (Seam provider — the scheduler Acar’s algorithm assumes)

Acar’s change-propagation algorithm is driven by an evaluator that re-runs readers; in gen-rebuild that evaluator is gen-scope (demand-driven HOAG eval with co-located _eval memo). The five named seams map onto Acar’s machinery:

S1 warm-cache eval = re-running a reader against the post-change store (Figure 5 line 9, “apply(reader(e), val(src(e)))”); the _eval memo is Acar’s already-computed node values reused across the unaffected store.
S2 dep-recording = adg edge creation: every read records a (source → consumer) edge tagged with the reader closure (S4.4, p8). This is the seam Acar leans on hardest — without dep-recording there is no adg to propagate over.
S3 frontier dependents = outEdges(v) (Figure 5 lines 1, 12): the out-edges of a changed/updated node, i.e. the propagation frontier.
S4 seeded fixpoint = the priority-queue drain seeded with changed inputs (Figure 5 lines 1-2) = restabilize’s engine.
S5 hashOf hook = the conservative comparison cmp (S4.1, p6) used to decide whether a recomputed target actually changed (early cutoff). Acar’s cmp is value equality up to a sound under-approximation; hashOf is the natural Nix realization.

gen-graph (Seam provider — the adg as a queryable graph)

Acar’s adg is literally a DAG with typed nodes (modifiables) and typed edges (reads). gen-graph provides the reachability queries (dependents, reverse-cone, time-span containment) that affected/support/why are built from. Acar adds one structural requirement beyond plain reachability: edge ordering + containment spans (S4.4, p8-9) — the adg is not just a DAG but a time-stamped DAG, and the containment hierarchy (an edge’s span vs another edge’s start) is a second relation layered on the reachability relation.

Appendix: Follow-up Work

Unexploited Ideas

Order maintenance as an explicit time-stamp service (S4.6, p11-12; Dietz-Sleator [4]). Acar’s efficiency hinges on a totally-ordered, dynamically-insertable stamp domain with constant-time compare/insert/delete/find-next. gen-rebuild currently has no notion of evaluation order among recomputations — only the reverse-dependency cone. For change propagation that must re-run readers in original order (to keep splice points valid), an order-maintenance structure (or its Nix-feasible surrogate: a monotone integer rank assigned during S2 dep-recording) is the missing primitive.
Containment-aware invalidation, not just cone invalidation (S4.5, p9-10; S5.3 nested traces, p20). Acar’s deletion step removes the reads dynamically contained in an updated read — a strictly smaller, more precise set than “everything in the reverse cone.” gen-rebuild’s dirtySet could be sharpened from “reverse-dependency cone” to “reverse cone minus obsolete-contained sub-traces,” which is the difference between |I| and |Iu| in Theorem 1. This is the formal route to a minimal dirty set.
Correctness-up-to-bijection as the gen-rebuild equational spec (Theorem 18, p42). Acar’s correctness statement — propagate ≡ full re-eval, up to a partial bijection on locations — is exactly the property gen-rebuild’s override/restabilize should satisfy: an incremental rebuild equals a from-scratch build, up to renaming of internally-generated keys. This gives gen-rebuild a precise, provable contract rather than an operational description.

Potential New Libraries or Features

gen-rebuild read/write/mod modifiable layer. The 13-op surface manipulates a store of already-computed values but has no constructor vocabulary for the dependency-bearing cells themselves. Acar’s mod/read/write are the minimal primitives that build the adg in the first place (S4.1, p6). gen-rebuild may need an explicit modifiable/read/write seam (even if thin over gen-scope’s _eval) to make dependency recording (S2) a first-class, inspectable operation rather than an implicit byproduct.
propagate as an explicit driver op distinct from override. Acar separates change (mutate an input, S4.3 p7) from propagate (drive the queue to quiescence). gen-rebuild’s applyDelta/batch/override conflate input mutation with propagation. A standalone propagate/restabilize driver — “given a set of changed keys, drain the frontier to a fixed point” — matches Acar’s factoring and makes batched changes (multiple changes before one propagate, S4.3 p7) natural.

Research Directions

Lazy-language adaptivity (S8, p44). Acar conjectures the mechanism extends to lazy languages and that lazy memoization is harmless to change-propagation correctness. gen-rebuild lives in Nix (lazy, persistent) — precisely the setting Acar flags as expected-to-work-but-unexplored. The open question: does Nix’s native thunk memoization subsume Acar’s _eval/node-value reuse, or must dependency order (S4.6) be tracked explicitly on top of it?
Splice granularity for Nix-embedded adgs. Acar splices at the read (edge) granularity. In a Nix-embedded rebuilder the natural unit is a (nodeId, attr) key. Characterizing the right splice granularity — per-read, per-attribute, per-node, per-subtree — for the cost bound of Theorem 1 to hold over a lazy store is open, and mirrors the trace-granularity question raised for verifying traces in the Mokhov summary.
Eliminating obsolete re-execution without static containment. Acar prevents re-running obsolete readers via the syntactic containment of R^{x.e}_l(Tc) traces (S5.3, p20) — it knows statically which reads are nested. A demand-driven Nix rebuilder records dependencies dynamically and may lack this nesting. Recovering containment (so obsolete sub-computations are not wrongly re-run) from a flat dynamic dependency log is a concrete research problem for gen-rebuild.

Palettes adapted from Catppuccin (Macchiato) (MIT), Tokyo Night (Apache-2.0), gruvbox (MIT), Catppuccin (Latte) (MIT), Rosé Pine (Dawn) (MIT).