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.

How gen uses this

gen-memo

gen-memo is gen’s incremental plane: given the last evaluation, it decides which keys must be recomputed and reuses the rest. Acar’s AFL is the formal model for that decision. Change propagation is the rebuild step expressed as an algorithm with a proof.

The adg is gen-memo’s dependency record. Acar’s node (a modifiable) is a key and its value in gen-memo’s store. Acar’s edge (a read) is a recorded dependency from a producer key to a consumer key, read through the caller’s accessor (S4.4, p8).
applyDelta and propagate are Acar’s change and propagate (S4.3, p7). gen-memo keeps the two apart the way the paper does. applyDelta records an input change and marks it dirty. propagate drains the dirty set to quiescence over the dependency cone. Several applyDelta calls before one propagate is Acar’s batched change. override is the fused convenience, propagate ∘ applyDelta. force demands a value after a change.
retract uses Acar’s splice-out (S4.5, p10). When a node is deleted, the reads it contained become obsolete and are removed before its dependent cone is recomputed.
earlyCutoff is the conservative comparison cmp (S4.1, p6; Figure 5 line 10, p10). After a reader is re-run, an unchanged result does not enqueue its out-edges, so propagation stops there. gen-memo compares content hashes produced by the caller’s hashOf.
dirtySet and Theorem 1 (S4.7, p12). Acar separates the invalidated edges I from the edges actually updated, Iu ⊆ I. The cost bound O(Σ_{Iu}(|e|+||e||)+|I|log q) says why a smaller dirty set pays: branches cut off by the comparison and obsolete reads are never re-run.
affected, support and why are adg reachability queries. affected is forward reachability from a changed input, the seed-and-walk of Figure 5. support and why read backward, from a value to the inputs it depends on.
verify and needsEval are trace strategies from Mokhov 2018 and Reps, Teitelbaum and Demers 1983. They sit on the trace-storage axis, which is outside Acar’s scope. Acar contributes the change-propagation axis, and the two combine.

restabilize is the cyclic counterpart of override. It re-solves strongly connected components to a fixed point, which Acar’s acyclic setting does not cover.

gen-graph

Acar’s adg is a DAG with typed nodes (modifiables) and typed edges (reads). gen-graph supplies the reachability gen-memo reads it through, such as dependentsOf for the reverse cone. Acar adds one requirement beyond plain reachability: edge ordering and containment spans (S4.4, p8-9). The adg is a time-stamped DAG, and containment (one edge’s span holding another edge’s start) is a second relation layered on reachability.

Appendix: Follow-up Work

Unexploited Ideas

Order maintenance as an explicit time-stamp service (S4.6, p11-12; Dietz-Sleator [4]). Acar’s efficiency depends on a totally ordered, dynamically insertable stamp domain with constant-time compare, insert, delete and find-next. gen-memo has no order among recomputations, only the reverse-dependency cone. Change propagation that re-runs readers in their original order, to keep splice points valid, needs an order-maintenance structure. In Nix a monotone integer rank assigned when dependencies are recorded is the feasible surrogate.
Containment-aware invalidation (S4.5, p9-10; S5.3 nested traces, p20). Acar’s deletion step removes the reads dynamically contained in an updated read, a smaller and more precise set than the whole reverse cone. gen-memo’s dirtySet could narrow from the reverse cone to the reverse cone minus obsolete contained sub-traces. That is the difference between |I| and |Iu| in Theorem 1, and the formal route to a minimal dirty set.
Correctness up to bijection as an equational spec (Theorem 18, p42). Acar proves propagation equals full re-evaluation, up to a partial bijection on locations. gen-memo’s contract is byte parity with a cold run, which is the same statement with the bijection fixed to the identity. Keys that gen-memo generated internally would need the bijection form.

Potential New Libraries or Features

A modifiable layer: mod, read, write. gen-memo operates on a store of computed values and a caller-supplied accessor. It has no constructor vocabulary for the dependency-bearing cells themselves. Acar’s mod, read and write build the adg in the first place (S4.1, p6). A thin modifiable layer would make dependency recording a first-class, inspectable operation.

Research Directions

Lazy-language adaptivity (S8, p44). Acar conjectures the mechanism extends to lazy languages and that lazy memoization does not harm change-propagation correctness. gen-memo runs in Nix, a lazy language with persistent values, which is the setting Acar flags as expected to work and unexplored. The open question is whether Nix’s thunk memoization subsumes Acar’s node-value reuse, or whether dependency order (S4.6) must be tracked on top of it.
Splice granularity. Acar splices at the read (edge) granularity. In a Nix rebuilder the natural unit is a (node, attribute) key. Which granularity makes the cost bound of Theorem 1 hold over a lazy store, per read, per attribute, per node or per subtree, is open.
Recovering containment from a dynamic log. Acar avoids re-running obsolete readers through the syntactic containment of R^{x.e}_l(Tc) traces (S5.3, p20). A demand-driven Nix rebuilder records dependencies dynamically and has no such nesting. Recovering containment from a flat dependency log is a concrete research problem.

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