Reactive Coeffects: spatial dependency response

论文版本948a07b (main)

The paper uses Reactive Coeffects to solve spatial composability — whether the system can automatically adjust lifecycles and dependency wiring after a component's dependencies appear, disappear or are replaced. Core idea: components declare what they need (a coeffect specification), and the runtime notifies them per spec when the context changes.

Coeffect Context and "set is an effect"

[Paper's original conclusion §3.2.1] The coeffect context Σ ≔ (k : K) ⇀ 𝒱_k is a finite partial function from dependency keys to typed values. get and set are the two core operations (Def 23), and set(k, v) is itself an effect — a coeffect operation is an effect, so coeffect provision automatically inherits trackability and recoverability. This is the bridge between Revertible Effects and Reactive Coeffects: declaring a dependency (provide) is simultaneously performing a revertible effect.

Coeffect Specification and the three-state change

[Paper's original conclusion §3.2.2] A coeffect specification d ⊆ K is the set of dependency keys a component declares; the satisfaction predicate σ ⊧ d ≔ ∀k ∈ d. k ∈ dom(σ). Any effect turning σ into σ' can be classified by d as activating / deactivating / neutral (Def 26):

• activating: before the change σ did not satisfy d, after the change σ' does — the component should be activated;
• deactivating: before the change it did, after the change it does not — the component should be unloaded;
• neutral: it is satisfied before and after, or not satisfied before and after — the component need not switch state (but the dependency instance may have been swapped).

The full database A + RAG B example

Concrete case (the standard example running through the paper):

Plugin A (database plugin): set('database', dbService)  provides the dependency
Plugin B (RAG plugin):     declares d_B = {'database'}    needs the dependency

• A appears: A provides the database service via ctx.set('database', dbService); the key 'database' appears in σ. B's declared d_B = {'database'} goes from unsatisfied to satisfied — activating, B is notified and automatically activated, and obtains dbService from ctx.get('database').
• A disappears or is replaced: A's fiber enters Unloading; the 'database' key is removed from σ. B's d_B goes from satisfied to unsatisfied — deactivating, B is notified and automatically unloaded (its own inverse accumulator is applied, releasing resources held by B).
• A new A is ready: the new database plugin A' provides via ctx.set('database', newDbService). B's d_B goes from unsatisfied back to satisfied — activating, B reactivates using the new dependency and obtains newDbService.

Throughout, B's code never has to actively probe "if A is gone, then ..." — the runtime notifies automatically per the coeffect spec.

Committed View vs Target View

[Paper's original conclusion §4.1, §4.2] In the Cordis implementation there are two key dependency resolution views:

• Committed View (ω): the currently committed dependency resolution, recording the fiber-name-to-provider mapping. What a component reads throughout an episode is this view, guaranteeing that dependencies are stable within the component's current lifecycle (see the Ordering theorem).
• Target View: the dependency resolution state the fiber is expected to be in, recomputed by refresh whenever the configuration changes. When target diverges from committed, lifecycle transitions (activation, unloading, or reload) are triggered.

[Paper's original conclusion §4.2] Key detail: the target view records provider identity (fiber uid), not whether the value is equal. The paper notes explicitly: "makes the comparison usable, since a different fiber providing an equal value would otherwise compare equal" — if only values were compared, different fibers providing equal values would be misjudged as "the dependency did not change", and reactivation would not fire, leaving the consumer using a snapshot of the old fiber without knowing the provider had been swapped. fiber.target in the Cordis implementation stores a uid digest of the dependency resolution result (§5.1.3).

Isolation and Interception

[Paper's original conclusion §3.2.3] Two orthogonal derived mechanisms:

• Isolation: through the isolation realm table ρ : K ⇀ R, the same key k resolves to different realms r in different contexts, and thus binds to different values. ctx.isolate(k, r) derives a new context that only overrides ρ's mapping at k (a derived realization, not modifying the parent table).
• Interception: hangs metadata on a coeffect ι : K → ℙ_k; the provider function receives the metadata and adjusts its behavior accordingly. ctx.intercept(k, ν) derives a context that merges ν into the metadata at k.

Difference: Isolation replaces "what binding a key resolves to" (swap instance), while Interception modifies "how the binding is used" (add constraints, no swap). Isolation is a derived realization (no inverse needed — just discard the child context), whereas set is an in-place realization (an inverse is needed to revert).

Scenario comparison

Scenario	Use Isolation	Use Interception
Multi-tenant / different workspaces	The same key 'db' resolves to each tenant's own instance	—
Sub-Agent independent environment	The same 'filesystem' resolves to independent instances per sub-Agent	—
Test doubles	Override with a mock realm	—
Read-only filesystem permission	—	Attach a readonly metadata
Different plugins using different models	Isolate each one's 'model' key	—
Strict access policy for community plugins	—	Attach capability-restriction metadata

Reactive Coeffects solve "perceiving dependency changes", but the component instance's own load/unload/reload process still requires a state machine to manage it. See Lifecycle and unload order.