A Programming Paradigm for Spatiotemporal Composability

1. The Problem the Paper Is Actually Solving

Most composition mechanisms assume that the set of parts is fixed before execution:

• function calls and module imports are resolved statically;
• dependency injection wires objects during initialization;
• lexical scopes, RAII, and bracket-style APIs release resources when a known scope ends.

Modern plugin hosts and potentially self-evolving agent harnesses violate that assumption. Components may be inserted, removed, replaced, or reconfigured while the process remains alive. Restarting a process or container is a coarse substitute, but it destroys unrelated process-local state such as caches, connections, and in-flight computations. It also manages composition at the wrong granularity when the actual components share one address space.

The authors isolate two distinct requirements:

Dimension	Question	Static analogue	Dynamic difficulty
Temporal composability	Can a component be removed and its contribution completely withdrawn?	Lexical scope, RAII, bracket	A plugin’s lifetime is long-lived and not lexically delimited; cleanup may be partial, asynchronous, or interleaved with other components.
Spatial composability	Can a component declare what it needs and react correctly when providers change?	Module imports, initialization-time DI	Dependencies may appear, disappear, or resolve to different providers while the program runs.

The important conceptual move is to connect these requirements to the dual vocabulary of programming-language theory:

• an effect describes how a computation changes its environment;
• a coeffect describes what the computation requires from its environment.

Classical effect and coeffect systems are normally static analyses over fixed program text. This paper reifies both as runtime data and runtime operations.

Motivating failure modes

The paper uses VSCode extensions as a representative plugin architecture. Executable extensions share an extension-host process and generally cannot be removed live; disabling one requires restarting the host. Cleanup is separated into a deactivate hook, so an author must manually remember every effect created elsewhere. Inter-extension APIs are also weakly structured and dependencies are uncommon.

The more forward-looking example is a self-evolving agent harness. If an agent can synthesize and replace its own tools, memory systems, sandboxes, or orchestration modules, full restarts repeatedly destroy useful state, while ad hoc replacement can leak resources or silently break dependents. The paper proposes Cordis as a possible foundation for this scenario, but does not evaluate an autonomous agent harness.

2. Core Intuition: Make the Environment a First-Class Context

The paradigm requires every interaction between a component and shared system state to pass through a context. That context has two jobs:

1. record each mutation together with the operation that reverses it;
2. hold the typed dependency bindings against which component requirements are resolved.

This gives a useful operational picture:

• plugging in a component executes context-mediated effects and accumulates their inverses;
• unplugging it runs those inverses and withdraws the bindings it supplied;
• a component is active only while its declared coeffects resolve to a stable set of providers;
• a dependency change triggers deactivation and, if a suitable provider is available, later reactivation.

The proposal therefore goes beyond hot code replacement. It defines when the old component’s semantic contribution to shared state has been removed and when the new dependency topology is coherent.

3. Revertible Effects: Temporal Composability

3.1 Effect context and inverse accumulation

Let $\Gamma$ be the system context. An ordinary effect is a transformation $\Gamma \to \Gamma$. A revertible effect instead returns both the successor state and an inverse:

$$\mathcal{E}_\Gamma = \Gamma \to \Gamma \times (\Gamma \to \Gamma).$$

If applying $e$ at $\gamma$ yields $(\delta, g)$, the required witness is local to that application:

$$g(\delta) \simeq \gamma.$$

The equivalence $\simeq$ is observational rather than necessarily physical equality. For example, freeing an allocation need not recreate the allocator’s exact heap layout; it must restore everything observers can distinguish through the context’s published operations.

The runtime stores an effect context

$$\partial\Gamma = \Gamma \times (\Gamma \to \Gamma),$$

whose first element is the current state and whose second is the accumulated recovery function. When an effect applies a forward map $f$ and yields inverse $g$, the current state becomes $f(\gamma)$ and the accumulator becomes $\varphi \circ g$. New inverses are therefore prepended so recovery naturally runs in last-in-first-out order.

This construction has two essential compositional properties:

• sequential effects form a monoid: the forward transformations compose in execution order and their inverses compose in the opposite order;
• tracking preserves composition, so the runtime can derive the inverse of a compound effect from the inverses of its atomic operations.

The author of a composite component does not write a separate teardown routine. Each atomic context operation supplies its inverse locally; the runtime builds the component’s teardown program automatically.

3.2 What LIFO recovery does and does not prove

For one component, reverse-order recovery is sufficient: each inverse encounters the state produced by its own forward operation. This yields local temporal composability.

Multiple components are harder. Suppose component $A$ changes the context, then $B$ changes it, and the system removes $A$ before $B$. $A$’s inverse now runs against a state altered by a foreign effect. Correctness requires independence:

1. every forward map and every possible yielded inverse of one component commutes with every transformation of the other;
2. moving the state with one component’s transformations does not change which inverse or continuation the other produces.

Under pairwise independence, any component can be withdrawn from an interleaved execution without erasing another component’s contribution. Within a component, noncommuting effects remain safe because its own accumulator imposes LIFO order. Across components, order-sensitive interactions must be made explicit as dependencies rather than left as supposedly independent effects.

This distinction is central to reading the paper correctly: the runtime’s accumulator alone does not make arbitrary shared mutations composable. Global recovery relies on a discipline that makes shared state context-mediated and cross-component operations independent, usually by assigning separately commuting operations to separate coeffect keys.

4. Reactive Coeffects: Spatial Composability

4.1 Typed dependency context

The coeffect context is a finite typed partial map:

$$\Sigma = (k : K) \rightharpoonup \mathcal{V}_k,$$

where every dependency key $k$ has a corresponding value type $\mathcal{V}_k$. The primitive operations are:

• get(k), which reads an existing binding;
• set(k, v), which installs a previously absent binding and yields deletion of that binding as its inverse.

Because set is itself a revertible effect, dependency provision and effect recovery are not separate mechanisms. Loading a provider installs its binding; unloading it automatically withdraws that binding.

A component declares a dependency specification $d \subseteq K$. A state satisfies it when all named keys are bound:

$$\sigma \vDash d \iff \forall k \in d,\; k \in \operatorname{dom}(\sigma).$$

Every context transition is classified relative to $d$:

• activating: unsatisfied before, satisfied afterward;
• deactivating: satisfied before, unsatisfied afterward;
• neutral: satisfaction does not change.

This notification rule yields local spatial composability: a component begins activation only when all dependencies exist, and any loss of satisfaction is noticed where it occurs.

4.2 Isolation and interception

The flat key-value model is extended in two ways.

Isolation adds a key-to-realm mapping $\rho$. A logical key first resolves to a realm and then to the realm’s value. Different subcontexts can therefore bind the same logical dependency to different providers. This supports tenants, tests, or component sandboxes without globally renaming keys.

Interception associates monoidal metadata with access to a key. Metadata declared by the component and metadata imposed by its surrounding context are merged before the provider is invoked. This supports cross-cutting policies such as logging, tracing, or path-level filesystem permissions without changing either consumer or provider. Context-imposed metadata takes precedence, letting an orchestrator constrain a component.

Isolation and interception derive child contexts rather than mutating the shared table in place, so recovery consists of discarding the derived context.

5. The Unified Context Paradigm

The effect and coeffect contexts are unified recursively as

$$\Gamma_\infty = \mu\Gamma.\; \Gamma \times (\Gamma \to \Gamma) \times \Sigma.$$

Intuitively, a context contains:

• a parent or underlying context state;
• an accumulator that recovers the effects at this level;
• a coeffect table carrying the dependencies visible at this level.

The recursive shape permits hierarchical composition: a component receives a child context, child effects accumulate into that context, and the parent’s teardown can retire descendants without conflating their local lifecycles.

Observational equivalence supplies practical independence

Physical equality is usually too strong for recovery. The paper therefore constructs context equivalence from the interfaces published by its coeffect keys. Two values at a key are indistinguishable if every finite test built from that key’s allowed operations is defined in the same cases and yields the same outcomes. Contexts are equivalent when they expose the same keys with equivalent values.

This serves two purposes:

1. internal state with no observable binding can be forgotten, allowing realistic operations such as allocation/free to count as recovery;
2. operations on distinct keys are independent by construction because each reads and writes only its own binding.

For a shared key, the provider is responsible for exposing a commutative interface if independently authored consumers should be freely interleavable. A registration table whose entries can be inserted and removed independently is the canonical example. An ordered middleware chain is not commutative; its order must instead be represented explicitly by component dependencies or another coordinating abstraction.

The paradigm thus divides computation into:

• commuting, locally reversible actions carried by effects;
• order-sensitive relationships carried by coeffects and lifecycle ordering.

6. Components, Fibers, and the Dynamic-Composition Calculus

6.1 Component and fiber model

A component is a triple

$$\mathcal{C}_\Gamma = \mathcal{D}_\Gamma \times \mathcal{P}_\Gamma \times \mathcal{E}^{*}_\Gamma,$$

containing:

• $d$: required dependency keys;
• $p$: keys the component may provide;
• $e$: a witnessed, revertible effect program executed on activation.

An instantiated component is a fiber. Besides $d$, $p$, and $e$, a fiber records its parent, its own provision table, whether it has been retired, its lifecycle state, its accumulated inverse, and the committed view mapping every declared key to the provider fiber chosen when activation began.

The registry is a tree of fibers. In the core calculus, provisions of different fibers are disjoint, so a key has at most one provider. Isolation realms and broker components relax this in the implementation without changing the basic lifecycle idea.

6.2 Target versus committed view

For every fiber, the runtime continually computes a target view:

• $\bot$ if the fiber is retired or any requirement is currently unsatisfied;
• otherwise, a map from each required key to its current provider fiber.

The committed view records what the component actually activated against. A mismatch means the fiber is stale even if all dependency keys remain present—for example, when a database key now resolves to a replacement provider. The lifecycle is driven by comparing these two views.

6.3 Lifecycle states

The realistic calculus uses four states:

Inactive -> Reloading -> Active -> Unloading -> Inactive
                 |                       |
                 +------> Unloading <----+

• Inactive: no installed effects; may also carry a recorded failure.
• Reloading: activation is executing incrementally and accumulating inverses.
• Active: activation completed against the committed dependency view.
• Unloading: the fiber has stopped serving new dependents but retains its committed dependencies until teardown completes.

External orchestration can insert a fiber, retire it, and remove it once inactive and childless. Retirement requests deactivation; it never directly discards an active fiber, because doing so would lose its accumulator and leak effects.

6.4 The subtle withdrawal protocol

The hardest spatial property is safe provider withdrawal. If provider $A$ supplies key db to consumer $B$, $B$ may need the database during its own teardown—for example, to return connections. Therefore $A$ cannot delete the binding before $B$ finishes, but $B$ must immediately stop being considered satisfiable so new work does not start.

The calculus separates those moments:

1. $A$ enters Unloading and immediately stops counting as an active provider.
2. This changes $B$‘s target, so $B$ also enters Unloading.
3. $B$ retains its committed view and may continue using $A$‘s binding throughout teardown.
4. $A$’s final inverse is guarded by not relied: it waits until every installed consumer that committed to $A$ has become inactive.
5. Only then does $A$ withdraw its binding and finish recovery.

This produces a nested lifetime property: providers activate before their consumers and finish deactivation after them. If a replacement provider appears while $B$ is leaving, $B$ completes its current teardown, becomes inactive, and then activates afresh against the new provider.

6.5 Iteration, asynchrony, and failure

Activation is modeled as an effect iterator. Every iteration yields a successor state, an inverse, and an optional continuation. This gives the runtime interruption points between atomic effects. If the target changes at a boundary, it stops activation and reverts only the prefix already installed.

An asynchronous iteration has inertia: once launched, it must land. If the dependency target changes while it is in flight, its result is accepted, its inverse is added to the accumulator, and the fiber immediately routes into unloading. The system never briefly advertises it as active against a stale view.

If an iteration raises an error, the fiber also routes through unloading, reverts the successful prefix, and records the error in its inactive state. Failure is local to that fiber rather than propagated to siblings. A failed activation therefore contributes nothing to shared state, although failure can make different schedules end with different fiber-status outcomes.

7. What the Metatheory Guarantees

The major results are best read together with their assumptions.

Result	Informal meaning	Important conditions
Preservation	Every lifecycle rule preserves registry well-formedness: parent pointers remain valid, provisions remain disjoint, committed views name real installed providers.	Effects are confined to their owning fiber; the guarded unloading protocol is used.
Recovery exactness	Removing one fiber from an interleaved execution leaves the state that the other fibers’ same steps would have produced without that fiber’s effects.	Correct inverses and pairwise-independent effect iterators; registrations by the removed fiber require special handling.
Terminal recovery	A completed, diverted, or failed episode leaves no effect contribution behind; removal of the inactive fiber also leaves nothing.	Same as recovery exactness.
Dependency ordering	A consumer activates only after its provider; the provider outlives the consumer; the consumer sees a stable binding throughout its episode, including teardown.	Committed views and the not relied guard.
Resolution coherence	All completed iterations of one activation run against one dependency resolution. A stale in-flight iteration is immediately recovered rather than committed as active.	Target checks at iteration boundaries and inertial transition semantics.
Progress / termination	A non-quiescent state always has a lifecycle step, and lifecycle processing reaches quiescence.	Acyclic provider relation, finitely many fibers, and a uniform finite bound on iterator length.
Confluence	With the same orchestration inputs, scheduling and lifecycle interleaving do not change the final quiescent state. The result equals loading the final supported components once in dependency order.	Pairwise independence, acyclic dependencies, total provision, no failed fibers, and the progress assumptions.

The confluence result is the paper’s strongest payoff. It licenses reasoning about a dynamic Cordis application as if it had been assembled statically from its final configuration. A history containing addition, replacement, removal, and reversal of replacement leaves no trace in the final observable state—subject to the hypotheses above. The claim concerns state, not irreversible outputs emitted during the history.

8. Cordis: Theory Realized as a Meta-Framework

Cordis is a TypeScript meta-framework: it supplies composition semantics but no application-domain vocabulary.

8.1 Core effect API

ctx.effect(callback) is the sole context-mutation primitive. The callback may be a single effect or an iterator that yields inverses. The runtime:

• executes it while a guard remains valid;
• prepends each yielded inverse to a composite disposer;
• makes disposal idempotent by disarming it after the first call;
• composes a child disposer into its parent’s disposer.

This directly realizes LIFO inverse accumulation and hierarchical recovery. The library does not verify that a supplied inverse is correct; the effect author must meet that proof obligation.

8.2 Coeffect API and notification

• ctx.set(key, value) installs a binding through ctx.effect, so deletion is tracked automatically.
• ctx.get(key) performs reflective lookup.
• ctx.isolate(key, realm) derives a child context with different key resolution.
• ctx.intercept(key, metadata) derives a child context that modifies access metadata.

Setting or deleting a binding notifies live fibers whose declarations include the key in the same realm. Their targets are recomputed, and only affected fibers transition.

8.3 Component lifecycle in code

ctx.use(component, config) creates a fiber and registers it as an effect of the parent. The implementation keeps:

• fiber.target: the current desired provider view;
• fiber.committed: the view the current activation uses;
• fiber.dispose: the accumulated inverse;
• fiber.inertia: the asynchronous transition in flight.

refresh compares target and committed state, while mutually recursive reload and unload functions ensure that an in-flight transition completes before reacting to another change. A provider is marked UNLOADING before its recovery task is scheduled, and its unload waits for notified dependents to drain before running its own disposer.

Proxy-mediated ctx[key] access walks the fiber ancestry and authorizes access only through a committed declaration. It rejects undeclared access and preserves access to the committed provider during teardown. This is capability-like mediation, but not a security sandbox against malicious code that can bypass the proxy and reach host objects directly.

8.4 Declarative loader and reconciliation

The loader represents a desired application as a tree of entries. Each entry records stable identity, module URL, isolation, interception, component configuration, and whether it is disabled. Configuration changes are reconciled with the least disruptive operation:

• identity or URL change rebuilds the fiber;
• isolation reassigns realms and notifies only fibers that gain or lose the moved binding;
• interception changes in place;
• configuration is delegated to the component for diffing;
• disabled unloads or reloads the fiber.

Nested group and include components are ordinary fibers, so configuration trees stay inside the same lifecycle calculus.

8.5 Hot module replacement

Cordis HMR has three phases:

1. Classify modules as accepted or declined from changed files and non-replaceable externals; unresolved import cycles default to declined.
2. Detect stale entries whose transitive dependency trees intersect accepted modules.
3. Transactionally reload by backing up and invalidating module caches, disposing stale fibers, importing new modules, and recreating their fibers. If import fails, caches and old fibers are restored.

Unlike Webpack/Vite-style HMR, the component fiber itself is the acceptance boundary, so authors do not declare a separate HMR path. Cordis resets a component from its tracked effects; it does not perform dynamic-software-update-style migration of the component’s private in-memory state unless that state lives in a longer-lived dependency.

9. Case Study: Koishi

Koishi is an open-source chatbot framework built on Cordis. The paper reports more than 4,000 community plugins developed over four years, including messaging adapters, database drivers, administration consoles, and end-user features. Its server and browser-based web console are separate Cordis applications, suggesting that the core abstraction is not tied to one runtime domain.

The case study supports two qualitative claims:

• Expressiveness: a full production framework can be built from context-mediated effects and coeffects, with the host supplying only domain vocabulary.
• Open-ecosystem composability: independently authored plugins can declare platform and storage dependencies, remain inactive when these are absent, and be selectively reactivated when providers change.

Its evidentiary limits matter:

• production Koishi currently uses Cordis v3, whereas the paper formalizes and redesigns Cordis v4;
• the evidence comes from one TypeScript ecosystem and is observational, not a controlled comparison;
• there are no performance, memory-overhead, latency, failure-injection, or developer-productivity measurements.

The case study is therefore an existence-and-adoption argument, not an empirical validation of every v4 theorem or implementation claim.

10. System Boundary: What Can Actually Be Undone?

Revertibility depends on what is inside $\Gamma$.

• A location is inside the system boundary when the runtime exclusively controls it and can restore its prior observable state.
• It is outside when another actor may modify it or when no inverse can restore it.

The paper distinguishes two stages of many external operations:

• acquisition creates a recoverable internal record: open returns a descriptor closed by close; malloc returns a block released by free; fork creates a child terminated by kill;
• emission sends information beyond the boundary: bytes written to a shared file, a sent network packet, a published message, or a real-world charge.

Acquisition can be tracked as a revertible effect. Emission generally cannot. Recovery must instead either withhold the emission until commit or execute a domain-specific compensation such as deleting a created object or refunding a charge. Compensation may compose in LIFO order, but the paper’s exact-recovery metatheory does not automatically transfer to it.

This boundary is especially important for agent harnesses: Cordis could retract a generated tool’s registrations, resources, and dependency bindings, but it cannot unsend messages, erase information already observed by an external service, or make untrusted code safe. Those require commit protocols, compensation, sandboxing, and authorization in addition to composability.

11. Broader Design Implications

Service multiplexing

The base calculus gives a key one provider. Multiple implementations can be handled either by exclusive rebinding or by a stable broker coeffect. A broker can multiplex providers for load balancing, rolling updates, or remote invocation while shielding consumers from churn in individual backends.

Access control versus sandboxing

Declared coeffects resemble capability requests, and interception can enforce fine-grained per-component policy. However, this protects only mediated access by benign code. Untrusted components still require a process, VM, WebAssembly, software-fault-isolation, or similar boundary.

Dependency cycles

A cycle leaves all participating components inactive because none can satisfy its dependencies first. The authors recommend factoring bidirectional interactions into dependency-free cores plus unidirectional integration components. This preserves acyclicity but may create quadratically many integration components and more configuration overhead.

Type and version compatibility

The formal model links dependencies by key identity. Independent compilation introduces interface drift and key collision. Cordis currently relies on npm peer dependencies and semantic versioning. Stronger options include namespaced keys or runtime/compile-time structural compatibility, but behavioral and polymorphic compatibility is difficult and remains open.

Language and OS co-design

A host language could make context implicit while keeping it unforgeable, check coeffect specifications statically, detect cycles at compile time, and compile effect iterators without allocating one closure per inverse. An operating system could expose memory, descriptors, files, and other resources as coeffects, attribute acquisitions directly to components, and enforce the declared dependency set as the component’s complete authority.

12. Relationship to Existing Approaches

Approach	What it already provides	What Cordis adds or trades away
RAII / lexical resource management	Reliable cleanup at a statically known scope	Arbitrary runtime component lifetimes and cross-component dependency coordination; loses compile-time enforcement in the library implementation.
Transactions / reversible computation	Automatic rollback inside a predefined transactional or reversible scope	Long-lived, component-scoped recovery with caller-supplied one-sided inverses; cannot automatically undo external emissions.
Conventional DI	Typed or named dependencies resolved at initialization	Reactive re-resolution, deactivation on provider loss, and provider replacement during execution.
OSGi / iPOJO	Services and availability-reactive components	Structurally accumulated inverses and asynchronous, dependency-ordered teardown; Cordis still trusts atomic inverse correctness.
React useEffect	Effect and cleanup colocated	Freely composable nested/conditional/iterated and asynchronous effect sequences, with a derived composite inverse.
Dynamic software updating	Migrates private state from an old version to a new one	Complete component removal and clean reapplication without hand-written migration; private state is reset unless externalized.
FRP / signals	Fine-grained value propagation and, in some systems, glitch freedom	Component-level asynchronous lifecycle and resource recovery; does not offer a global reactive turn or equivalent glitch-freedom guarantee.

13. Critical Assessment

Strongest contributions

1. A clean decomposition of dynamic composition. Temporal and spatial composability are independent enough to reason about separately but fit naturally through effects and coeffects.
2. Local inverse pairing. Cleanup is attached to each atomic mutation, so teardown of an arbitrary composite is derived rather than separately authored.
3. The committed-view/target-view distinction. Tracking provider identity—not merely whether a key exists—makes replacement and stale asynchronous activation precise.
4. A correct teardown ordering story. Marking a provider unavailable before withdrawing its binding, then draining consumers while preserving their committed access, addresses a subtle problem many plugin frameworks leave implicit.
5. A serious metatheory-to-runtime mapping. The implementation table and algorithms expose where each abstract rule appears in the library instead of presenting the formalism and framework as unrelated artifacts.
6. Confluence as a useful engineering contract. Under its assumptions, the final dynamic system can be understood as the static assembly of its final supported components.

Main limitations and open questions

1. The crucial witnesses are trusted. Cordis cannot verify that an inverse truly recovers its effect, respects observational equivalence, or is safe at all relevant states.
2. Independence is a strong global condition. Cross-component transformations must commute and must not alter each other’s yielded inverses or continuations. The paper gives a coeffect discipline that can establish this, but the TypeScript library does not enforce that every shared location is reified or every key interface is commutative.
3. The system boundary excludes many consequential actions. Network sends, shared-file writes, messages, and real-world actions need withholding or compensation, which sit outside the strongest theorems.
4. Progress excludes cycles and unbounded self-expansion. The provider relation must be acyclic, iterator length bounded, and the number of generated fibers finite. Self-evolving systems could violate the last assumption directly.
5. Confluence excludes failure. Different schedules may cause a context-sensitive operation to fail in one execution and succeed in another. Recovery still removes the failed fiber’s partial contribution, but final lifecycle status can diverge.
6. No quantitative evaluation. The paper does not measure steady-state overhead, notification cost, HMR latency, recovery time, or the effect of thousands of fibers and dependency edges.
7. The case study is one version behind the formal design. Koishi demonstrates that the core model is viable, but not that the exact Cordis v4 algorithms have seen equivalent production exposure.
8. State replacement is not state migration. Clean reapplication is simpler and safer, but components with important private state must externalize it or add a separate migration layer.
9. Dependency compatibility remains nominal. Key equality alone is insufficient for independently versioned ecosystems.

14. A Compact Worked Example

Assume three components:

• database provides db;
• web requires db, provides routes, and registers route handlers through revertible effects;
• metrics requires routes and instruments them.

Loading occurs in dependency order even if all fibers are inserted concurrently:

1. database activates and installs db.
2. web’s specification becomes satisfied; it commits to the database provider, registers its handlers, and installs routes.
3. metrics commits to the routes provider and installs instrumentation.

If the database is replaced:

1. the old database becomes unavailable as a provider but retains its actual binding;
2. web sees a changed target and enters unloading, but can still use its committed db while closing connections and reversing handlers;
3. metrics similarly unloads before web can finish withdrawing routes;
4. after metrics is inactive, web removes routes; after web is inactive, the old database removes db;
5. once the replacement database is active, web and then metrics activate against the new provider chain.

If all effects meet the independence and inverse conditions, the resulting state is observationally the same as starting a fresh process with only the replacement database, web, and metrics configured.

15. Bottom Line

The paper’s deepest idea is that dynamic composition should be a property of the programming model, not a convention built from optional unload hooks. A component must make both sides of its relationship with the world explicit: what it changes and what it needs. Revertible effects make the first recoverable; reactive coeffects make the second continuously resolvable. The calculus shows that, with disciplined mediation and explicit ordering assumptions, this local structure scales to a whole interleaved system.

Cordis is compelling as a blueprint for plugin hosts and continuously reconfigured runtimes. Its formal results should not be read as automatic guarantees for arbitrary TypeScript code: they describe the contract a compliant context, effect library, component author, and dependency interface jointly uphold. The most valuable future work is therefore enforcement and measurement—making inverses, confinement, commutativity, dependency compatibility, and authority less dependent on convention, then quantifying what that discipline costs in real systems.