Chapter 7
Independence — why unrelated plugins don't disturb each other
The question this chapter answers: chapter 4's guarantee assumed an undo meets exactly the world its own step produced. In a running system it never does. Disable stats while search, loaded after it, stays: stats's undos run against a world that search has since changed. Or two plugins load concurrently, their steps interleaved. When does an undo still undo the right thing in a world foreign steps have moved? The answer is: when the foreign steps and the undo commute.
7.1 Commuting: order doesn't matter
Two changes to the world commute when doing them in either order lands in the same place: f ∘ g = g ∘ f. "Register route /stats" and "register route /search" commute — the routing table ends up with both either way. "Insert middleware A before everything" and "insert middleware B before everything" do not — whichever ran second is in front.
A plugin's activation gives rise to many maps: the forward map of each step, and the undo each step returns at each world. The paper collects them:
𝔐(i) is the set of all functions you can build by composing forward maps and yielded undos of any step reachable from iterator i.
In words: everything the plugin can ever do or undo, and all sequences thereof. Lemma 41: to check that two of these commute elementwise, it is enough to check their generators (the individual steps and undos); composition cannot introduce a new failure.
Iterators i and j are independent when (1) every map in 𝔐(i) commutes with every map in 𝔐(j), and (2) applying any of j's maps to the world does not change what i's steps yield — neither the undo they return nor the continuation they choose — and vice versa.
In words: (1) the two plugins' doings and undoings can be reordered freely; (2) neither plugin changes the other's mind — what undo it would hand back, or which step it takes next. Clause (2) matters because an undo is computed from the world it sees (chapter 4.3); a foreign change could make it compute a different undo. Note the pairing in (1) includes "one plugin's forward step with the other plugin's undo" — that is the case removal actually exercises.
7.2 The payoff: undo in any order
Let e₁, …, eₙ be pairwise independent, applied in order from γ₀. Applying their undos at the final world, in the order of any permutation, reaches γ₀.
In words: if plugins are independent, you may disable them in any order — including an order different from the one they loaded in — and the world ends where it began. This is what makes "disable stats but keep search" legitimate. The proof is a page; its idea is that independence lets each undo be slid leftward past the foreign forward steps until it meets its own step, where the chapter-4 promise applies.
7.3 Reduce it to keys, and put the burden on the provider
Checking Def 42 for every pair of plugins would be hopeless. The context paradigm makes it tractable, because every step is an operation at a key, a provision at a key, or an instantiation:
- Thm 45. Operations at distinct keys always commute — each reads and writes one binding.
- Def 44. A key is commutative when any two of its own operations are independent (outcomes included, an operation with itself included).
- Thm 47. Two context-mediated plugins are independent provided neither provides a key the other touches (P₁∩S₂ = P₂∩S₁ = ∅) and every key at which both perform operations is commutative.
So the whole question collapses to: which keys are commutative? And the paper makes proving it the provider's obligation (Def 46: the proof is the third component of the key), discharged by a representation choice. Consumers assume nothing.
| Key shape | Commutative? | Why |
|---|---|---|
| Table of entries; each add draws a unique id, its undo removes that id (event listeners, routes, CRDT-style adds) | Yes | Either order leaves a table that answers every test alike; either entry can be withdrawn while the other stands. |
| Ordered chain (middleware) | No | Insertion before vs after is observable; neither order withdraws without disturbing the other. |
| Allocator whose handles are never compared | Yes | ≃ₖ relates heaps up to renaming handles (as CompCert relates memories). |
Allocator whose handles are compared (POSIX open) | No | The next outcome separates the two orders. |
This is where chapter 6's lever pays: publishing fewer outcomes admits fewer tests, coarsens ≃ₖ, and can move a key from the "no" row to the "yes" row.
7.4 The division of labour
The commuting part of a plugin's work is carried by effects: perform them in whatever order the task calls for, revert them in whatever order the system finds convenient (Thm 43); no two plugins constrain each other. The order-sensitive part is carried by coeffects: within one plugin the accumulator imposes LIFO (Thm 16); across plugins a declared dependency imposes provider-before-consumer (chapter 5, made global in chapter 9). "Composability is thereby had at the grain of components rather than of single effects."
Everything above assumes every shared location is bound at a key. A location the system cannot reify as a coeffect is outside Thm 47 and outside the system boundary of chapter 12.
"Live sibling registry currently requires full re-call; framework ask filed for incremental add/drop" — this is the commutative-key question. A roster as a set of uniquely-tagged entries makes each plugin's registration a commuting revertible effect (add/drop incremental, order-free). If order genuinely matters, the paper's advice is to carry it in a coeffect — a sequencer or broker service — not in the effects.