Lesson 10: The Context Paradigm: Unifying Context Types

One-liner: The Context Paradigm packs three things — "where I am (current state), what I changed (inverse functions), what I need (dependency table)" — into a single recursive ctx entity, turning the "plug and unplug" metaphor for components into a structure that can actually be implemented — the correctness of undo and reconnection no longer relies on developer discipline but is guaranteed by construction.

Step 1: One ctx Holds Three Things — "Where I Am, What I Changed, What I Need"

First, recall the two main threads from the previous lessons:

• Effects: the side effects components leave behind when they do things (changing files, spawning processes...), which must be reversible;
• Coeffects: the things components need when they do things (some service, some config...), which must connect automatically.

Previously, we handled these with two separate mechanisms. This section of the paper makes a bold unification: it stuffs effects, coeffects, and the "current state" all into a single entity — a recursive context type:

Definition 24 (Context Type): Γ∞ ≔ μΓ. Γ × (Γ → Γ) × Σ

Don't worry if you can't read this formula; broken down, it's one sentence: a single ctx carries three things at once.

Together, the three components answer the three questions a component must answer before every interaction with the environment: Where am I? What have I changed? What am I still missing? Every interaction goes through this single ctx entity.

Why is it called "recursive"? Because inside the first component Γ, there is still the same Γ — like Russian nesting dolls, every layer is the same kind of thing, so you can nest as deep as you like. This "self-nesting" structure has a dedicated name: self-similarity. Earlier in the paper, effects were abstracted into an ever-growing "𝜕 tower"; here, recursion flattens the whole tower into a single type.

Looking one level deeper, this design brings two additional benefits:

• Effects become endomorphisms on ctx: an effect is "take a ctx in, come out with a new ctx and an inverse function" — in and out are the same type, so any effects can be composed arbitrarily.
• Σ can hold all shared state: because the type Σ ultimately depends on is unrestricted, any global state you want to share between components can be encoded as a typed dependency inside Σ. In other words, Σ covers not just "inter-component dependencies" but all shared mutable state.

Step 2: Hierarchical Composition — Plugging In Really Is Just "Plug" and "Unplug"

In the previous lesson (component lifecycle), we said "components are like plugs; they can be plugged in and unplugged." Now that we have Γ∞, this metaphor finally goes from rhetoric to construction.

Because ctx is recursive, a child component's ctx is naturally nested inside its parent's ctx — the parent context aggregates the effects of multiple child layers, forming a tree-shaped control structure:

        ┌───────────────┐
        │  parent ctx   │  ← aggregates and manages all child components' effects
        └───────┬───────┘
    ┌───────────┼───────────┐
    ▼           ▼           ▼
 [Comp A]    [Comp B]    [Comp C]   ← each plugs/unplugs independently, without affecting others

"Plug and unplug" is realized directly as two operations:

This design provides three key guarantees:

1. Unplugging does not affect others: unmounting a component only restores its own effects; other running components are not affected at all;
2. Layers do not interfere with each other: components at different levels of the tree can mount and unmount independently, with no globally imposed order;
3. Nesting at arbitrary depth: the parent context aggregates and manages the effects of all its child components, and children can nest more children — as many layers as you like.

🎁 Analogy: a parent context is like a "power strip with multiple sockets" — pull out one device and the others keep drawing power; and the power strip itself can be plugged into another power strip, extending endlessly.

Step 3: One Effect, Two Implementations — In-place or Derived

Here the paper makes a crucial conceptual cut: separating denotation from implementation.

Typing an operation as an effect on Γ∞ fixes its denotation — "a successor state + a corresponding inverse function"; but it does not fix its implementation — how that inverse function actually executes is up to the implementation.

Definition 25 (Two Implementations of an Effect Function): An effect function f admits two implementation styles.

Note the distinction between "denotation" and "implementation": for the same effect, the denotation is fixed (successor state + inverse function), but either of the two implementations may be chosen. Which one you pick depends on the host environment:

• In a purely functional environment, there is no such thing as "in-place mutation", so the two implementations coincide (both can only be derived);
• In an imperative host, developers can choose per operation freely: use in-place when you want speed, use derived when you don't want to touch the original data.

💡 The paper says Section 4.1.2 will give representative code for both implementations — in the next lesson we'll see what they look like.

Step 4: Why Is It a "Paradigm"? — Contrasting Two Old Approaches

The paper's ambition goes beyond "giving a type": it claims this context type itself constitutes a programming paradigm. To understand this, first look at how the two old paradigms handle side effects — they stand at opposite poles of the same spectrum.

Far Left: Explicit State Passing (Functional)

To preserve referential transparency, purely functional languages model side effects as explicit transformations of state — the classic example being the state monad S → (A, S), which threads the environment through every computation.

• ✅ Benefits: effects are visible in the types, enabling equational reasoning and excellent traceability;
• ❌ Costs: every function in the call chain must take and return the state parameter, even if it just passes the state through unchanged; once the number of effect dimensions grows (logging, config, I/O), the boilerplate of monad stacks or effect handlers quickly balloons.

🎁 Analogy: the company requires every document to pass through every employee and be signed by each, even if they're just forwarding it — traceable, but exhausting.

Far Right: Implicit Mutation (Imperative / OOP)

Mainstream imperative languages let components directly mutate shared state and directly take dependencies, declaring nothing at the call site.

• ✅ Benefits: easy to write, excellent ergonomics;
• ❌ Costs: untraceable. The paper gives two concrete examples:
  • On the effect side: React's useEffect hook — it registers persistent side effects on a fiber inside the component, but neither the effect target nor the registration mechanism is an explicit parameter; its identity is determined by the call-order position hidden in runtime state;
  • On the coeffect side: Java's service locator (e.g. Spring's getBean(...)) — dependencies are fetched from a global registry, every call site must null-check and cast, and the dependencies are implicit and scattered throughout the codebase.

Worse: to understand what f() actually changes about the system or depends on, you have to recursively read its implementation along the call graph; refactoring therefore becomes fragile — moving or deleting a call can silently break invariants far away.

🎁 Analogy: a shared blackboard — anyone can write on it, but nobody signs their name — convenient, but when something goes wrong you can't find out who changed it.

The Middle: The Context Paradigm — the Best of Both

The Context Paradigm stitches the two poles together: both effects and coeffects are mediated through an explicit context parameter. Therefore:

• Every operation can be attributed to the ctx that invoked it, and in turn to the component that owns that ctx — as traceable as the functional style;
• Developers don't hand-write a pile of state parameters through the call chain — as terse as the imperative style.

And it's not just a "compromise" — it also upgrades the correctness guarantees:

Put both directions together and you get this section's core conclusion: correctness that previously required developer discipline has become a structural property of the paradigm.

Key Points Recap

That was a lot of information; just remember these five sentences:

1. Unified context: Γ∞ ≔ μΓ. Γ × (Γ → Γ) × Σ — a single ctx holds "current state Γ", "accumulated inverse functions Γ → Γ", and "dependency table Σ", i.e. "where I am, what I changed, what I need".
2. Recursive self-similarity: inside Γ there is still Γ, like Russian nesting dolls — nest as deep as you like; effects become endomorphisms on ctx (ctx in, ctx out plus inverse), and Σ can encode all shared mutable state.
3. Hierarchical composition: parent contexts aggregate child effects into a tree structure; mount = plug in the effect, unmount = unplug and restore, without affecting each other, supporting nesting at arbitrary depth.
4. Denotation vs. implementation: an effect fixes its "denotation" (successor state + inverse function) but not its implementation — in-place (mutate ctx + non-trivial inverse) or derived (return new ctx + identity inverse, restoration = discard).
5. Paradigm positioning: functional explicit state passing is traceable but verbose; imperative implicit mutation is ergonomic but untraceable; the Context Paradigm uses an explicit ctx to get both, turning correctness from "developer discipline" into "structural guarantee".

🚀 Armchair theorizing ends here — the next lesson enters Chapter 4 of the paper, "Implementation and Case Study": the Cordis core library, to see how Γ∞ becomes real code and how the in-place / derived implementations are actually written.