Chapter 5
Reactive coeffects — declaring what you need
The question this chapter answers: how does a plugin say what it needs, and what should happen when what it needs appears, disappears, or is replaced while the system runs? The paper's answer: put every shared thing in one typed table; make adding to the table an undoable effect (so chapter 4 already tracks it); and have each plugin declare the keys it needs, so every change to the table can be classified as "now satisfied", "no longer satisfied", or "doesn't matter" for that plugin.
A db plugin provides a database connection under the key db. A search plugin declares inject: ['db']. Scenarios: search loads before db; db is disabled while search is running; db is swapped for a different database plugin; two tenants each want their own db.
5.1 The service table is a typed dictionary
Σ ≔ (k : K) ⇀ 𝒱ₖ
In words: a finite dictionary from keys to values, where each key has its own value type (the "dependent" part — see primer §6). σ(k) looks up; σ[k ↦ v] inserts; σ ∖ k removes; k ∈ dom(σ) asks whether the key is present. This is an inversion-of-control container, formalized.
get(k)(σ) = σ(k) [needs k ∈ dom σ] set(k, v)(σ) = (σ[k ↦ v], λσ′. σ′ ∖ k) [needs k ∉ dom σ]
In words: get reads a key that must be present. set inserts a key that must be absent, and returns two things: the new table, and a function that removes the key again.
Stop on that second return value. set has the shape Σ → Σ × (Σ → Σ) — it is an effect function in the sense of chapter 4. So providing a service is tracked and undone by the machinery we already have. The paper's own phrasing: "coeffect operations are effects, and effects are revertible." That one sentence is the hinge of the design: chapters 4 and 5 are not two mechanisms bolted together, they are one mechanism applied to a particular kind of state.
// ctx.provide('db', conn) in Cordis is exactly set(k, v): it runs inside ctx.effect
// and returns a disposer that deletes the key. (chapter 10 shows the real code)The preconditions (no double provide, no removing an absent key) are errors that leave the table unchanged, so all the chapter-4 formulas apply as they stand.
5.2 Declaring needs, and classifying every change
Reading an absent key is a runtime failure, so a plugin should only run once everything it needs is present. Its needs are a set of keys:
𝔇Σ ≔ Set(K) σ ⊧ d ≔ ∀k ∈ d. k ∈ dom(σ)
In words: a specification d is the inject list. The table satisfies d (written σ ⊧ d) when every listed key is present. Decidable, since the table is finite.
notify_d(σ, σ′) = activating if σ ⊭ d ∧ σ′ ⊧ d; deactivating if σ ⊧ d ∧ σ′ ⊭ d; neutral otherwise
In words: compare "was it satisfied before?" with "is it satisfied after?". Became satisfied → activate the plugin (run its effects, tracked). Stopped being satisfied → deactivate it (run its accumulator). Otherwise ignore.
| Event | search's spec {db} | Classification | What happens to search |
|---|---|---|---|
| search loads, db absent | unsatisfied | — | waits (PENDING); no error |
db provides db | unsatisfied → satisfied | activating | runs its effects |
logger provides log | satisfied → satisfied | neutral | nothing |
db is disabled (its disposer removes db) | satisfied → unsatisfied | deactivating | its accumulator runs; back to waiting |
Why is this "reactive" for free? Because every change to the table goes through set or its undo, and both are effects, so every change is visible at an effect boundary. "This is the algebraic basis of reactivity: the effect system guarantees that every coeffect change is observed."
What is guaranteed: a plugin activates only at a satisfying table, so it never reads an absent key; and every change is classified against its spec. What is not yet guaranteed, because it involves other plugins: that db is withdrawn only after search has finished tearing down (search's teardown may need the connection to close cleanly); and that the keys search reads stay put while it is activating. Both come in chapter 9.
5.3 Isolation: the same key, a different binding per subtree
Two tenants each want their own db. A flat table cannot hold two values at one key. The paper adds one level of indirection:
Σiso ≔ (ρ : K ⇀ R) × (σ : (r : R) ⇀ 𝒱ᵣ)
In words: two tables. ρ maps a key to a realm identifier (a key with no entry is its own realm). σ maps realms to values. To read key k: find its realm, then the value — σ(ρ(k)).
| Context | ρ(db) | σ(realm) |
|---|---|---|
| root | db | — |
| tenant A subtree (after isolate(db, r_A)) | r_A | A's connection |
| tenant B subtree (after isolate(db, r_B)) | r_B | B's connection |
isolate(k, r) rewrites ρ at one key — in a child context, leaving the parent untouched. Providing still goes through set (still an effect, still undoable); isolating needs no undo because nothing shared changed: drop the child context and the adjustment is gone. Uses: multi-tenancy, test doubles, sandboxes. The paper calls this "runtime ad-hoc polymorphism" — the same key resolving differently depending on where you ask from.
5.4 Interception: adjust how a key is used, without reloading anything
Suppose the orchestrator wants the community-written search to get a read-only database, while core plugins keep full access — without changing either db or search. The paper attaches metadata to access:
Σinter ≔ ((k : K) → ℳₖ) × ((k : K) ⇀ (ℳₖ → 𝒱ₖ)) 𝔇inter ≔ (k : K) ⇀ ℳₖ
In words: every key has a metadata type ℳₖ with a merge operation ⊕ₖ and an empty value εₖ (a monoid — e.g. records merged field-by-field). The context carries metadata ι(k); the plugin declares metadata d(k) in its inject; and the provider is now a function from metadata to a value. On access the plugin receives σ(k)(d(k) ⊕ₖ ι(k)).
The merge is right-biased: the context's ι(k) is applied last and wins. So an enclosing context can constrain a plugin's use of a key against the plugin's own declaration. And because interception changes how a binding is used, not whether it is present, changing it is classified neutral by Def 22: no reload, no disturbance to the dependency graph. (Chapter 12 develops this into capability-style access control.)
// Cordis: metadata declared per key in inject, or installed on a subtree with ctx.intercept
ctx.intercept('db', { readonly: true }).plugin(search) // search sees a read-only db; nothing reloads5.5 One denotation, two ways to realize it
An effect's meaning is "(new state, undo)". Its realization may be in-place — mutate the shared thing and return a real undo — or derived — leave the input alone, return a fresh child that inherits from it, with id as the undo (recovery is dropping the child). Purely functional hosts make the two coincide; an imperative host chooses per operation. Providing is in-place; isolation and interception are derived — Cordis literally does Object.create(parent).
inject declarations → a fiber sits PENDING until its providers exist; no more manual boot sequencing. The subtree write fence is interception metadata: readable through Service.resolveConfig without a reload (spike result). "Vault rows override plugin claims" is right-biased ⊕: the enclosing context's metadata wins. Node-agent scopes (Phases 5–6) are isolation realms.