A Programming Paradigm for Spatiotemporal Composability

1.1. Dimensions of Composability

• Temporal composability requires completely reversing component modifications upon removal; spatial composability requires structured dependency declaration, discovery, resolution, and lifecycle coordination.Static counterparts use lexical scoping, including RAII and bracket patterns, and module import resolution. Dynamic composition instead involves long-lived, stateful effects outside lexical scopes and dependencies that appear, disappear, or change identity.Source: §1.1 · p. 4

1.2.1. Plugin Systems

• 87 of the top 100 VSCode extensions contain executable code requiring host restarts for removal; only 7 declare dependencies on non-built-in extensions.The deactivate hook runs during host termination, separating cleanup from creation rather than enabling live removal. Fixed host extension points discourage inter-extension dependencies, while exported interfaces are untyped by default and provide no checked structural contract.Source: §1.2.1 · pp. 4–5

1.2.2. Self-Evolving Agent Harnesses

• Self-evolving agent harnesses need temporal and spatial composability to avoid restart-driven state loss, disrupted tasks, broken dependents, and circular dependencies.The envisioned harness generates and deploys component modifications while continuously serving requests. A faulty modification can disable recovery itself, while missing spatial composability leaves modules to adapt to dependency changes through ad hoc mechanisms.Source: §1.2.2 · p. 5

1.2.3. The Coarse-Grained Workaround

• Process-level recovery and service-level orchestration [3] mismatch component granularity, discarding local state and failing to express dependencies between components sharing an address space.Maintaining availability during recovery requires redundant replicas, adding resource overhead. Service-level interactions also incur network overhead where local function calls could suffice.Source: §1.2.3 · pp. 5–6

1.3. Contributions

• Lifting effects and coeffects from compile-time reasoning to runtime yields a language-agnostic foundation for temporal recovery and reactive dependency management.Revertible effects carry explicit inverses held by the runtime; tracking and recovery preserve composition to restore context upon removal. Reactive coeffects classify context changes against declared requirements as activating, deactivating, or neutral, driving component lifecycles.Source: §1.3 · p. 6
• The context paradigm mediates effects and coeffects through one context type, enabling component independence up to observational equivalence.A dynamic-composition calculus combines revertible effects and reactive coeffects into components with operational semantics. Its metatheory carries spatiotemporal composability from individual components to whole systems of interleaved components.Source: §1.3 · p. 6
• Cordis implements the formal model with effect tracking, coeffect resolution, and a declarative component loader supporting configuration reconciliation and hot module replacement.The implementation is a meta-framework for spatiotemporal composability.Source: §1.3 · p. 6

2.1. Effects

• Effect systems annotate result types with algebraic descriptions of possible side effects, enabling compositional reasoning about stateful computations.Moggi’s monadic approach encapsulates effectful computations, lifts pure values, and sequences nested computations. Algebraic effects separate operations from implementations; handlers interpret operations through continuations, which may be invoked zero, one, or multiple times.Source: §2.1 · p. 7

2.2. Coeffects

• Coeffect systems annotate contexts with environmental requirements, including resources, permissions, and services, rather than annotating result types.Comonads provide context extraction and duplication, with Environment and Stream instances modeling fixed environments and temporal data. Graded coeffects quantify variable usage through a pre-ordered semiring, composing requirements sequentially with × and in parallel with +.Source: §2.2 · pp. 7–8

2.3. Relationship to Dynamic Composability

• Temporal composability requires invertible stateful effects, while spatial composability requires declared dependencies resolved reactively against what the environment supplies.Inversion enables undoing a component’s environmental modifications upon unloading; coeffects capture its inter-component dependencies.Source: §2.3 · p. 8
• Dynamic composition requires runtime mechanisms because static effect scopes and predetermined coeffect contexts cannot accommodate components and dependencies that emerge during execution.The proposed shift reifies effect and coeffect structures for direct runtime operation rather than adding further static annotations.Source: §2.3 · p. 8

Section 3.3

• The context paradigm unifies effect and coeffect contexts, mediating every effect and coeffect through a single runtime context.This mediation induces the observational equivalence under which subsequent equalities are interpreted.Source: §3 · p. 9

Section 3.1

• Revertible effects pair each context transformation with an inverse held by the runtime, establishing temporal composability local to one component.This local guarantee stops where other components enter.Source: §3 · p. 9

Section 3.2

• Reactive coeffects classify every context change against a declared dependency, establishing spatial composability local to one component.Like the temporal guarantee, this local guarantee stops where other components enter.Source: §3 · p. 9

Section 3.4

• Effect independence and coeffect commutativity allow distinct components’ effects to interleave without disturbing one another, up to the induced observational equivalence.Section 3.4 establishes these properties to extend beyond the component-local guarantees.Source: §3 · p. 9

3.1.1. Effect Context

• Tracking preserves forward behavior and is a monoid homomorphism, so tracking individual effects agrees with tracking their twisted composite.Twisted composition accumulates inverses in reverse order and uses the identity pair as its unit.Source: §3.1.1 · pp. 9–10
• Tracked effects with valid inverses preserve the soundness invariant, allowing recovery to restore the initial effect context.The effect context pairs the current state with an accumulated inverse; tracking updates both. Recovery applies the accumulator and resets it to the identity.Source: §3.1.1 · pp. 10–11

3.1.2. Effect Functions

• Effect functions return state-specific inverses, overcoming fixed-inverse tracking and providing individual undo operations instead of all-or-nothing recovery.A witnessed effect returning (δ, g) at γ requires only g(δ) = γ, rather than one inverse that works at every state. Returning an inverse at the effect-context level provides the individual undo operation.Source: §3.1.2 · p. 12
• Effect composition forms a monoid, preserves witnesses, embeds uniformly invertible transformation pairs, and is preserved by the effect lift.The unit returns the unchanged context with the identity inverse.Source: §3.1.2 · pp. 13–14
• Lifted undo restores context state and preserves the recovery target, but restores the accumulator only when its inverse works uniformly across states.Lifted forward and inverse maps project to their original context transformations. Undo is itself tracked, with reapplying the forward effect serving as its inverse.Source: §3.1.2 · pp. 13–15

3.1.3. Effect Iterators

• Effect iterators reify sequences into steps yielding a modified context, inverse, and continuation; reverse-order undo restores preceding states while preserving soundness.Each witnessed continuation remains witnessed. Inverses accumulate in application order, so applying the accumulator executes them in LIFO order.Source: §3.1.3 · pp. 15–16
• An iterator is itself an effect, with boundaries between steps exposing the current context and recovery accumulator, matching generator yield.Its continuation is a reified delimited continuation, and a component’s entire loading can be represented as one iterator.Source: §3.1.3 · p. 16
• Revertible effects restore a component’s initial context and give each inverse the state its own application ran against, establishing local temporal composability.Loading runs one iterator and accumulates its inverses; unloading applies that accumulator. These guarantees concern one component’s effects taken by themselves.Source: §3.1.3 · p. 16
• Each effect function explicitly supplies its inverse, effect tracks its effects, and the ⋄ operation composes effect functions while preserving revertibility.A plain effect function embeds as an iterator whose first iteration yields Nothing; notions defined for iterators extend to effect functions through this embedding.Source: §3.1.3 · p. 16
• Reverting outside the accumulator’s imposed order or interleaving other components’ effects requires independence, a condition on effects rather than a property of the construction.Section 3.4 supplies this additional condition for multi-component composition.Source: §3.1.3 · p. 16

3.2.1. Coeffect Context

• The coeffect context is a finite, typed partial dependency map whose registrations are automatically tracked and recoverable through revertible effects.Each key has a specific value type; reads require an existing binding, while registrations require an absent binding. Duplicate provision or absent revocation signals an error without a transition.Source: §3.2.1 · p. 17

3.2.2. Specification and Notification

• Transitions activate components when all declared dependencies become available, deactivate them when satisfaction is lost, and otherwise remain neutral.Activation executes tracked effects; deactivation applies the recovery accumulator. Satisfaction is decidable because context domains are finite, and effect boundaries expose every satisfaction change.Source: §3.2.2 · p. 18

3.2. Reactive Coeffects

• Reactive coeffects guarantee local spatial composability: components activate only with satisfied dependencies, and every context change is classified to detect dependency loss.This local guarantee does not ensure that withdrawal waits for resulting deactivations or that bindings remain stable during activation; those require the global guarantee.Source: §3.2 · p. 17, §3.2.2 · p. 18

3.2.3. Isolation and Interception

• Isolation realms let the same dependency key resolve to different values in different contexts, providing dynamically adjustable, component-specific dependency resolution.Access first maps a logical key to a realm, then retrieves that realm’s value. Isolation derives a context discarded on recovery without changing the shared table, whereas registration remains a revertible effect.Source: §3.2.3 · pp. 19–20
• Interception merges component-declared and context-carried metadata before invoking dependency providers, letting enclosing contexts constrain dependency use without modifying components.Each key uses an associative metadata merge with an identity; context metadata takes priority. Interception derives a context without changing the provider table.Source: §3.2.3 · pp. 19–21

3.3.1. Unified Context

• A recursive unified context combines current state, an effect-reverting accumulator, and dependency information, mediating every interaction between components and their environment.Dependency operations have inverses held by the accumulator, and arbitrary shared mutable state can be encoded as dependency values.Source: §3.3.1 · p. 21
• Context-mediated iterators restrict interactions to key-local operations and binding provisions, guaranteeing that iterators and yielded inverses respect observational equivalence at their stage keys.Operation outcomes select continuations; provision stages install bindings that operations cannot create. Hidden reads are excluded unless their state is represented through a context key.Source: §3.3.1 · p. 22, §3.3.2 · p. 25
• Recursive contexts support arbitrarily nested composition, with parents aggregating child effects and components independently loadable and unloadable across hierarchy levels.Loading executes component effects; unloading reverts them without affecting other running components.Source: §3.3.1 · pp. 22–23

3.3.2. Observational Equivalence

• Observational equivalence identifies values that no finite operation-and-inverse test distinguishes and is the coarsest equivalence respected by every operation.Tests must agree on definedness and yielded outcomes. This replaces physical-state comparison with observation through the operations available at each key.Source: §3.3.2 · p. 23
• Context equivalence compares bindings key by key, forgetting unbound state while preserving dependency satisfaction and reactive change classification.Restricting comparison to a key set additionally forgets bindings outside that set, allowing component-specific claims at the keys named by its declarations.Source: §3.3.2 · p. 24
• Equivalence on maps and iterators is partial: respecting it requires related inputs to produce related outputs, and respect at different key sets need not coincide.Respecting maps descend to the quotient, and related maps induce the same quotient map. Branching on a key outside the selected set can violate restricted respect despite preserving full-context equivalence.Source: §3.3.2 · pp. 24–25
• Recovery guarantees survive replacing state equality with observational equivalence when effects and their yielded inverses respect that equivalence.Every reachable accumulator respects the relation because it composes respecting inverses. The argument also applies to any substituted equivalence using transitivity and respect.Source: §3.3.2 · pp. 24–25

3.4.1. Effect Independence

• Commutation need only be checked between transformation-monoid generators, and effect composition introduces no transformations beyond the monoid generated by its constituents.If every generator of one monoid commutes with every generator of the other, all their elements commute.Source: §3.4.1 · p. 27
• Independence requires commuting transformations, including forward maps and yielded inverses, while foreign transformations preserve each iterator’s yielded inverse and continuation.The transformation monoid includes maps generated by every reachable iteration, not merely the initial forward map.Source: §3.4.1 · pp. 26–27
• Pairwise independent effects can be reverted in any order, each inverse removing only its own contribution and all inverses together restoring the initial state.An inverse remains valid even when later effects have changed the state.Source: §3.4.1 · pp. 27–28

3.4.2. Coeffect Commutativity

• Operations at distinct keys are independent; witnessed coeffects certify independence within each key, including preservation of operation outcomes.The key provider supplies the commutativity proof at definition time, so consuming components need not establish it.Source: §3.4.2 · pp. 28–29
• Commutativity depends on interface observations: uniquely identified registrations commute, ordered middleware does not, and allocation depends on whether handles are observably distinguishable.Opaque handles permit equivalence up to renaming; exposing addresses as equality-comparable outcomes can distinguish allocation orders.Source: §3.4.2 · p. 29
• With witnessed coeffects, the disjointness condition P_1 ∩ S_2 = P_2 ∩ S_1 = ∅ establishes component independence and system-wide temporal composability.Disjointness is checked from component declarations; independence transfers from context-mediated iterators to their lifted effect functions.Source: §3.4 · p. 26, §3.4.2 · p. 30
• The decomposition separates commuting effects from order-sensitive coeffects, establishing composability at component rather than individual-effect granularity.Within a component, the accumulator reverts effects in LIFO order; across components, declared coeffects require provision before dependency satisfaction.Source: §3.4.2 · pp. 30–31
• The theorem requires every shared location to be represented by a context key; locations that cannot be reified as coeffects remain outside its guarantee.This mediation requirement is a programming discipline, not a property enforced by the construction.Source: §3.4.2 · p. 31

• The metatheory establishes global temporal and spatial composability, extending single-component guarantees to every fiber under arbitrary interleavings.Source: §4 · p. 31
• Each component comprises a coeffect specification, a provision, and a witnessed effect function; its instantiations are fibers.Source: §4 · p. 31
• Orchestration rules let the orchestrator insert and retire fibers, while lifecycle rules let the system activate and deactivate them unprompted.Source: §4 · p. 31

Components

• A component combines dependency requirements, permitted provision keys, and a witnessed effect iterator whose inverses withdraw its active effects.Dependencies declare what the component requires from its environment; provisions bound the keys at which its effects may install bindings.Source: §4.1 · p. 31

Fibers

• Fibers are component instances with independent lifecycles comprising Inactive, Reloading, Active, and Unloading states.Each records its component, parent, own coeffect table, and retirement flag; installed states carry an accumulator and a committed view identifying dependency providers. Activation executes effects, while deactivation applies the accumulator to recover the context.Source: §4.1 · pp. 31–32

Registry

• A registry with tree-structured parent pointers identifies fibers using fresh atomic names that survive mutation, following dynamically created local names.Parent pointers and committed views reference these names, which rules compare only for equality; lifecycle rules update one fiber while leaving the others unchanged.Source: §4.1 · p. 32
• Disjoint provisions give each key one possible provider and restrict components with nonempty provisions to one simultaneous fiber.The calculus uses one shared realm; systems needing multiple providers can use separate realms or a broker fiber that dispatches among registered implementations.Source: §4.1 · p. 33
• The coeffect context publishes only Active fibers’ bindings, so dependency satisfaction requires active providers and transitioning fibers provide nothing.Reloading and Unloading fibers read dependencies through their committed views, allowing a fiber to stop providing before its effects have been withdrawn.Source: §4.1 · pp. 32–33
• Effect witnesses inspect dependency and provision bindings across all fibers, including unpublished transition bindings, rather than only the active coeffect context.This holds inverses accountable for removing bindings regardless of lifecycle state, without letting lifecycle-only changes alter the projection. Restoration is required only for the declared dependency and provision interface.Source: §4.1 · pp. 33–34

4.2. The Calculus

• Nine rules separate permitted orchestration actions from automatically triggered lifecycle steps, allowing both kinds of transition to interleave.The rules are nondeterministic and specify no scheduler; results proved over every rule sequence therefore apply to every scheduling policy.Source: §4.2 · p. 34, §4.2.2 · p. 37

4.2.1. Orchestration

• Orchestration requests insertion or retirement without directly setting lifecycle states, enforces one possible provider per key, and permits removal only after safe teardown.Retirement is state-independent; removal requires prior deactivation, removal of children, and an empty binding table so no accumulated inverse or binding is discarded.Source: §4.2.1 · pp. 34–35
• Instantiation inserts a child component and returns retirement—not removal—as its inverse, allowing teardown to cascade through descendants without making parents wait.Unlike conditional removal, retirement remains applicable regardless of lifecycle state. The resulting retired, inactive, empty entry differs from absence only in control fields that the rules cannot distinguish.Source: §4.2.1 · p. 35

4.2.2. Lifecycle

• Lifecycle transitions compare committed and target provider mappings, detecting provider replacement even when values match; retirement or unresolved coeffects makes the target absent.Targets depend only on retirement and coeffect resolution. Quiescence means every fiber has settled at its target, with no transition in progress.Source: §4.2.2 · pp. 35–36
• Activation executes an effect iterator while accumulating inverses in last-in-first-out order; interrupted activation diverts directly into unloading rather than briefly becoming active.L-Begin starts reloading, L-Iter advances an iteration, and L-Finish commits activation. Diversion occurs at iterator boundaries, either aborting the pending iteration or allowing it to land before teardown.Source: §4.2.2 · pp. 36–37
• Guarded deactivation preserves consumers’ dependency access during teardown, while excluding unloading providers from target resolution ensures the withdrawal guard eventually releases.L-Leave stops new resolutions without discarding committed views; L-Unload applies accumulated inverses and finally discards its committed view. The guard tracks actual committed bindings rather than parent–child relationships.Source: §4.2.2 · p. 37

4.2.3. Confinement

• Confinement restricts ordinary effects and their inverses to the fiber’s table and declared coeffect bindings, excluding registry structure, control fields, and unrepresented state.Context-mediated operation, provision, and instantiation stages enforce this discipline. Instantiation exceptionally adds a new entry, while its inverse writes only that entry’s retirement flag.Source: §4.2.3 · p. 38

4.3. Metatheory

• Each step separates confined state transformations from registry edits, restricting cross-fiber table changes to values at the acting fiber’s declared dependency keys.A fiber’s committed provider view remains constant throughout an installed episode, and only unloading applies its accumulated inverse.Source: §4.3 · pp. 40–41
• Observationally equivalent states enable the same rules and remain equivalent after stepping, while bijective fiber renaming preserves execution and well-formedness.Executions differing only in the names their instantiations draw are identified up to renaming.Source: §4.3 · pp. 41–42
• Removing a vestigial entry preserves table observations and other fibers’ transitions, except that removal can enable previously blocked insertions.A vestigial entry is retired, inactive, empty-table, and has no child pointing to it. Removal can enable O-Insert to reuse its name or claim a key from its provision.Source: §4.3 · p. 42

4.3.1. Preservation

• Every calculus rule preserves registry well-formedness, maintaining valid parent pointers, disjoint provisions, and committed dependencies on installed providers.Committed dependency views remain total, and disjoint provisions ensure each key has at most one provider. The unload guard prevents stale commitments, allowing inactive fibers to be removed and their names reused without a separate dependency check.Source: §4.3.1 · pp. 43–44

4.3.2. Temporal Composability

• Every execution is pairwise independent: non-entangled fibers have independent effects, while entangled fibers are handled through commutative shared operations and lifecycle guards.The unload guard pins providers while consumers remain installed. During a fiber’s reloading, steps of entangled fibers have identity state maps.Source: §4.3.2 · pp. 44–45
• Running a fiber’s accumulated inverse withdraws its contribution and nothing else, even when other fibers have changed the state between execution and reversal.The single-accumulator invariant survives interleaving because intervening steps commute with the accumulated inverse.Source: §4.3.2 · pp. 44–45
• Recovery removes a fiber’s episode effects while preserving the table outcomes of interleaved steps by other fibers, up to key-defined equivalence.At episode closure, unloading applies recovery and leaves the fiber’s table empty. Interpreting recovery as if the fiber never began additionally requires that fibers it instantiates take no steps during the interval.Source: §4.3.2 · pp. 46–47
• Recovery restores only key-observable table equivalence, not physical state: allocators need not rewind, heap layouts need not return, and sent messages remain sent.Control fields are excluded from comparison, and state not reified at any key lies outside the calculus.Source: §4.3.2 · pp. 46–47

4.3.3. Spatial Composability

• Dependency ordering starts transitions only when dependencies are provided and postpones provider withdrawal until every dependent using its bindings has deactivated.A dependent’s committed provider resolution remains fixed throughout its episode, which begins after its provider’s episode and closes before it if the provider closes.Source: §4.3.3 · p. 47
• Resolution coherence keeps transition iterations on one committed resolution: completion activates against it, while diversion leads to unloading and recovery.Dependency loss or replacement diverts the transition; a landing diversion may install a stale-resolution effect, which recovery also removes. If execution ends during the transition, only iteration coherence is asserted.Source: §4.3.3 · p. 48

4.3.4. Progress

• S(n) ≤ (K + 3)(V(n) + 1) bounds lifecycle steps per fiber; under the theorem’s assumptions, maximal lifecycle sequences terminate quiescently without deadlock.The assumptions are acyclic precedence, transition lengths at most K, finitely many fiber names, and lifecycle-only steps; V(n) counts target-view changes. Finitely many component programs and bounded branching ensure finite names when direct or indirect recursive instantiation is excluded.Source: §4.3.4 · pp. 49–50

4.3.5. Confluence

• For fixed orchestration inputs, lifecycle confluence makes quiescent states equivalent to loading final active components once in dependency order, without unloading.The claim concerns lifecycle scheduling and transition exits, not different orchestration inputs; each key has only one possible provider.Source: §4.3.5 · p. 51
• Acyclic precedence yields a unique, schedule-independent support set, which equals the active fibers at quiescence when every component is total on its provision.Support requires a nonretired fiber, a supported creator, and supported providers for all declared dependencies. Provision totality requires every completed activation to install all declared provision keys.Source: §4.3.5 · pp. 51–52
• Independent activation steps on distinct fibers commute when both are initially applicable, and activation–orchestration pairs commute when activation does not instantiate the orchestration target.Transposition preserves applicability and reaches the same state in either order.Source: §4.3.5 · p. 52
• Under total provision and quiescence, eligible closed episodes and steps targeting their instantiated fibers can be deleted while preserving final-state equivalence.Eligibility requires that no episode of m with n≺m closes and no fiber instantiated during n’s episode has an episode. Equivalence is ≃_K overall and ≃ outside the instantiated names.Source: §4.3.5 · p. 53
• For components total on their provision, quiescent executions with the same orchestration steps reach equivalent states up to renaming.Together with termination, confluence gives the lifecycle relation unique normal forms.Source: §4.3.5 · pp. 54–55
• Canonical reduction removes closed episodes and makes remaining episodes contiguous in dependency-and-instantiation order while preserving orchestration order.Orchestration steps targeting orchestrator-inserted fibers precede lifecycle steps; those targeting activation-instantiated fibers follow their instantiation. Reduction preserves the endpoint up to withdrawn names.Source: §4.3.5 · pp. 54–55
• Confluence licenses reasoning about a Cordis application as statically assembled, but guarantees its final state rather than its intermediate emissions.Adding, removing, replacing a provider, and undoing the replacement reaches the state of the final composition assembled initially; coeffect scope can be assessed at quiescence.Source: §4.3.5 · p. 55

Asynchrony

• Asynchronous hosts let in-flight iterations finish before deactivation, restricting L-Divert to its landing alternative without sacrificing the calculus’s guarantees or quiescence.In-flight inverses need no analogous restriction: interleaved steps commute with remaining inverses, making interval-spanning deactivation observationally equivalent to one-step application. Deactivation may immediately chain into activation according to the current target view.Source: §4.4 · pp. 55–56

Failure

• Failures roll back accumulated effects, retain an error locally, and block automatic retry; preservation and recovery remain unchanged, but confluence excludes failed fibers.The failing iteration contributes nothing to undo; siblings continue running, and revision reinserts an error-free fiber for retry. State-dependent failures can make schedules reach quiescent states differing only in the affected fiber’s lifecycle state.Source: §4.4 · p. 56

Isolation

• Fixed realm assignments reduce isolation to keys in K × R, allowing identical provisions in different realms while preserving existing rules and results.Runtime realm reassignment changes a fiber’s declared interface and therefore requires configuration revision. Interception needs no extension because access-time metadata changes how bindings are used, not how keys resolve, and disappears with its context.Source: §4.4 · p. 56

Configuration

• Configuration revisions retire, deactivate, remove, and reinsert fibers, reaching the same quiescent endpoint as loading the revised configuration from scratch.Configuration payloads become part of effect functions; disabling only retires, whereas re-enabling instantiates a fresh fiber under the surviving entry identity rather than reversing retirement. Removal proceeds children before parent, dependents deactivate before provision withdrawal and reactivate when provisions return, and optimized revision routes must match the composite’s endpoint.Source: §4.4 · p. 57

5. Implementation and Case Study

• Cordis supplies domain-independent dynamic composition semantics through three tiers: a core library, a component loader, and application frameworks such as Koishi.The loader extends the core with configuration reconciliation and hot module replacement; application frameworks supply domain-specific functionality.Source: §5 · p. 57

5.1. Core Library

• The core library connects theoretical constructs to runtime operations, building effects, reactive coeffects, component lifecycles, and context access from the bottom up.Runtime names distinguish implementation operations from theoretical symbols; @@name denotes a framework-internal symbol key accessing an opaque context slot, not a string-keyed map.Source: §5.1 · pp. 57–58

5.1.1. Effect Tracking

• ctx.effect tracks every context mutation and composes supplied inverses for unloading, but inverse correctness and coeffect commutativity remain component-author obligations.The iterator engine accumulates inverses in LIFO order and checks a guard before each step; disposal stops in-flight iteration and permits recovery at most once. Each disposer is also tracked by its parent context, recursively composing recovery.Source: §5.1.1 · pp. 59–60

5.1.2. Coeffect Operations

• Coeffects resolve keys through realm symbols to stored values, while isolation redirects bindings and interception adjusts access metadata.ctx.set installs a binding whose disposer removes it, with both operations notifying dependents. Isolation and interception derive child contexts without modifying parents, so discarding the child suffices for recovery; isolation provides independent bindings, while new interception metadata takes priority over inherited metadata.Source: §5.1.2 · pp. 60–61
• Binding changes refresh dependent fibers sharing the affected key and realm, activating or deactivating them according to dependency satisfaction.Only ACTIVE providers satisfy dependencies, so entering UNLOADING triggers dependent teardown while the provider’s bindings remain installed. Refresh is idempotent for neutral changes, and notification returns refreshed fibers so callers can await them.Source: §5.1.2 · pp. 60–61

5.1.3. Component Lifecycle

• ctx.use creates hierarchical fibers whose asynchronous reload and unload transitions finish before responding to changed dependency targets.Instantiation binds configuration to the effect function and is itself a parent-tracked effect, so parent unloading cascades to children. Fresh provider identities—not values—determine reloads; iterator-boundary target checks permit partial rollback, completion checks chain transitions, and in-place writes by the same provider are unobserved.Source: §5.1.3 · pp. 61–63
• Cordis preserves dependency access during teardown by retaining committed bindings and waiting for affected dependents to become INACTIVE before reverting a provider’s effects.A provider becomes UNLOADING before any inverse is scheduled, and notification selects dependents whose declared keys resolve to its realm. Waiting precedes the entire recovery; termination follows from waiting only on already-unsatisfied dependents, traversing the provider graph on demand rather than analyzing it beforehand.Source: §5.1.3 · pp. 63–64

5.1.4. Context Access

• Proxy-mediated property access enforces declared coeffects against committed fiber views, preserving dependency reads during teardown rather than merely querying the current store.The proxy walks ancestor fibers, accepting the first committed binding and rejecting unloaded declarations or undeclared keys; bare ctx.get instead returns the stored value or nothing without failing. Because dependency specifications are static, these access violations are also detectable in principle at compile time.Source: §5.1.4 · p. 64

5.2. Component Loader

• The loader realizes persistent configuration entries as fibers, synchronizing changes bidirectionally between entry fields and components.Entries form the authoritative configuration tree: @cordisjs/group loads child entries, while @cordisjs/include grafts external YAML or JSON configurations into nested subtrees.Source: §5.2 · p. 64, §5.2.1 · p. 65

5.2.1. Declarative Configuration

• Incremental reconciliation reaches the final configuration’s quiescent state regardless of operation order, removes departing fibers’ contributions, and permits concurrent module loading without orchestrated dependency ordering.Declarations alone determine which components remain loaded only when every component installs every key it declares. Missing dependencies delay activation rather than module loading, and dependents deactivate before departing providers.Source: §5.2.1 · pp. 65–66
• Field-specific reconciliation chooses minimally disruptive updates rather than rebuilding every changed entry.Identity or URL changes rebuild; isolation changes reassign realms; interception updates in place; disabling unloads and reenabling reloads. Components handle configuration changes themselves, with groups recursively reconciling children through keyed diffs over their identifiers.Source: §5.2.1 · p. 66
• Managed realms support moving entries between groups, using inherited delimiter tags to move owned bindings and identify dependents whose access changes.Local realms remain private to an entry, while named global realms are shared; unreferenced realms are discarded. Dependents retain access when they and the provider move together or both stay, gaining or losing access only when the move separates them.Source: §5.2.1 · pp. 66–67

5.2.2. Hot Module Replacement

• Component-level hot replacement disposes and reinstantiates fibers without restarting the process or requiring developer-annotated acceptance boundaries, unlike Webpack or Vite.Disposing the old fiber withdraws everything the component installed; instantiating a fiber from the reloaded module reinstalls it.Source: §5.2.2 · p. 67
• HMR classifies dependencies, detects stale entries, and transactionally replaces their fibers, restoring caches and previous components if any import fails.Nonreplaceable external modules trigger a full restart; classification accepts modules with an accepted import, declines those whose imports all decline, and defaults unresolved cycles to declined. Stale-entry detection traverses dependencies with declined modules as boundaries, folding stale dependency trees into the accepted set for cache invalidation.Source: §5.2.2 · pp. 67–69

Case study scope

• Over 4000 community-contributed plugins accumulated over four years make Koishi a production-scale case study of Cordis’s dynamic composability.Koishi uses Cordis v3, whereas the paper presents v4 with refined effect and coeffect semantics and a redesigned loader; both share the core compositional model.Source: §5.3 · p. 69

Expressiveness and generality of the meta-framework

• Koishi demonstrates expressiveness and generality: context primitives support its server-side features and independent browser console while leaving domain vocabulary and runtime-specific meanings to applications.Every server feature is a plugin; the console is a separate Cordis application composing browser and user-interface primitives.Source: §5.3 · p. 69

Temporal composability without cognitive overhead

• Context-mediated effects receive automatic, ordered cleanup, allowing plugin removal and hot replacement without authors writing uninstall paths.Console-driven disabling reverts effects in place; development hot replacement preserves cache state and live connections elsewhere in the system.Source: §5.3 · p. 70

Spatial composability across an open ecosystem

• Reactive coeffects coordinate independently authored plugins, reactivating only dependents whose resolved dependencies change and keeping plugins inactive while required dependencies are unavailable.Messaging adapters and database drivers provide capabilities that functional plugins declare as coeffects; authors coordinate through those coeffects.Source: §5.3 · p. 70

Threats to validity

• The single-ecosystem, single-language observational evidence cannot isolate paradigm benefits from TypeScript or Koishi’s domain, and provides no controlled architectural comparison.The result establishes existence and adoption; measuring overhead and developer productivity against a baseline remains future work.Source: §5.3 · p. 70

6.1. System Boundary

• Revertibility is bounded per location by exclusive modification and state restoration: resource acquisition can be tracked, while external emission remains outside the boundary.Coeffects can bring locations inside by restricting access to invertible operations, at a per-access cost. External emissions require withholding until commitment or application-defined compensation; compensation composes in LIFO order, but commutation must be re-established under its coarser equivalence.Source: §6.1 · pp. 70–71

6.2. Service Multiplexing

• A stable service broker supports multiple providers without dependency-triggered consumer reloads, enabling load balancing, rolling updates, and cross-process invocation.Revertible registrations automatically remove unloaded providers from routing; rolling updates load a new provider, shift traffic once ACTIVE, and unload old providers after in-flight requests finish. Cross-process invocation preserves the interface through RPC but requires an asynchronous contract because calls incur latency and may fail mid-flight.Source: §6.2 · pp. 71–72

6.3. Access Control and Sandboxing

• Dependency declarations and interception constrain proxy-mediated access, but untrusted components require an external sandbox because host-runtime access can bypass language-level checks.Declarations expose requested capabilities for load-time approval, resembling capability-based security; context interception adds fine-grained policies that can change without dependency reloads. Sandboxed components receive host dependencies through a transparent bridge whose host-side capabilities can be restricted.Source: §6.3 · pp. 72–73

6.4. Language Independence and Selection

• Language portability requires closures capturing inverses, retractable runtime loading, typed context dependencies, and dynamic access mediation.Managed module registries or native dynamic linking/unlinking support retraction, although ES modules lack public eviction; provider-extended context types support typed dependencies. Transparent interception mediates access, reflection sacrifices type safety and developer experience, and metaprogramming can generate typed accessors without a general interception primitive.Source: §6.4 · pp. 73–74

6.5. Mutual Dependencies and Component Granularity

• Eliminating mutual dependencies may require quadratically many integration components, preserving correctness and runtime performance while increasing configuration and cognitive overhead.Dependency cycles leave components permanently inactive and are detectable from declarations; separating independent cores from directional integration bindings removes cycles and permits selective loading. Package bundling, convention-based wiring, and scaffolding reduce authoring burden without weakening the acyclic model’s guarantees.Source: §6.5 · p. 74

6.6. Dependency Typing and Versioning

• Key-only dependency linking permits interface drift and unrelated key collisions across independently built components; compatibility-preserving versioning remains unresolved.Package-qualified keys prevent collisions but couple identity to registries; Cordis uses peer-version constraints, relying on semantic versioning and generally preventing simultaneous package versions. Structural compatibility handles records more readily than behavioral contracts and becomes undecidable with bounded quantification; unifying these approaches while preserving dynamic composition guarantees remains open.Source: §6.6 · pp. 75–76

6.7. Co-Design with Languages and Operating Systems

• Language co-design could make contexts implicit, prevent cross-context lifecycle escapes, and give compilers direct support for effects and coeffects.Implicit contexts remove explicit context parameters and prevent accidental access to another component’s lifecycle or dependencies, while derived contexts still require a language construct. Effect syntax could consolidate inverse closures into a state-machine frame; typed coeffect specifications could detect cycles at compile time and support structural dependency matching through row types.Source: §6.7 · p. 76
• Operating-system co-design could enforce declared-dependency sandboxes and supply resources as coeffects, consolidating acquisition tracking and expanding reversible operations.Making declared dependencies the entirety of a component’s reach would provide sandboxing, with per-component bindings and access interception. OS-owned resource attribution avoids duplicate tracking; transactional persistent writes and copy-on-write or immutable storage could make additional operations reversible.Source: §6.7 · pp. 76–77

7.1. Effect and Coeffect Systems

• Cordis requires caller-supplied, one-sided inverses for atomic effects rather than the globally invertible computations modeled by Heunen et al..Their categorical account derives two-sided inverses from its structure. Cordis records inverses at runtime when effects are applied and derives composite recovery by composing them, without requiring the entire computation to be reversible.Source: §7.1 · p. 78
• Cordis moves effect and coeffect reasoning from static types into runtime tracking and dependency re-resolution over ordinary host code.ZIO, Effect-TS, and fp-ts require monadic embedding, whereas Cordis overlays ordinary code and re-resolves requirements as providers change. Effekt emphasizes modular interpretation through statically scoped capabilities, with boxing for first-class use; Granule’s graded discipline unifies effects and coeffects at the type level.Source: §7.1 · pp. 77–78

7.2. Programming Paradigms

• The context paradigm attributes operations to components without threading state through every function, but cannot reproduce dynamically scoped context-oriented activation.Compared with explicit State-monad threading and implicit imperative mutation, its language-agnostic overlay retains traceability while leaving other code ordinary. COP changes ambient method dispatch without tracking or reverting effects; Cordis activates through dependency satisfaction and covers only COP’s global, value-driven selection fragment.Source: §7.2 · pp. 78–79
• Unlike AOP, Cordis restricts crosscutting behavior to declared coeffects and integrates changes with component reversion and reactive propagation.Declared dependencies let an orchestrator inspect and govern crosscutting behavior through configuration, rather than through oblivious pointcuts over arbitrary join points. Dynamic-AOP systems also weave and unweave at runtime, but do not bind this operation to component lifecycles or dependent re-resolution.Source: §7.2 · p. 79

7.3. Temporal Composability

• Cordis reloads components by reverting and reapplying tracked effects, enabling complete unloading but preserving local state only when stored in longer-lived dependencies.Forward migration carries state across versions at safe points—quiescence or tranquility —whereas Cordis needs no handwritten migration functions. Unlike developer-authored cleanup, including React’s structurally paired but control-flow-restricted useEffect, Cordis freely composes asynchronous effects and derives composite cleanup from atomic inverses.Source: §7.3 · pp. 79–80
• Cordis recovers component-defined effects across whole lifecycles rather than limiting recovery to statically fixed scopes or platform-recognized resources.Its accumulator applies inverses last-in-first-out and delays provider withdrawal until consumers deactivate; Kim and Rinard’s verified collection operations demonstrate checkable inverse and commutativity obligations, but not lifecycle-wide inverse composition. Interposed reclamation in Nooks, shadow drivers, and Akeso records platform-known acquisitions within restart or request boundaries, whereas Cordis accepts component-supplied atomic inverses and propagates removal to dependents.Source: §7.3 · p. 81

7.4. Spatial Composability

• Cordis extends availability-reactive component activation with accumulated-effect recovery and asynchronous teardown that completes before further lifecycle changes.Initialization-time dependency injection does not reactively re-resolve existing dependents; OSGi Declarative Services and iPOJO do react to availability, but rely on handwritten, synchronous deactivation callbacks. Cordis instead reverts dependent effects and uses an inertial Unloading state to await asynchronous teardown.Source: §7.4 · p. 82
• Cordis’s component-level reactivity complements value-level FRP, but guarantees transition-local dependency consistency rather than glitch freedom.FRP propagates values through dependency-ordered turns, while Cordis adds asynchronous component lifecycle semantics and guarantees that no transition straddles two coeffect resolutions. Coeffects can carry reactive values, allowing components to react only to consumed parts and combine both granularities.Source: §7.4 · p. 82

8. Conclusion

• Revertible effects provide local temporal composability by retaining an inverse for every context transformation, enabling context recovery upon component removal.Both tracking and recovery preserve composition.Source: §8 · p. 82
• Reactive coeffects provide local spatial composability by classifying context changes as activating, deactivating, or neutral against component specifications, driving activation and deactivation.Source: §8 · pp. 82–83
• The context paradigm mediates effects and coeffects through one context type, making distinct components’ effects independent up to observational equivalence.A dynamic-composition calculus carries spatiotemporal composability from individual components to whole systems of interleaved components.Source: §8 · p. 83
• Cordis implements effect tracking and coeffect resolution, alongside a declarative component loader supporting configuration reconciliation and hot module replacement.Source: §8 · p. 83
• Over 4000 community plugins are supported by the production Koishi system, whose case study validates Cordis’s design.Source: §8 · p. 83
• Future validation targets self-evolving agent harnesses, testing complete recovery during rapid component replacement and dependency coordination under frequent topological change.This proposed setting involves agents continuously generating and replacing their own harness components with little human oversight; its validation remains future work.Source: §8 · p. 83