Chapter 6
The context paradigm & observational equivalence
The question this chapter answers: chapters 4 and 5 each guarantee something about one plugin. What has to be true of the whole system for those guarantees to survive many plugins loading and unloading in any order? The paper's answer has two halves. First, a discipline: every interaction between a plugin and the world goes through one context object, and every shared piece of state lives at a key in the table. Second, a definition of "the same" coarse enough that "undo restores the world" can actually be true — because physically it never is.
6.1 One context, containing itself
Chapter 4 gave us the effect context (world + undo stack); chapter 5 the service table. Put them in one structure and let it nest:
Γ∞ ≔ μΓ. Γ × (Γ → Γ) × Σ
In words: a context is (a context, an undo stack for this level, a service table). The first component being a context again is what makes it a tree: a parent context holds child contexts, each with its own undo stack. Loading a plugin = plugging a child in; unloading = running its undo stack and unplugging it; and this works at every depth, so a plugin that loads sub-plugins is nothing special.
Because the table's value family 𝒱 is unconstrained, any shared mutable state can be bound at a key — a counter, a registry, a connection pool. The paper: "Σ subsumes all shared mutable states, not just inter-component dependencies. Every interaction between a component and its environment passes through this single entity."
6.2 What a key really is: a type, some operations, and a promise
If everything shared lives at a key, then what a plugin may do to a shared thing has to be fixed too — otherwise "through the context" would be an empty phrase.
A key k carries a triple (𝒱ₖ, 𝒜ₖ, witness): its value type; a set of operations a holder may perform on the value; and a promise (chapter 7) that those operations commute with one another. Each operation a ∈ 𝒜ₖ has type
a : Xₐ → 𝒱ₖ ⇀ 𝒱ₖ × (𝒱ₖ ⇀ 𝒱ₖ) × Bₐ
In words: given an argument, an operation transforms the value, returns an undo for that transformation (so it is an effect function on the value), and returns an outcome Bₐ — the result the caller sees. A roster key might have operations add(name) → id and remove(id) → (). Lifting an operation to the whole table touches the binding at k and nothing else.
A plugin's effect function must be an iterator whose every step is one of: (1) an operation at a key it declared, (2) a provision (set) at a key it said it provides, (3) an instantiation of a child plugin. The paper calls such iterators context-mediated. Anything else — "a map reading anything else" — is outside the paradigm. Its example: an allocator drawing handles from a counter the context does not hold is outside, and becomes inside the moment the counter is bound at a key.
Nothing in the construction enforces that every shared location is at a key. It is the rule a plugin author follows. A location the system cannot reify as a coeffect lies outside the guarantees (§3.4's closing remark; chapter 12 on the system boundary).
6.3 "The same" up to what you can observe
Thm 7 said the undo stack takes the world back to γ₀. Physically that is false: free does not put the heap back the way it was before malloc; a fresh id, once generated, is not un-generated by removing the entry that used it. So every equality in the paper is read up to an equivalence ≃, and the honest question is: which one?
The paper's answer is the one you know from algorithms: two data structures are the same if no sequence of their operations can tell them apart.
A test is a finite sequence of the key's operations (forward maps and their undos), applied one after another, recording the outcomes. Two values are indistinguishable, v ≃ₖ v′, when every test is defined on both or neither and yields the same outcomes on both. Lemma 32: this is an equivalence relation, every operation respects it, and it is the coarsest such relation.
In words: ≃ₖ is "equal as far as the published operations can see". A roster that returns sets from list cannot see insertion order, so two rosters with the same members are ≃ₖ. Coarsest means: any equivalence the operations respect is contained in it — so to show two values are ≃ₖ, exhibit any relation the operations respect that contains the pair.
σ ≃_S σ′ ≔ dom(σ)∩S = dom(σ′)∩S ∧ ∀k ∈ dom(σ)∩S. σ(k) ≃ₖ σ′(k)
In words: two tables agree at a set of keys S when they have the same keys from S, each bound to indistinguishable values. Everything outside S — and everything no key binds at all, like heap layout — is forgotten. That forgetting is exactly what lets "undo restores the world" be true.
The chapter-4 definitions are then re-read with ≃_S in place of = (Defs 36–37), where S is the set of keys the plugin declares or provides. So a plugin's promise is local: its undo has to restore its own interface, not the universe (Lemma 39).
It is the paper's answer to "you can't really undo send()". Recovery means restoration up to what the published interface can observe. That turns interface design into a lever: publish fewer outcomes → coarser ≃ₖ → more counts as reverted, and more operations commute (next chapter). The paper's example: POSIX open must return the lowest free descriptor, so two opens don't commute; mmap may return any address, so they do. This is the scalable commutativity rule of Clements et al., re-read as a design principle.