A Programming Paradigm for Spatiotemporal Composability

> *Make "plugins" truly plug-and-unplug* > A close reading of Shi, Zhang & Cui (Peking University / DeepSeek-AI), 88 pages, 8 sections, 124 references.

---

One-Sentence Thesis

**Reify classical *effects* and *coeffects*—long confined to static type annotations—into a single first-class runtime "context type." Components can then be freely plugged and unplugged at runtime: unloading fully rolls back side effects, and dependencies automatically reconnect as services appear or disappear.**

This sounds modest but strikes at a root. Classical effect systems track effects within lexical scopes and dispose of them via compile-time handlers; dynamic composition, by contrast, needs guarantees in a runtime where components come and go and contexts continuously evolve. The paper transplants that conceptual structure wholesale into the runtime layer, where it can be directly manipulated.

---

Why Unloading a Plugin Is Hard

The VS Code Predicament

VS Code's extension host loads hundreds of extensions in one process. Once an extension calls activate, stopping or uninstalling it requires restarting the host—including all other loaded extensions. The deactivate hook is merely a graceful-shutdown callback, not a mechanism for *in-place* uninstallation. Cleanup quality depends entirely on author discipline: a textbook violation of *locality of concern*, where creation and destruction should live in one place.

A second layer: among VS Code's top 100 extensions, only 7 declare dependencies on non-built-in extensions. The extension surface (commands, views, language features) is a fixed host-defined API, and extensionDependencies values are essentially untyped—no checkable interface to rely on.

Self-Evolving Agent Harnesses: More Urgent

Modern agent harnesses must modify themselves on the fly—tool sets, execution environments, permission sandboxes, memory systems, sub-agent orchestration. Each self-modification is an instance of dynamic composition.

• Without temporal composability, every self-edit demands a full process restart, discarding in-process state (caches, connections, half-computed work); worse, a buggy self-edit can paralyze the very process that would recover from it.
• Without spatial composability, each module must hand-write ad-hoc re-derivation logic when dependencies appear, vanish, or change owner.

Coarse-Grained Workarounds Are Costly

Operating systems and container orchestration offer coarse alternatives, but at a steep price. Restarts discard process state and cost seconds to minutes; maintaining availability requires redundant replicas. Container-level orchestration cannot express dependencies within a single address space and adds network overhead at every interaction. The mismatch of granularity demands a composition abstraction that operates at the component's own granularity.

---

The Two Axes: Temporal and Spatial Composability

| Dimension | Question | Classical Theory | Dynamic Requirement | |-----------|----------|------------------|---------------------| | Temporal | Can a component's environment changes be fully and safely rolled back on unload? | Effects — how a computation *changes* its environment | Long-lived, non-lexically scoped side effects must be tracked and revertible | | Spatial | Can inter-component dependencies be declared, resolved, and adapted on the fly? | Coeffects — how a computation *relies on* its environment | Dependencies born and dying at runtime require reactive topology management |

The four quadrants:

• Bottom-left: classic static composition (functions, modules, inheritance).
• Top-left: container/process isolation—rolls back cleanly, but granularity is too coarse.
• Bottom-right: OSGi, extensionDependencies—topology is expressible, but cleanup relies on author discipline.
• Top-right *(Cordis)*: both dimensions together—correctness promoted from author discipline to a structural property.

> Core move: instead of piling more annotations on top of static types, *reify* the effect/coeffect conceptual structure so the runtime can manipulate it directly.

---

Reversible Effects: Every Transformation Carries Its Inverse

An effect is modeled as a function Γ → Γ × (Γ → Γ): applied to the current context, it returns not only the new context but also a rollback function. If an author cannot supply an inverse, they cannot perform the operation—this is the key safety property.

Effect Context and Accumulator

Define effect context ∂Γ ≔ Γ × (Γ → Γ), written (γ, φ):

• γ: current context state.
• φ: accumulator—the composition of inverses of all applied effects, i.e., the restore function.

Initial state: (γ₀, idΓ).

trackΓ(f, g) converts a "forward f + candidate inverse g" into a transformation on ∂Γ: apply f to γ and compose g into φ. Theorem 5 proves trackΓ is a monoid homomorphism—track-then-compose and compose-then-track agree.

recoverΓ(γ, φ) ≔ (φ(γ), idΓ) restores γ via φ and resets the accumulator.

Theorem 7 (soundness invariant): before and after recover, φ(γ) = γ₀ holds. So no matter how many effects are applied, as long as each supplied inverse is genuinely an inverse, recovery returns the system to its initial state.

Independence and Corollary 21

When multiple components interleave, a component's inverse may run after another component has shifted shared state. Can it still undo only its own changes?

Yes—when two effects' transformation monoids commute (Definition 19), inverses can be applied in any order and still reach γ₀. This is Corollary 21: *independence buys arbitrary ordering*, including interleaved multi-component orderings. Corollary 21 is the passport for parallel multi-component plug/unplug; non-commuting effects fall back to a sequencing theorem (Theorem 63).

---

Reactive Coeffects: Dependencies as Specifications

Spatial composability lets components declare dependencies declaratively: "I need a service of type S with capability C." The runtime resolves the dependency, binds it, and—crucially—notifies the component when the binding changes (a service appears, vanishes, or is replaced).

Two structural consequences:

1. Coeffects as effects, effects as reversible: the coeffect's binding logic is itself an effect, so subscribing, accessing, and unsubscribing all participate in the same reversal machinery. No orphaned subscriptions, no dangling bindings. 2. Isolation and interception: declaring a dependency through a context isolates it; the runtime can intercept, route, or mock the resolution—useful for testing and sandboxing.

---

Unified Context Γ∞: Where the Two Mechanisms Meet

The two mechanisms fuse into one abstraction:

• Hierarchical composition: context composition forms a literal tree, with each node owning its sub-effects. Plugging and unplugging a subtree is a single localized operation.
• Observation equivalence ≃: two contexts are equivalent if no observer can distinguish them. This gives a clean notion of when an unload truly restored the environment.
• Paradigm positioning: Γ∞ is not a library API—it is a *programming paradigm* that makes dynamic composition the default, rather than a heroic discipline.

---

Dynamic Composition Calculus and Meta-Theory

The paper formalizes the above as a calculus with:

• A type system for contexts and capabilities.
• Operational semantics for plug, unplug, rebind, and recover.
• Key theorems: the soundness invariant (Theorem 7), independence/commutativity (Corollary 21), and a sequencing theorem (Theorem 63) that orders non-commuting effects.

Together these deliver *temporal* guarantees (any sequence of operations followed by recover returns to the starting state, modulo independence assumptions) and *spatial* guarantees (dependency updates propagate reactively and consistently).

---

The Cordis Implementation: Three Layers of a Meta-Framework

Core Library Essentials

• Context type Γ∞ as the unit of composition.
• track / recover primitives.
• Reactive dependency resolution with automatic subscription bookkeeping.

Loader: Reconciliation and Hot-Module Reload

The loader reconciles a desired plugin set against the running set, computing a minimal sequence of unloads, loads, rebinds, and recoveries. Combined with hot-module reload (HMR), authors can edit a plugin and see results in-process—no restart, no lost state, no manual cleanup.

---

Case Study: Koishi, an Ecosystem of 4,000+ Plugins

Koishi is a chat-bot framework whose community has published over 4,000 plugins. Cordis is its runtime substrate. Empirical observations from the paper:

• Plugins can be installed, uninstalled, and updated without restarting the host process.
• A plugin's side effects (registered commands, opened connections, scheduled tasks) disappear cleanly when it unloads.
• When a plugin updates, downstream consumers automatically rebind—no manual coordination.
• The same machinery supports the agent-harness self-modification scenario described in §2.

---

Highlights from the Discussion Section

The authors surface several non-obvious observations:

• The reverse is part of the operation, not a separate callback. This is what makes correctness a structural property rather than a discipline.
• Independence is a design choice, not an accident. Authors who keep their effects on commuting sub-monoids gain free arbitrary ordering; authors who don't pay an ordering tax but get strong guarantees from Theorem 63.
• Reactive coeffects collapse a class of bugs. The classic "subscribe but forgot to unsubscribe," "called service that has been replaced," and "cyclic dependency after reload" categories become structurally absent.

---

Relationship to Prior Work

The paper positions itself against:

• Algebraic effect handlers (Plotkin & Pretnar, Koka, Eff): excellent for lexical, compile-time-tracked effects, but their handler structure is static.
• OSGi, Eclipse, VS Code: dynamic modules, but cleanup is callback-based and dependency declarations are weakly typed.
• Container orchestration (Kubernetes, etc.): dynamic lifecycle, but at the wrong granularity and with the wrong cost model.
• CRDTs, observable systems, dependency injection frameworks: each addresses a facet; Cordis unifies them under one reversible-effect + reactive-coeffect framework.

---

Conclusion: Built for Self-Evolution

The closing argument is that self-evolving software—agents that rewire their own tools, environments, and policies—needs composition guarantees that survive its own modifications. A self-editing system that cannot roll back its edits is sawing off the branch it sits on. Cordis supplies that structural rollback and reactivity in one framework, validated at ecosystem scale by Koishi's 4,000+ plugins.

---

Key Points

• Core idea: reify effects and coeffects into a single first-class runtime context type Γ∞, so dynamic composition gains guarantees that classical static type systems cannot provide.
• Temporal axis: every effect carries its inverse as part of the operation signature, not as a separate cleanup callback. An accumulator plus recover restores initial state by construction (Theorem 7).
• Spatial axis: coeffects declared as specifications are resolved reactively; binding changes propagate automatically. Coeception logic participates in the same reversal machinery, eliminating orphaned subscriptions.
• Unification: Γ∞ is a tree of contexts; recover at any subtree returns that subtree's observable state. Observation equivalence ≃ formalizes "fully restored."
• Independence buys arbitrary ordering (Corollary 21): commuting effects can be undone in any sequence, enabling parallel multi-component plug/unplug.
• Cordis meta-framework: three-layer implementation (core library, loader, ecosystem) with hot-module reload and minimal-diff reconciliation between desired and running plugin sets.
• Empirical validation: Koishi's 4,000+ production plugins demonstrate clean install/uninstall, automatic rebind on updates, and in-process self-modification for agent harnesses.
• Position: distinct from algebraic effect handlers (lexical/static), OSGi/VS Code (callback-based cleanup, weakly typed deps), and container orchestration (wrong granularity, high overhead).
• Stated motivation: self-evolving agent harnesses that can safely modify their own toolset, execution environment, and policies in-process, with structural rollback if a self-edit fails.