Chapter 12
Edges & related work (§6–7)
12.1 The system boundary (§6.1)
A location is inside when the system can modify it exclusively and restore it; otherwise outside, where operations act as id — untracked, unreverted. A coeffect moves the boundary inward by reifying a location behind operations with inverses. Operations that reach outside split into acquisition (open, malloc, fork — installs a record inside; revertible) and emission (write, send — crosses out; not revertible). For emissions: withhold until the state is certain to persist (the output-commit problem), or compensate (delete the file, refund the charge — sagas). Compensations compose LIFO like inverses; but the metatheory's commutation is proved against ≃ and does not transfer to the coarser equivalence a compensation restores.
12.2 Multiplexing, access control, languages, cycles, versions
- Service multiplexing (§6.2). Exclusive binding: swap the provider and every consumer reloads. Broker: providers and consumers both inject a central service; provider churn is invisible to consumers. Gives load balancing, rolling updates (load new provider, shift weight, drain old — Kramer–Magee quiescence as an app-level pattern), cross-process RPC (must be async-contracted).
- Access control (§6.3).
injectis a capability request, the proxy a mediator; the full capability set is static and reviewable at load. Interception is fine-grained policy without touching either party, no reload. Real sandboxing needs an execution boundary (process, Wasm) plus a bridge fiber. - Language independence (§6.4). Temporal needs closures + retractable modules (
require.cache;dlopen/dlclose; Wasm instances). Spatial needs typed keys extensible by providers (typeclass instances, Rust impls, TS module augmentation) + transparent interposition on access (Proxy, Python descriptors, or macros that generate accessors). - Mutual dependencies (§6.5). A cycle leaves both components permanently inactive — detectable from declarations at load time. Cure: split into cores plus integration components (server-core, ac-core, request-mediation, policy-management). Quadratic in the worst case; mitigate with bundling, convention wiring, scaffolding.
- Versioning (§6.6) — the acknowledged gap. Linking is nominal, by key string. Interface drift and key collision go unchecked. Options: namespace keys by package (couples the model to a registry); peer dependencies via npm (what Cordis does; relies on semver honesty; one version per package); structural compatibility (undecidable in general).
- Co-design (§6.7). A language could make the context implicit (preventing a component from reaching another's context through a closure), compile iterators to state machines, admit coeffect specs into types (cycles at compile time; row-typed structural compatibility). An OS could hand out fds and memory as coeffects with attribution.
12.3 Related work, positioned
| Family | Representatives | How Cordis differs |
|---|---|---|
| Monadic effect systems | Effect-TS, ZIO, fp-ts | Tracking costs a monadic embedding; a withdrawn service leaves its effects in place. Cordis is an overlay with inverses and re-resolution. |
| Effects as capabilities | Effekt | Same "context mediates capabilities" view, but static and for modular interpretation, not reversion. |
| Reversible effect semantics | Heunen et al., inverse arrows | Two-sided, global reversibility by construction; Cordis wants one-sided per-atomic-effect inverses supplied by the caller. |
| Graded types | Granule; coeffects for Java-like languages | Static; orthogonal. |
| COP / AOP | ContextL; AspectJ | COP resemblance is nominal (layers don't track or revert; activation isn't dependency-driven). A coeffect is the declared, non-oblivious analogue of an aspect, lifecycle-integrated. |
| Stateful forward migration | DSU, Kitsune, Erlang code_change, webpack/Vite HMR | Migrate state forward with hand-written functions. Cordis reverts to a clean slate and reapplies — in-memory state doesn't survive unless in a longer-lived dependency. More general (no migration code, real unload), less graceful; layering DSU on top is future work. |
| Developer-authored recovery | OSGi / Eclipse / VSCode unload hooks, Command pattern, sagas, finalizers, event sourcing | The inverse is an unenforced duty. React useEffect is the closest structural pairing but non-composable (top level only; no async or iterator body). |
| Statically scoped reversal | STM, reversible languages, RCCS, linear types, RAII/Rust | Reversal fixed to a scope in advance; Cordis fixes none and treats lexical resource management as complementary within a component. |
| Interposed reclamation | Nooks, shadow drivers, Akeso | Runtime-maintained record of acquisitions, but the platform fixes what is recordable; Cordis components introduce effects of their own with an inverse each. |
| Availability-reactive components | OSGi Declarative Services, iPOJO, R-OSGi | Closest precedent for reactive coeffects; but hand-written, synchronous deactivation callbacks. Cordis reverts accumulated effects and runs async teardown to completion (inertial Unloading). |
| Value-level reactivity | FRP, signals | Value-level and glitch-free within a turn; Cordis is component-level with async lifecycle and no turn (only Thm 71). Complementary — a coeffect can carry reactive values. |
Threats to validity the paper names
One ecosystem (Koishi), one host language, observational not controlled, no overhead measurement. Koishi runs Cordis v3; the paper describes v4. The API is marked unstable.