PaperlayerView exact revision on arXiv

Source-linked AI summary

A Programming Paradigm for Spatiotemporal Composability

Yifan Shi, Wei Zhang, Tianyi Cui

arXiv:2608.25512v1cs.PLcs.SE

TL;DR

Dynamic composition lacks fully developed foundations for reversible effects and reactive dependencies. This paper unifies both mechanisms in a context paradigm and calculus, with Cordis realizing them and supporting termination and production-scale validation.

  • Problem

    Component ecosystems can link dependencies by key identity alone, leaving independently developed components vulnerable to incompatible interfaces and unpredictable failures.

  • Method

    The paper combines inverse-held effect tracking, coeffect-driven lifecycle management, and a unified context into a calculus and Cordis framework for dynamic composition.

  • Results

    The metatheory establishes composability for interleaved components and guarantees that lifecycle sequences terminate in quiescent states.

  • Takeaways & Limitations

    Cordis provides a practical framework for effect tracking, coeffect resolution, configuration reconciliation, and hot module replacement in dynamically composed systems.

  • Takeaways & Limitations

    Reversion is bounded by observational equivalence and cannot restore unreified physical state, including monotone allocation, heap layout, or already-sent messages.

Abstract

from arXiv · show

Modern software -- from plugin systems to self-evolving agent harnesses -- increasingly requires dynamic composition, yet its formal foundations remain underdeveloped. We identify two orthogonal dimensions of the problem: temporal composability, the ability to completely revert a component's side effects upon removal, and spatial composability, the ability to declare and reactively manage inter-component dependencies. We address the two dimensions by lifting classical effect and coeffect concepts to runtime mechanisms. In particular, we formalize revertible effects, in which every context transformation carries an inverse that the runtime holds, establishing temporal composability local to one component. We formalize reactive coeffects, in which every context change is classified against a component's coeffect specification to drive its activation and deactivation, establishing spatial composability local to one component. We then unify the effect context and the coeffect context into a single context type and mediate every effect and coeffect through it, yielding a discipline we call the context paradigm; the mediation induces an observational equivalence up to which the effects of distinct components interleave without disturbing one another. Combining these mechanisms into the notion of a component, we give a calculus of dynamic composition whose metatheory carries spatiotemporal composability from a single component to a whole system of interleaved components. We implement these ideas in Cordis, a meta-framework of spatiotemporal composability that provides a core library with effect tracking and coeffect resolution, as well as a declarative component loader with configuration reconciliation and hot module replacement.

1. Introduction

Dynamic composition requires fine-grained runtime support for both reversing components’ environmental modifications and managing dependencies that appear, disappear, or change. The paper addresses these dimensions by extending effect and coeffect ideas into revertible effects and reactive coeffects for local temporal and spatial composability.

  • Motivation: Modern software increasingly needs components loaded, unloaded, and reconfigured at runtime, but traditional composition remains fixed through compile-time calls, imports, and inheritance.Plugin architectures and self-evolving agent harnesses motivate this shift toward dynamic composition.
  • Problem: Dynamic composability has two orthogonal requirements: completely reversing a removed component’s environmental modifications and declaring, discovering, and resolving changing inter-component dependencies.Temporal composability requires orderly reclamation of allocations, registrations, and mutations; spatial composability handles dependencies that appear, disappear, or change identity.
  • Problem: Plugin systems expose both limitations: VSCode cannot unload executable extensions without restarting its shared host, while only 7 of its top 100 extensions declare non-built-in extension dependencies.Among those extensions, 87 contain executable code and therefore require a restart upon removal; these limitations recur across plugin systems generally.
  • Problem: Process and container restarts provide only coarse-grained substitutes, discarding accumulated state, requiring redundant replicas, and failing to express dependencies among components sharing an address space.Rebuilding state after restarts takes seconds to minutes, while service-level orchestration cannot replace component-level composition.
  • Contributions: The paper formalizes revertible effects, attaching runtime-held inverses to context transformations so component removal recovers context and establishes local temporal composability.Effect systems provide the existing vocabulary for environmental modifications, but prior formulations focus on compile-time analysis over lexically fixed scopes.
  • Contributions: It also formalizes reactive coeffects, specifying component requirements and classifying each context change to activate or deactivate components, establishing local spatial composability.Coeffect systems formalize environmental requirements, but existing formulations do not extend to dynamic runtime composition.

2. Preliminaries

This section introduces effects as descriptions of how computations modify their environment and coeffects as descriptions of their environmental requirements, establishing the theoretical basis for dynamic composability. It motivates reifying both as runtime mechanisms because static scopes and compile-time contexts cannot support components that arrive, depart, and interact with evolving contexts at runtime.

  • Effect systems: Effect systems annotate computation types with effect-algebra elements describing possible side effects, enabling compositional reasoning about stateful computations.The STLC judgment Γ ⊢ t: T is refined to record computational effects; Lucassen and Gifford introduced a kinded system distinguishing types, effects, and regions for parallel-program scheduling constraints.
  • Coeffect systems: Coeffect systems annotate contexts with requirements on environmental resources, permissions, or services, complementing effects’ account of computational impact.Effects model how a program changes the world, whereas coeffects model the world’s constraints on the program.
  • Dynamic composability: Temporal composability requires stateful environmental transformations to be invertible for reversion on unloading, while spatial composability requires dependencies to be declared and resolved reactively.These requirements correspond respectively to the effect and coeffect directions of dynamic composition.
  • Dynamic composability: Classical effects and coeffects are static: effects use lexically fixed scopes and compile-time handlers, while coeffects rely on contexts determined before execution.Such mechanisms cannot directly guarantee composability for runtime-loaded or unloaded components operating against continuously evolving contexts.
  • Dynamic composability: The paper therefore reifies effect and coeffect structures so the runtime can operate on them directly and establish their guarantees dynamically.This shifts the approach from adding further static annotations to making the underlying conceptual structures runtime mechanisms.

3. Revertible Effects and Reactive Coeffects

This section lifts effects and coeffects into runtime mechanisms for dynamic composition by reifying typing contexts as first-class, runtime-operable context types. It establishes temporal composability locally by pairing each effect transformation with a runtime-held inverse.

  • 3. Revertible Effects and Reactive Coeffects: The section turns effect and coeffect typing contexts into first-class context types that can operate at runtime.This reification provides the foundation for a theory of dynamic composition.
  • 3.1 Revertible Effects: Each effect is modeled as a context transformation paired with an inverse retained by the runtime.This mechanism establishes temporal composability locally to a single component.
  • 3. Revertible Effects and Reactive Coeffects: The section develops runtime mechanisms from the effects and coeffects introduced earlier, constructing a theory of dynamic composition.

3.1. Revertible Effects

Revertible effects make component side effects trackable and recoverable by pairing each context transformation with an explicit inverse. The resulting mechanism provides local temporal composability, while addressing state-dependent inverses and selective reversion through enhanced effect constructions.

  • 3.1. Revertible Effects: Revertible effects pair each context transformation with an explicit inverse, allowing a component’s accumulated side effects to recover the context state it initially encountered.An effect has type Γ → Γ × (Γ → Γ), and the accumulator stores composite inverses for recovery.
  • 3.1. Revertible Effects: The tracking transformation preserves forward behavior while composing inverses, and its monoid homomorphism property makes sequentially tracked effects equivalent to tracking their twisted composite.This supports reasoning about an entire effect sequence as one tracked effect.
  • 3.1. Revertible Effects: Recovery applies the accumulated inverse and resets it, with the soundness invariant ensuring that tracked effects whose inverses revert their steps preserve the recovery target.The guarantee extends across sequences when each inverse maps its post-effect state back to the preceding state.
  • 3.1. Revertible Effects: The basic track/recover model requires a fixed inverse before seeing the state and can only undo all effects, motivating per-state inverse witnesses and selective reversion.The enhanced effect model preserves composition and supports reverting while leaving the recovery target untouched.
  • 3.1. Revertible Effects: Together, effect functions, tracking, and composition define revertible effects that establish local temporal composability for a component’s effects considered in isolation.The criterion is that the accumulator recovers the component’s starting context after any applied effect sequence.

3.2. Reactive Coeffects

Reactive coeffects model runtime dependencies as typed context state whose satisfaction is re-evaluated after every change, activating or deactivating components accordingly. Combined with revertible effects, this yields local spatial composability and supports context-aware isolation of dependency bindings.

  • 3.2. Reactive Coeffects: Reactive coeffects classify each context transition as activating, deactivating, or neutral against a component’s dependency specification, driving activation or recovery when satisfaction changes.Components activate only when all declared dependencies are present, preventing reads of absent bindings; deactivation applies the tracked accumulator to recover effects.
  • 3.2. Reactive Coeffects: The coeffect context is a finite dependent partial function mapping dependency keys to statically typed values, with guarded get, provision, and restriction operations.Duplicate provision and revocation of absent dependencies are errors that produce no transition, while effectΣ tracks and recovers dependency registrations.
  • 3.2. Reactive Coeffects: Because all coeffect mutations pass through effect functions with recoverable inverses, every dependency change is observed at an effect boundary, establishing local spatial composability.The criterion requires activation only in states satisfying the specification and detection of lost satisfaction where it occurs, so deactivation is driven automatically.
  • 3.2. Reactive Coeffects: Coeffect isolation lets the same logical dependency resolve to different values in different component contexts by separating key-to-realm resolution from realm-to-value storage.This provides runtime-adjustable, fine-grained isolation for multitenant systems, testing environments, sandboxes, and customized component contexts.

3.3. The Context Paradigm

The context paradigm unifies effects and coeffects in a recursive context whose operations mediate all component interactions. It establishes observational equivalence for state comparison and supports hierarchical loading, unloading, and independent composition.

  • 3.3.1: Context-mediated iterators constrain each stage to perform a coeffect operation or install a binding, so every interaction is mediated through declared context keys.Operations act only on their bound values, and out-of-context reads or allocations are excluded unless their state is first bound at a key.
  • 3.3.1: The unified context Γ∞ combines recursive state, effect-reverting accumulators, and coeffect dependency information, with Σ able to encode arbitrary shared component state.Effect maps act on the unified self-similar type, while dependency operations and their inverses are stored in the context.
  • Hierarchical composition: The recursive context structure supports hierarchical composition: loading executes a component’s effects, unloading reverts them without affecting other running components, and parents manage independently loadable children.This yields arbitrarily nested, tree-shaped control across composition levels.
  • 3.3.2: Observational equivalence compares states by all finite sequences of forward operations and their inverses, abstracting away physical state that no context key binds.The induced relation is the coarsest equivalence respected by every operation, and component claims can be restricted to the keys that component declares.

3.4. Attaining Independence

The section defines independence as commutation of all forward transformations and yielded inverses, plus protection of each component’s contributions from the other’s transformations. It shows that this condition lets independently interleaved effects be reverted in any order and transfers to context-mediated components through coeffect witnesses.

  • 3.4.1 Independence: Commutation can be checked on generators: if the generators of two transformation monoids commute pairwise, all their transformations commute, and product composition introduces no transformations beyond the generated union.This reduces independence reasoning from entire transformation monoids to their forward maps and yielded inverses.
  • 3.4.1 Independence: Independence requires every transformation of one iterator to commute with every transformation of the other, while neither disturbs the other’s yielded inverse or continuation.The definition quantifies over transformation monoids generated by reachable forward maps and yielded inverses, and includes the symmetric condition.
  • 3.4.1 Independence: Under pairwise independence, applying each effect’s inverse after arbitrary interleaving reaches the original state regardless of the permutation used for reversion.This supports removing a component while later effects remain in place and extends local reversion to interleaved effects.
  • 3.4.2 Attaining Independence: For operations, independence is defined for every pair of arguments and additionally requires that transformations preserve the other operation’s yielded outcome; operations at distinct keys satisfy this condition.A key is commutative when any two operations at that key are independent, including each operation with itself.
  • 3.4.2 Attaining Independence: Context-mediated component effects meet the independence assumption because coeffect witnesses supply the commutativity required by the theorem, yielding temporal composability for whole systems.The decomposition assigns order-insensitive computation to effects and order-sensitive constraints to coeffects.

4. A Calculus of Dynamic Composition

This section gives Section 3 an operational semantics for dynamic composition by modeling running systems as components and defining rules for their movement and lifecycle.

  • The calculus decomposes a running system into components, each consisting of a coeffect specification, a provision, and a witnessed effect function.
  • Component instantiations are represented as fibers within the calculus.
  • Orchestration rules insert and retire fibers, while lifecycle rules activate and deactivate them without prompting.

4.1. Components and Fibers

This section defines components, fibers, and registries as the runtime objects for dynamic composition. Components declare required and provided coeffects with witnessed reversible effects, while fibers and registries organize lifecycle state and derive the active coeffect context.

  • Components: A component is a triple comprising a coeffect specification d, a provision p of keys it may provide, and a witnessed effect function e with corresponding inverses.The witness is defined up to observational equivalence over the declared dependencies and provisions.
  • Fibers: A fiber is a component instantiation with its own lifecycle, parent, coeffect table, retirement flag, and lifecycle state.Its table starts empty, while lifecycle state tracks inactivity, reloading, or installation through an accumulator and committed view.
  • Fibers: Activation executes a fiber’s effects and accumulates context changes, whereas deactivation applies the accumulator to recover the prior context.Fibers contribute nothing when inactive and their effects when active; real transitions unfold over time rather than occurring atomically.
  • Registry: A registry stores named fibers in a parent-pointer tree, and fiber names provide stable identities while rules mutate only the selected fiber’s lifecycle state.Names are atomic and introduced only when unused, so identity survives mutation and fibers can be addressed unambiguously.
  • Registry: The coeffect context is derived as the union of active fibers’ tables, with disjoint provisions ensuring each provided key has exactly one provider.Satisfaction therefore requires every declared dependency to have an active provider; realm-based systems could relax global disjointness to disjointness within each realm.

4.2. The Calculus

The calculus models dynamic component composition with nine orchestration and lifecycle rules, using state-derived target views to coordinate activation, deactivation, and dependency changes. Revertible activation and guarded teardown preserve component isolation while ensuring provider withdrawal eventually completes.

  • The Calculus: Nine rules generate interleaved orchestration actions and automatic lifecycle steps, with insertion and retirement as the only external inputs to component state.Orchestration rules describe actions the orchestrator may request, whereas lifecycle rules fire whenever their premises hold; the orchestrator never sets lifecycle state directly.
  • Target views: A fiber’s target view is a state predicate determined by retirement and whole-system coeffect resolution, mapping each declared key to its current provider or ⊥.Lifecycle transitions compare this target with the fiber’s committed view, so activation and deactivation respond reactively to dependency changes.
  • Activation: Activation iterates effects that yield inverses and continuations, composing inverses in last-in-first-out order so deactivation can revert the complete activation.L-Begin, L-Iter, and L-Finish represent multi-step activation and retain the accumulated inverse until teardown.
  • Deactivation: Deactivation defers withdrawal while consumers rely on a provider, preserving the committed view needed by teardown code until the provider can safely unload.L-Leave records deactivation, while L-Unload applies the accumulator, discards the committed view, and makes the fiber inactive.
  • Deactivation: The reliance guard cannot deadlock because unloading removes a marked provider from the active context, causing dependent consumers to leave and eventually releasing the guard.Theorem 73 establishes that this guarded withdrawal always releases.

4.3. Metatheory

The metatheory proves that lifecycle rules preserve well-formedness, provide global temporal and spatial composability, and terminate under stated finiteness and acyclicity assumptions. It also establishes confluence: quiescence matches loading the same final configuration from scratch, subject to key-level observational equivalence.

  • Structural invariants: The calculus is invariant under state equivalence and bijective renaming, and vestigial entries can be removed without affecting other fibers except for specified name or key collisions.These structural lemmas support reasoning about registry states while preserving rule applicability and resulting behavior.
  • Preservation and composability: The metatheory proves preservation, global temporal recovery, and global spatial ordering and coherence for interleaved component lifecycles.Well-formedness is preserved by every rule; recovery withdraws a fiber’s contribution without disturbing others, while dependencies govern activation order and keep transition effects tied to one resolution.
  • Recovery boundary: Recovery restores tables only up to each key’s observational equivalence, so monotone allocators, heap layouts, and already-sent messages are not physically rewound.The guarantee concerns bindings and their key-induced equivalence, not complete recovery of external physical state.
  • Progress and quiescence: Every maximal lifecycle sequence reaches a quiescent state, with no deadlock and S(n) ≤ (K + 3)(V(n) + 1) under acyclicity, bounded dependencies, and finitely many names.The finiteness of names is assumed or follows when components cannot recursively instantiate fibers of components that instantiate themselves.
  • Confluence and normal form: At quiescence, lifecycle history leaves no trace: the resulting state is observationally equivalent to loading the same active configuration once in dependency order.Support is well founded and quiescent support equals the set of active fibers, enabling confluence toward a common normal form.

4.4. Extensions

Section 4.4 extends the calculus to asynchrony, failure, isolation, and configuration while leaving Section 4.3’s results intact. These extensions respectively address in-flight operations, effect failures, realm-indexed keys, and runtime configuration changes.

  • Asynchrony: Asynchrony preserves Section 4.3’s results under inertia: in-flight iterations complete, hosts cannot abort certain diversions, and inverses need not obey inertia.Theorem 73 still establishes quiescence, while deactivation is never declined and concurrent fiber steps commute with unapplied inverses.
  • Failure: Failure extends iteration with explicit errors for refused external effects, treating raises as having nothing to undo and exiting reloading through an aborting diversion.Examples include an already-bound port, a missing file, or an unresponsive peer.
  • Isolation: Isolation relaxes shared-key semantics by indexing keys with fixed fiber realms, resolving declarations against their declaring fiber’s realm while preserving underlying key values and operations.The construction takes the key set to be K × R, with each pair (k, r) carrying the value set and operations of k.
  • Configuration: Configuration is carried inside components’ effect functions, so one component instantiated with two payloads becomes two calculus components, while the declarative layer can revise running fibers.Runtime revision includes replacing configuration, reassigning realms, or disabling and lat—

5. Implementation and Case Study · 5.1. Core Library

Cordis implements the paper’s spatiotemporal composability model as a domain-independent meta-framework whose core library mediates effects, coeffects, component lifecycles, and context access. Its runtime design combines tracked reversible mutations with reactive dependency resolution and inertial component transitions.

  • 5. Implementation and Case Study: Cordis is a domain-independent meta-framework that supplies universal dynamic-composition semantics through a layered implementation, with the core library realizing the formal effect and coeffect models.The implementation separates the core library from higher-level component loading and case-study functionality.
  • 5.1.1. Effect Tracking: Every Cordis context mutation flows through ctx.effect, which tracks supplied inverses, composes them into parent disposal, and automatically reverts effects when components unload.The runtime accepts both effect functions and effect iterators; disposal is self-disabling and executes recovery at most once.
  • 5.1.1. Effect Tracking: Effect tracking relies on component-author obligations: Cordis does not verify that supplied inverses actually revert their effects or that coeffect operations commute.The calculus relies on these witnesses, while the runtime leaves their correctness to the component author and representation choice.
  • 5.1.2. Coeffect Operations: Reactive coeffects use symbol-keyed value, realm, and interception tables, separating binding resolution from isolation and access-time interception.Provision and withdrawal are tracked effects, while notifications propagate binding changes to dependent fibers.
  • 5.1.2. Coeffect Operations: Dependency changes refresh affected fibers by testing declared keys against active providers, so satisfaction changes activate or deactivate components and provider withdrawal becomes visible before teardown.A provider in UNLOADING no longer counts as available, causing dependents to recompute their target views and begin teardown.
  • 5.1.3. Component Lifecycle: Components are fibers whose coeffect specifications and effect functions run through an inertial lifecycle: reload and unload complete before target changes trigger chained transitions.Targets identify providers by fresh fiber UIDs, while tracked effects are reverted in LIFO order and dependent transitions are drained during unloading.
  • 5.1.3. Component Lifecycle: The lifecycle preserves coeffect ordering by committing a resolved view during reload, discarding it only after inverse execution, and waiting on dependents that are no longer satisfiable.The provider graph is traversed on demand rather than analyzed in advance, and asynchronous transitions require host scheduling of their task handles.
  • 5.1.4. Context Access: Cordis exposes both reflective ctx.set/ctx.get operations and Proxy-mediated property access, which authorizes reads only through declared and committed component bindings.Undeclared or uncommitted accesses fail at runtime, although static coeffect declarations can support analogous compile-time checks.

5.2. Component Loader

The component loader realizes a persistent declarative configuration as a reconciled tree of fibers, supporting dependency-aware activation, nested loading, and incremental updates. Cordis also enables transactional hot module replacement by disposing and rebuilding component fibers without restarting the process.

  • Component Loader: The loader treats a persistent configuration tree as the authoritative specification of fibers, with entries binding declarative fields and runtime component state in both directions.Entries can represent leaves or nested groups, while @cordisjs/group and @cordisjs/include support grouped and external configuration loading.
  • Component Loader: Theorem 80 guarantees that incremental reconciliation reaches the same quiescent state as loading the final configuration from scratch, regardless of intermediate operations or their order.The loader therefore reconciles changes incrementally rather than tearing down and rebuilding fibers wholesale.
  • Component Loader: Theorem 70 permits concurrent module loading: dependencies constrain fiber activation timing, so fibers wait for missing keys and deactivate before providers leave.The orchestrator need not arrange a load order, because dependency readiness is enforced at activation rather than module fetch and evaluation.
  • Component Loader: Field-specific reconciliation applies the least disruptive update: identity or URL changes rebuild, isolation reassigns realms, interception updates in place, and configuration is delegated to the component.An @cordisjs/group configuration is a child-entry list that can be diffed and updated incrementally.
  • Hot Module Replacement: Hot module replacement replaces component modules in place by disposing old fibers and instantiating new ones, while failed imports restore caches and rebuild every stale entry from backup.This transactional guarantee prevents the system from entering a half-reloaded state.

5.3. Case Study: Koishi

Koishi provides a production-scale validation of Cordis’s dynamic composability through more than 4,000 community plugins spanning chatbot servers and an independent web-console application. The case study demonstrates in-place effect reversal, runtime plugin reconfiguration, and broad applicability, while remaining observational and limited to one ecosystem and host language.

  • Case Study: Koishi: Koishi has accumulated over 4,000 community-contributed plugins across messaging, databases, administration, and end-user features, making it a representative production validation of Cordis.The ecosystem has developed over four years and uses Cordis context primitives for every feature.
  • Expressiveness and generality of the meta-framework: Koishi demonstrates Cordis’s generality across independent runtimes: server features compose chatbot plugins, while the web console composes browser and user-interface primitives.Koishi contributes domain vocabulary while relying on the meta-framework’s context primitives.
  • Temporal composability without cognitive overhead: Disabling a plugin from Koishi’s console reverts its effects in place, while hot-module replacement reapplies edited plugins without disturbing cache state or live connections elsewhere.Cordis tracks context-mediated effects and composes their inverses automatically, reducing the author’s burden for reversible removal.
  • Spatial composability across an open ecosystem: Koishi exposes genuine inter-plugin dependency topology: messaging adapters and database drivers provide coeffects that functional plugins declare and access, enabling runtime provider reconfiguration.The supplied passage specifically cites switching storage backends or reconnecting adapters as reconfiguration examples.
  • Threats to validity: The case study is observational and confined to one ecosystem and host language, so it establishes existence and adoption rather than a controlled quantitative comparison.It cannot isolate the paradigm’s merits from those of its TypeScript realization or Koishi’s domain.

6. Discussion

The discussion identifies boundary-dependent limits to revertibility, distributed and dependency-management challenges, and interface-compatibility risks in the context paradigm. It proposes co-designing languages and operating systems with the paradigm to provide finer-grained effect tracking, dependency handling, isolation, and resource management.

  • System boundary: Revertibility depends on a system boundary: internal state can be restored directly, while external emissions require withholding or application-defined compensation.External operations can first acquire and record resources inside the boundary, such as open/close, malloc/free, or fork/kill.
  • Cross-process invocation: Cross-process service access can preserve provider interfaces through RPC, but latency and mid-flight failure make synchronous exposure problematic.
  • Dependency structure: Dependency cycles predictably leave involved components inactive, while decomposing bidirectional interactions can require O(n^2) integration components.The cycle condition can be reported from declarations during loading rather than detected dynamically as a schedule-dependent deadlock.
  • Interface compatibility: Key-based dependency linking permits interface drift and key collisions across independently built components, motivating language-agnostic structural compatibility checks.Drift can cause type errors, missing methods, or behavioral divergence; collisions can connect consumers to unrelated provider interfaces.
  • Co-design with languages: A co-designed language could make contexts implicit while exposing effect inverses and coeffect specifications to the compiler for optimized execution and earlier dependency-cycle reporting.Compiler support could store inverses in an iteration state-machine frame and admit coeffect specifications into the type system.
  • Co-design with operating systems: A co-designed operating system could provide fine-grained dependency-bounded sandboxing and attribute acquired resources as coeffects, including memory and file descriptors.The operating system could supply declared dependencies at load time, restrict other reachability, and maintain resource records once on behalf of components.

7. Related Work

Related work spans type-level effect and coeffect systems, runtime paradigms for contextual behavior, and approaches to replacing components while managing their effects. Cordis differs by combining runtime effect recovery with reactive dependency management through an explicit context.

  • Effects and coeffects: Cordis extends effect and coeffect research by moving capability tracking, effect reversal, and their unification from type-level disciplines into runtime context mediation.Effekt treats effects as statically tracked capabilities, reversible arrows pair effects with inverses, and graded modal types unify effects and coeffects in one type system [90–93].
  • The context paradigm: The context paradigm mediates every effect and coeffect through an explicit context, contrasting with explicit state threading and implicit imperative mutation while supporting dynamic component activation and deactivation.Its contribution is to carry spatiotemporal composability through runtime context mediation rather than treating effects, dependencies, or recovery as separate mechanisms.
  • Context-oriented programming: Unlike context-oriented programming’s dynamically activated layers, Cordis uses context as an explicit mediation point whose coeffects declare shared dependencies and whose effects can be recovered on removal.COP activates and deactivates behavior according to ambient execution context, whereas Cordis targets complete resource recovery and explicit dependency management.
  • Aspect-oriented programming: Cordis parallels aspect-oriented programming in addressing scattered contextual behavior, but replaces woven pointcuts and advice with coeffects that components declare dependencies on.These shared mediation points allow crosscutting behavior to be reshaped without editing every dependent component.
  • Temporal composability: Temporal-composition systems either migrate state forward across versions, rely on developer-authored cleanup or compensation, or reverse effects automatically only within predefined scopes.Stateful updating requires quiescence or tranquility and hand-written state transformations [53, 54, 101–103]; plugin callbacks, commands, and sagas require developer-written recovery; transactional and reversible calculi constrain reversal to fixed scopes and causal histories.

8. Conclusion

The paper establishes a formal foundation for dynamic composability by combining revertible effects for local temporal composability with reactive coeffects for local spatial composability. The context paradigm unifies both mechanisms, while future validation targets self-evolving agent harnesses with rapid replacement and changing dependencies.

  • Revertible effects provide local temporal composability by storing an inverse for every context transformation, enabling tracking and recovery.
  • Reactive coeffects provide local spatial composability by classifying context changes as activating, deactivating, or neutral, thereby driving component activation and deactivation.
  • The context paradigm unifies effect and coeffect contexts into one type, mediates every effect and coeffect through it, and yields observational independence among distinct components.
  • The resulting component calculus carries spatiotemporal composability from individual mechanisms to dynamic composition systems through its metatheory.
  • Future validation could apply Cordis to self-evolving agent harnesses, testing complete recovery during rapid replacement and dependency coordination under frequent topological change.
Loading 2608.25512v1…