Hammer, Phang, Hicks & Foster (2014) -- Adapton: Composable, Demand-Driven Incremental Computation

Paper Summary

Hammer et al. observe that prior incremental computation (IC), a.k.a. self-adjusting computation, has two crippling drawbacks (S1, p.1). First, recomputation is oblivious to demand: when an input changes, all dependent values are recomputed eagerly, even outputs no observer currently wants. Second, computations are incrementalized as a monolithic unit with little reuse across contexts — because traditional IC imposes a total ordering on its execution trace (typically via the Dietz-Sleator order-maintenance structure [9,15]), three common reuse patterns are impossible: sharing (the same subcomputation F(A1..A100) appears in two cells — traditional IC recomputes the second), swapping (reordering F(A)+F(B) to F(B)*F(A) forces recomputation due to total ordering), and switching (toggling F(A1..A50) to F(A51..A100) and back recomputes from scratch). The motivating example is a spreadsheet where cells are changed, hidden, and shown (S1, p.1; S2, pp.2-3).

The paper’s answer is a core calculus λcdd_ic and its OCaml realization, Adapton. The key insight (S1, p.1) is to combine traditional IC-style reuse with the memoization of thunks from lazy computation. Updates to mutable ref cells merely signal the potential need for recomputation; the actual recomputation is delayed until a thunk reading those cells is forced. Under the hood, both refs and thunks are implemented over a Demanded Computation Graph (DCG), which captures the partial order of which computation’s results feed which other computations — as opposed to the total order of prior IC. This partial order is what enables sharing, swapping, and switching.

Adapton’s second core idea is an explicit inner/outer layer separation (S1-S3), which the authors claim is absent from all prior IC. Inner computations — the bodies of thunks, the incrementally-reused units — may read refs (get) but may neither allocate nor mutate them. Outer computations — the interactive top level, the observer — may allocate refs (ref), mutate them (set), and force thunks, thereby precipitating change propagation. The restriction that inner computations are read-only is precisely what makes them safe to memoize and reuse. Layer purity is enforced in λcdd_ic by the type system (rules Ty-E-Ref, Ty-E-Set are outer-only; Ty-E-Get is layer-polymorphic; Ty-E-Inner coerces an inner computation into an outer context but not vice-versa, and |Γ| strips the outer layer’s recursive functions from the inner layer — Fig 3, p.5). In the OCaml library the layer separation is not statically enforced (OCaml’s types make it hard): an inner computation “implicitly begins when force is called and ends when the call returns” (footnote 1, p.7).

The DCG is the central data structure (S2, pp.2-3; S5.2, pp.7-8). Each node is a ref (drawn as a square, holds an address + content) or a thunk (drawn as a circle, holds a suspended expression and, once forced, its valuation). Each directed edge points from a thunk to a ref or thunk it depends on: edges targeting refs come from get, edges targeting thunks come from force. Edges are labeled with the value returned by that get/force call — this label is the early-cutoff witness. Edges are stored bidirectionally: each node keeps an ordered list of outgoing edges (appended in get/force order — leftmost created first) and an unordered set of incoming edges, so the graph can be walked caller→callee or callee→caller. The DCG starts empty; nodes are added on aref/athunk/memo-miss; edges are added on get/force during evaluation.

The heart of the algorithm is the two-phase split of change propagation into dirtying and propagation (S2, p.3; S5.2, pp.7-8; Algorithm 1, Fig 8 + the box on p.7). Dirtying runs on set: starting from the mutated ref, traverse incoming edges backward (caller-ward), marking each traversed edge dirty; stop at any edge already dirty (dirty(node): for each incoming edge, if not already dirty, set dirty and recurse to edge.source). This is eager but cheap — it only flips flags, it does not recompute. Propagation/cleaning runs on force: starting from the forced thunk, do an in-order traversal of its outgoing edges (in the order they were added, line 7). For each dirty edge: clean the flag (line 9); if the target is a thunk, recursively propagate into it (lines 10-11); then compare the edge’s stored label against the target’s current value (line 12 — this is the early-cutoff check). If the label still matches, the dependency is unchanged and the subgraph is cut off (not recomputed). If it differs, at least one input changed, so clear all the node’s outgoing edges (line 13) and re-evaluate the thunk (line 14), returning immediately (line 15) since the remaining edges will be rebuilt during re-evaluation. Crucially, propagation traverses bottom-up, left-to-right, in original evaluation/demand order, so it lazily repairs only the parts of the graph currently under demand — a thunk whose result no observer forces is never repaired (the line-6 example does not recompute t2, S2 p.3).

The two phases maintain a key invariant (S5.2, p.8) that amortizes their cost: if an edge is dirty at the end of a dirtying/propagation phase, every edge transitively reachable via incoming edges from its source is also dirty; dually, if an edge is clean, every edge transitively reachable via outgoing edges from its target is also clean. This lets dirtying stop early at already-dirty edges and propagation skip already-clean subgraphs, amortizing dirtying across consecutive sets and propagation across consecutive forces.

Formally (S3-S4), λcdd_ic extends Levy’s call-by-push-value [27,28] — which already has explicit thunk/force and syntactically separates values from computations — with ref/get/set and the inner/outer layer annotations. The incremental semantics (S4, Fig 4, p.5) reduces expressions to demanded computation traces (DCTs) rather than values: judgment K; S1 ⊢ e ⇓ S2; T reads “under prior knowledge K and store S1, e reduces to store S2 and trace T”. Trace events (Fig 6, p.4) are get^a_v (read address a yielding v) and force^e_ẽ[T] (forced thunk expression e, its terminal ẽ, and the sub-trace T). Traces are hierarchical trees — locally consistent, with no global ordering — which is exactly what permits compositional reuse. DCTs are trees; DCGs are graphs (S4.1, p.6): a shared subgraph in the DCG appears as a duplicated subtree in the DCT, so the DCT is easier to reason about but doesn’t explicitly represent sharing. Change propagation K; S ⊢ T1 ↝prop T2 is specified declaratively by checking + patching: the checking judgment S ⊢ √T verifies a trace is consistent with the store (Check-Force: the recorded terminal ẽ still matches trm(T); Check-Get: S(a)=v still holds), and the patching judgment T1{e:T2} ↝patch T3 substitutes a fresh sub-trace for all occurrences of a forced expression e “all at once”, simulating DCG sharing (p.6). Rule Incr-ForceProp performs memoization at force by non-deterministically choosing a prior trace of the same expression e from K and repairing it; importantly, change propagation is NOT initiated at set — it is delayed until the result is demanded by a force (p.6). The semantics are proved sound: every incremental reduction has a corresponding from-scratch reduction with the same terminal, so patched results equal what recomputation from scratch would produce (Thm 4.1 blind-evaluation equivalence, Thm 4.2 subject reduction, Thm 4.3 soundness, p.6).

The named/keyed-allocation and GC concerns surface in two places. Memoization (S5.1, pp.7-8): λcdd_ic memoizes implicitly at force by syntactic equality of expressions, which OCaml cannot do. So the library exposes memo, a constructor of memoized thunks keyed by argument: memo takes a 2-argument function and returns a constructor that, on each call, checks a memo table keyed by the argument — on a miss it allocates a fresh athunk and stores it; on a hit it returns the same athunk (equivalent to choosing the most-recently-patched trace in Incr-ForceProp). Memo tables are weak hash tables, relying on OCaml’s GC to evict athunks that are no longer reachable. Garbage collection of stale graph structure (S5.2, p.8): when a thunk is re-evaluated, its outgoing edges are cleared (line 13) and only relevant ones re-added; the incoming edge sets are stored in weak hash tables so OCaml’s GC removes now-irrelevant edges automatically. The paper explicitly notes (S6.1, p.9) the open problem that mergesort’s limited inter-recursion memoization caused trouble for both Adapton and EagerTotalOrder, and that prior work patched it with adaptive memoization [3] or keyed allocation [17] — a named-allocation discipline they cite as future work, not yet integrated.

Empirically (S6, pp.8-10; Table 1, p.9), Adapton is compared against EagerTotalOrder (traditional totally-ordered monolithic IC, [2]) and LazyNonInc (plain lazy values, no incrementality, set throws) across filter/map/quicksort/mergesort/fold/exptree under four change patterns: lazy (demand one output element), swap, switch, batch (demand entire output). Where traditional IC gets 2×-20× speedups over naive recomputation, Adapton gets 7×-2000×; for mergesort, EagerTotalOrder slows down 6.5× while Adapton speeds up 300×. Adapton wins decisively on the lazy/swap/switch patterns (it can memo-match regardless of total order; e.g. updown1, which EagerTotalOrder cannot memo-match at all). Adapton’s weakness is the batch pattern (all output demanded): it is 1.5×-3.5× slower than EagerTotalOrder, because EagerTotalOrder is optimized to propagate to all outputs unconditionally whereas Adapton’s conditional/demand-checking adds overhead — though it still beats naive. The dirtying cost is observed to grow with demand size (more output demanded → more edges cleaned by propagation → more edges to re-dirty). The case study AS2 (Adapton SpreadSheet, S6.2, pp.9-10) incrementalizes a stateless formula-evaluation spec and gets up to 20× speedups where classic IC always slowed down (up to 100×), with Adapton’s benefit growing exponentially in #sheets and #changes, validating that the sharing pattern is the decisive factor.

Related work (S7) positions Adapton against self-adjusting computation (Acar et al. [2,4]) which uses dynamic dependency graphs (DDGs) but assumes a single totally-ordered trace and ignores the outer layer; non-monotonic IC (Ley-Wild et al. [29,31]) which handles swapping but not sharing/switching, has no laziness, and was never implemented; and FRP [13,14,26] whose dependence DAGs resemble the DCG but reevaluate eagerly (push-based, topological) with no explicit outer-layer demand.

Key Concepts

Demanded Computation Graph (DCG) (S2 p.2-3; S5.2 p.7-8). Acyclic graph; nodes = aref (square: address + content) or athunk (circle: suspended expr + cached valuation); directed edges = a thunk’s dependency on a ref (via get) or thunk (via force), labeled with the returned value. Edges stored bidirectionally: ordered outgoing list (get/force order) + unordered incoming set (weak). The graph is the trace; it grows by demand and is repaired by demand.
Demand-driven vs. eager IC (S1 p.1; S2 p.3; S7). Traditional/self-adjusting IC propagates every change to all dependents at set time (eager, push, topological). Adapton makes set only signal change (dirty flags) and defers recomputation to force time (lazy, pull, demand-ordered). Undemanded outputs are never recomputed.
Inner/outer layer separation (S1, S3, Fig 3 p.5). Inner = thunk bodies, read-only on the store (get only), incrementally reusable. Outer = observer/top-level, may ref/set/force, precipitates change propagation. Type system enforces purity (ref/set are outer-only; inner e coerces inner→outer, not the reverse; |Γ| hides outer recursion from inner). Library does not enforce statically — inner begins at force, ends at return (fn.1 p.7). Claimed novel vs. all prior IC.
Dirtying (S2 p.3; Alg 1 lines 1-5). On set a, walk incoming edges backward from a, marking edges dirty, stopping at already-dirty edges. Eager, flag-only, no recomputation. Invariant: dirty edge ⟹ all incoming-reachable edges from its source are dirty.
Cleaning / propagation / repair (S2 p.3; Alg 1 lines 6-15). On force, in-order traverse outgoing edges; clean each dirty flag; recurse into thunk targets; compare stored edge label vs. current target value (early cutoff). Match ⟹ cut off (reuse). Mismatch ⟹ clear outgoing edges + re-evaluate thunk. Bottom-up, left-to-right, original demand order ⟹ lazy, only repairs demanded subgraph. Invariant: clean edge ⟹ all outgoing-reachable edges from its target are clean.
Memoization composed with change propagation (S4.1 Incr-ForceProp p.6; S5.1 p.7-8). Memo-match at force: reuse a prior trace of the same expression, then repair it via change propagation (check + patch). Patching replaces all occurrences of a forced expr “all at once” = DCG sharing. Library memo keys on argument (syntactic eq impossible in OCaml), returns the same athunk on a hit.
DCT (trace) vs. DCG (graph) (S4 p.4-6). Incremental semantics reduces to hierarchical demanded computation traces (trees of get^a_v and force^e_ẽ[T] events, locally consistent, no global order). DCTs are trees; DCGs are graphs — a shared DCG subgraph = a duplicated DCT subtree. Trees are easier to reason about formally; graphs capture sharing operationally.
Sharing / swapping / switching (S1 p.1; S2 p.2-3). The three reuse patterns traditional (totally-ordered) IC cannot do. Sharing: reuse a subcomputation across contexts. Swapping: reorder subcomputations. Switching: toggle between alternatives and reuse the inactive one. The DCG’s partial order supports all three; the total-order trace of prior IC supports none.
GC of unreachable nodes/edges (S5.1, S5.2 p.7-8). Memo tables and incoming-edge sets are weak hash tables; OCaml’s GC evicts athunks/edges that become unreachable (e.g. after a thunk re-evaluation clears + rebuilds its outgoing edges, the orphaned incoming edges are collected). Keyed/adaptive allocation [3,17] for better reuse (e.g. mergesort) is cited as future work, not integrated.
Soundness (Thms 4.1-4.3, p.6). Incremental (trace-based) reduction is consistent with from-scratch reduction: patched results equal full-recomputation results. Blind-evaluation equivalence + subject reduction + soundness.
Call-by-push-value foundation (S3 p.3-4). λcdd_ic = Levy’s CBPV [27,28] (explicit thunk/force, values vs. computations syntactically split, explicit evaluation order) + ref/get/set + inner/outer layers. CBPV chosen as “canonical” since both CBV and CBN translate into it.

How gen uses this

gen-memo

gen-memo is the rebuilder of Mokhov 2018: it decides whether a key needs recomputation over a dependency graph. Mokhov’s rebuilders answer “given a key, is its cached value still valid?” and assume a scheduler has already chosen to visit the key. Adapton supplies the demand-driven half, where set only marks change and recomputation waits until a force demands a result.

gen-memo takes Adapton’s split between change and demand, with dirtiness held as a value instead of a mutated flag.

applyDelta is Adapton’s set (Alg. 1 lines 1-5). It rewrites the changed key’s data, appends the key to the context’s pending dirty list and recomputes nothing. The store and trace stay out of date until the change is propagated. batch folds several deltas before one propagation.
force is Adapton’s demand entry point (S2, S5.2). On a quiescent context it reads the value. On a context with pending changes it drains them and then reads. forceCtx returns the drained context for reuse. propagate performs the drain directly.
earlyCutoff is the stored-value comparison (Alg. 1 line 12). After a key is recomputed, an unchanged hash stops propagation past it. gen-memo compares a node’s output hash, where Adapton compares the value stored on each edge.
dirtySet and affected compute the reverse-dependency cone of changed keys, the region Adapton’s dirtying walk marks.

gen-memo’s force drains the whole dirty cone. Adapton’s clean walks only the path the forced result depends on, in its original demand order, with a cutoff at every edge. Selective per-edge repair needs dirty flags that persist between interactions and an order among recomputations, which a single pure Nix evaluation cannot hold. propagateEager narrows the work on localised edits, and total work stays at least proportional to the cone.

gen-scope

Adapton’s force corresponds to gen-scope’s demand-driven evaluation, and Adapton’s memo to gen-scope’s memoisation on each node’s _eval attrset. The suspending scheduler Mokhov attributes to Nix’s lazy evaluation is how an Adapton force brings dependencies up to date before resuming. A demand on a node attribute is a force, and a read of another node’s attribute through get is a dependency edge. Nix has no weak references, so memoised values are not evicted within one evaluation.

gen-graph

Adapton stores edges in both directions: an ordered outgoing list for propagation and an incoming set for dirtying. gen-graph answers both directions. Dirtying corresponds to reverse reachability (dependentsOf), and propagation to a forward dependency walk.

Correspondence

Adapton concept	gen realisation
DCG (S2, S5.2)	The dependency graph gen-memo decides over, read through a caller-supplied accessor: keys as nodes, recorded dependencies as edges
`set` and dirtying (Alg. 1 lines 1-5)	`applyDelta`: record the change as pending, recompute nothing
`force` and propagation (Alg. 1 lines 6-15)	`force` and `propagate`: drain the pending cone with early cutoff (whole cone, not per edge)
Edge-label compare (line 12)	`earlyCutoff`, per output hash
`memo` (S5.1)	gen-scope’s `_eval` memoisation
Weak-table GC (S5.1-5.2)	No counterpart within a pure evaluation
Inner and outer layers (S1, S3)	Node equations are inner and read only. `applyDelta`, `override` and `retract` are outer operations
Soundness (Thm. 4.3)	gen-memo’s contract: the incremental result is byte-identical to a cold run

The paper’s lesson for gen is that demand-driven rebuilding is more general than eager cone recomputation. It comes from separating invalidation from revalidation and from checking value equality at each edge during the demand-ordered walk. gen-memo has the first separation. The second needs state across evaluations.

Appendix: Follow-up Work

Unexploited Ideas

Per-dependency early cutoff through edge labels (Alg. 1 line 12). earlyCutoff compares a node’s output hash. Adapton stores the returned value on each edge and cuts off when the label still matches the target’s current value, which prunes per dependency. Label-bearing edges would let revalidation prune subtrees mid-walk.
Sharing, swapping and switching as a reuse benchmark (S1, S2, S6). The three patterns totally ordered incremental computation cannot handle make a conformance test for a demand-driven rebuilder: reuse a subcomputation across contexts (sharing), tolerate reordered dependencies (swapping) and restore an inactive prior result (switching). gen-memo’s store should give sharing. Swapping and switching test whether the rebuilder works over a partial order.
Weak-table GC of undemanded entries (S5.1, S5.2 p.8). Adapton evicts unreachable thunks and edges through OCaml weak hash tables. Pure Nix has no weak references and no reachability hook within an evaluation, so this is the least natively expressible idea (see Research Directions).

Potential New Libraries or Features

Selective clean. A demand-ordered repair of only the path to one key, with cutoff at every edge, as the lazy counterpart to propagate. The store would need per-edge dirty flags and value labels, which in pure Nix must be re-derived each evaluation from a serialised trace of the previous run.
Keyed allocation (S5.1 p.7-8; [17]). Adapton’s memo keys thunk allocation by argument, and its absence hurt mergesort. An allocation keyed by a stable identity would keep node identity across runs so reuse survives structural change. This is the prerequisite for swapping and switching and the fix the paper cites as future work [3,17].

Research Directions

Can dirtying be expressed in pure Nix? (S5.2 p.7-8). Adapton’s dirty flags are mutable per-edge state, set by set and cleared by force across observer interactions, with an invariant maintained between phases. A single Nix evaluation has no mutation and no “between interactions”. Two options remain. The first re-derives dirtiness in each evaluation by diffing a serialised trace of the prior run against the new inputs, which keeps purity and cannot amortise dirtying across several sets. gen-memo’s pending dirty list is this option within one evaluation. The second persists the DCG outside the evaluation, in a file the harness reads and writes between nix eval runs, which recovers incrementality across runs and is impure at the harness layer.
GC without weak references (S5.1, S5.2 p.8). Adapton’s gc needs weak hash tables and a tracing collector. Within one Nix evaluation, laziness already drops unforced thunks. GC is meaningful only for an externally persisted trace: evict entries unreachable from any key demanded in the latest run, a pure reachability computation the harness runs between evaluations.
The inner and outer layers as a static discipline (S3, Fig. 3 p.5). Adapton’s split between read-only inner code and mutating outer code maps onto gen: node equations only read other attributes, and gen-memo’s delta operations are the outer layer. OCaml Adapton could not enforce the split statically (fn. 1 p.7). Nix’s purity enforces the read-only inner half already.
Trace granularity (S4 p.4-6; cf. Mokhov S4.2.2). Adapton’s DCT is hierarchical, with a subtree per force, and Mokhov’s verifying trace is flat, a dependency-hash list per key. The tree structure is what gives sharing, swapping and switching. gen-memo’s trace is the flat form. A persisted trace across evaluations could be flat (cheap, per key) or hierarchical (supports the three patterns, costs more storage and a tree diff), and that choice is open.

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