Incr

Incremental computation as a handler over a content-addressed dependency graph.

An incremental computation is a demand-driven graph of two node kinds: an input is a changeable cell you set; a memo node caches a pure or replayable thunk keyed by its content. Reading a node from inside another node (get) records a dependency edge, because the read goes through the effect and run_incr sits in the middle: the effect is the instrumentation. After a set, re-reading a node re-demands exactly the affected cone, and a memo whose recomputed value is unchanged (by content hash) does not disturb its dependents. That early cutoff is the whole game, and here it is an exact blake3 comparison over the serialized value, not a user-written equality.

The engine is the spec’s demand() verbatim: verify a memo’s recorded deps by re-demanding each and comparing hashes; return the cached value if they all match; else rerun, capturing a fresh dep set. It is one tail-resumptive handler that re-installs itself to run a memo thunk (so the thunk’s own gets are caught as that node’s deps), threading the node table as parameter-passed state that Perceus reclaims when the run_incr scope drops.

Values are heterogeneous across a single run (an Int total beside a Map of scores), so the engine works over the type-erased Bytes a Serialize instance produces, and the typed surface (input/get/set/memo) encodes at the boundary where the type is known. A node handle Incr(a) is a phantom-typed key, so get on it round-trips back to a.

Types

`Incr`

type Incr(a) = IncrRef(String)

A handle to an incremental node carrying values of type a. It is a phantom-typed wrapper over the node’s content key; get on it returns a.

Effects

`IncrRaw`

effect IncrRaw
  incr_input(Bytes) : String
  incr_get(String) : Bytes
  incr_set(String, Bytes) : Unit
  incr_memo(() -> Bytes ! {IncrRaw | e}) : String

Functions and Values

`run_incr`

run_incr : forall e0 a. (() -> a ! {Incr.IncrRaw, e0}) -> a ! {e0}

Discharge the Incr effect, running action as the root observer of a fresh demand graph. The node table lives only for this scope. The ambient row e (the replayable effects the memo thunks perform beyond reading nodes) flows out unchanged, exactly as run_async passes its fibers’ row through.

`input`

input : forall a. (a) -> Incr.Incr(a) ! {Incr.IncrRaw}

Create an input node holding v. Its key is its creation order in the run.

`get`

get : forall a. (Incr.Incr(a)) -> a ! {Fail, Incr.IncrRaw}

Read a node, recording a dependency edge from the memo currently being computed (if any) to this node.

`set`

set : forall a. (Incr.Incr(a), a) -> Unit ! {Incr.IncrRaw}

Update an input node. A no-op when v is equal (by content) to the node’s current value.

`memo`

memo : forall e0 a. (() -> a ! {Incr.IncrRaw, e0}) -> Incr.Incr(a) ! {Incr.IncrRaw, e0}

A derived node caching thunk by content, with early cutoff on its result: a cache hit reuses the value and skips the thunk, so a memo that does not recompute does not re-perform its (replayable) effects. Its key is its creation order in the run.

Write a multi-statement memo with the trailing block form, whose statements read other nodes with get:

let ranking = memo() fn
  let live = get(scores)
  sort_desc(map_to_list(live))

A one-liner is the same thing spelled with a lambda: memo(\() -> get(a) + 1).

`run_incr_durable`

run_incr_durable : forall a. (String, String, () -> a ! {Fail, Incr.IncrRaw}) -> a ! {Fail, IO}

Discharge the Incr effect with a durable snapshot at path, tagged by tag (the caller-named program identity: a snapshot written under a different tag cold-starts). This is the file-substrate form of the production path, which rides the content-addressed store once a program can hold a runtime handle on it; the same reduced table is what that store persists.

The action must be pure up to Fail, so its row is closed at {IncrRaw, Fail}: a warm hit skips the memo thunk, and skipping a thunk that printed or drew a random would change the output, so only effect-free thunks may be reused across runs. Only the creation prefix (the memos built before the first get/set) is warmed and persisted; input-dependent memos stay scratch and recompute. Within those bounds a warm run’s output is byte-identical to a cold run, and deleting or corrupting the snapshot changes only cost, never the result.

`run_incr_store`

run_incr_store : forall a. (String, String, () -> a ! {Fail, Incr.IncrRaw}) -> a ! {Fail, IO}

Discharge the Incr effect with a durable snapshot on the content-addressed store rooted at root, tagged by tag (the caller-named program identity). The store form of run_incr_durable: the reduced memo table rides the real store’s object layer (the blob keyed by its content hash) with a ref for tag, rather than a snapshot file. The file substrate stays available; a call site picks the substrate by picking the handler.

Every durability guarantee of the file form carries over. The action is pure up to Fail, so only the creation-prefix memos are warmed and persisted; a warm run’s output is byte-identical to a cold run; and a missing, dangling, or corrupt store entry cold-starts, changing only cost, never the result.

`run_incr_durable_replay`

run_incr_durable_replay : forall e0 a. (String, String, () -> a ! {Fail, IO, Incr.IncrRaw, Output, e0}) -> a ! {Fail, IO, e0}

Discharge the Incr effect with a durable, trace-replay snapshot at path, tagged by tag. Unlike run_incr_durable, the memo thunks may perform any replayable effect: a cold run records each memo’s output beside its result, and a durable warm hit REPLAYS that output instead of re-running the thunk, so a warm run’s console is byte-identical to a cold run’s, effects included. A missing, corrupt, foreign, or wrong-version snapshot is a silent cold start.

`run_incr_store_replay`

run_incr_store_replay : forall e0 a. (String, String, () -> a ! {Fail, IO, Incr.IncrRaw, Output, e0}) -> a ! {Fail, IO, e0}

The content-addressed-store form of run_incr_durable_replay: the traced memo table (results and output traces) rides the real store’s object layer, keyed by tag, rather than a snapshot file. Every guarantee of the file form carries over; a missing, dangling, or corrupt store entry cold-starts.

Keyboard shortcuts

Prism