A Programming Paradigm for Spatiotemporal Composability: Making Plugins Truly Pluggable

*Deep-research paper walkthrough, published 2026-08-21. Original paper: "A Programming Paradigm for Spatiotemporal Composability" by Yifan Shi, Wei Zhang (Peking University), and Tianyi Cui (Peking University / DeepSeek-AI). 88 pages, 8 sections, 124 references. Implementation: the Cordis meta-framework; empirical validation on Koishi (4000+ community plugins).*

Thesis

> Elevate classical "effects" and "coeffects" from static annotations in type systems to first-class runtime mechanisms; unify them into a single "context type," forming a programming paradigm in which components can be freely plugged and unplugged at runtime—unloading fully rolls back side effects, and the birth or death of dependencies triggers automatic reconnection.

Classical effect systems track behavior within lexical scopes and dispose of it via compile-time handlers. Dynamic composition instead requires guarantees that hold while components come and go and contexts continuously evolve. The paper's central move is to reify the conceptual structure of effect/coeffect theory so the runtime can manipulate it directly.

Why is unloading a plugin so hard?

Software composition has traditionally relied on three mechanisms—function calls, module imports, and class inheritance—all fixed at compile time and immutable at runtime. Modern systems increasingly demand dynamic composition: plugin architectures and self-evolving agent harnesses load, unload, and reconfigure components while running.

• VS Code's predicament. Once an extension activates, disabling or uninstalling it still requires restarting the extension host process. VS Code only offers a deactivate hook—an optional cleanup callback—separating effect creation from effect disposal, so correctness degrades into an author-discipline problem (loss of *locality of concern*). Cross-extension dependencies are also nearly absent: only 7 of the top 100 extensions declare dependencies on non-builtin extensions, and extensionDependencies values are untyped (any).
• Self-evolving agent harnesses are more pressing. They must modify their own tools, execution environments, permission sandboxes, memory systems, and sub-agent orchestration while serving requests. Without temporal composability, every self-modification requires a full restart (losing in-process state, and risking a bad self-modification disabling the very process needed for recovery). Without spatial composability, modules must handle dependency churn with ad hoc code-replacement strategies that can silently break dependents or introduce cycles.
• Coarse-grained workarounds (OS processes, container orchestration) are costly: restarts discard all in-process state and take seconds to minutes; container-level orchestration cannot express dependencies between components within one address space and adds network overhead across boundaries.

Two orthogonal dimensions

| Dimension | Question answered | Classical counterpart | Dynamic requirement | |---|---|---|---| | Temporal composability | Can environment changes be fully, safely rolled back on unload? | Effects — how a computation *modifies* its environment | Long-lived, non-lexically-scoped side effects must be trackable and reversible | | Spatial composability | Can inter-component dependencies be declared, resolved, and adapted as things change? | Coeffects — how a computation *depends on* its environment | Reactive management of a topology whose providers live and die at runtime |

These two dimensions span a quadrant map: classical static composition sits at the bottom-left; container orchestration buys rollback via restarts (too coarse) at the top-left; OSGi-style systems can declare dependencies but not clean up in place, at the bottom-right. Only the top-right—achieving both—defines the paper's target.

Key points

• Revertible effects (temporal). An effect is modeled as a function Γ → Γ × (Γ → Γ): applying it yields the new context *plus an inverse function*. The inverse is part of the forward operation's return value—there is no separately-written cleanup; if you cannot write the inverse, you cannot offer the operation.
• Effect contexts and accumulators. The effect context ∂Γ ≔ Γ × (Γ → Γ) pairs current state γ with an accumulator φ (the composition of inverses, i.e., the restoration function). trackΓ(f, g) applies f and composes g into φ; Theorem 5 proves trackΓ is a monoid homomorphism (composition does not break tracking). Theorem 7 (soundness invariant): φ(γ) = γ₀ holds around every recoverΓ, so full restoration to the initial state is a structural guarantee.
• Independence and Corollary 21. When two effects' transformation monoids commute, their inverses can be applied in any order—including interleaved multi-component orders. Interfering effects must instead be constrained by ordering theorems (Section 7, Theorem 63).
• Reactive coeffects (spatial). Coeffects become effects, and effects become revertible: dependencies are declared as contracts, and the runtime reacts to providers appearing/disappearing or transferring ownership—rather than each module hand-writing detection and adaptation.
• Unified context Γ∞. The two mechanisms merge into a single context type with hierarchical composition (the literal metaphor of plug/unplug) and an observational equivalence (≃) guarantee; the paper grounds this in a dynamic combination calculus with metatheory.
• Implementation: Cordis. A three-layer meta-framework: a core library (context/effect primitives), a loader handling reconciliation and HMR (hot module replacement), and framework bindings.
• Empirical validation: Koishi. An ecosystem of 4000+ community plugins demonstrates the paradigm at scale—correctness is promoted from "author self-discipline" to a "structural property."
• Positioning. Unlike OS/container orchestration (process granularity) or OSGi/extensionDependencies (declared but untyped dependencies, no in-place cleanup), Cordis manages effects and dependencies at the granularity of the components themselves, preparing the ground for self-evolving systems that can safely modify themselves in place.

Conclusion

The paper's lasting contribution is reframing plugin safety: instead of adding more annotations to a static type system, it moves effect/coeffect structure into the runtime, making installation, uninstallation, and dependency rewiring verifiable operations. For self-evolving agent harnesses especially, this means a system can modify its own components without sawing off the branch it sits on.