01The idea in 60 seconds
What if a plugin could vanish without a restart—and every component that relied on it adjusted safely? This paper turns that wish into a programming model with two explicit guarantees.
databasedatabase02Two orthogonal guarantees
Think of a live system as a shared room. Removing one guest means cleaning up their mess—and warning everyone who borrowed their things. §1 · pp. 4–6
Along time
Every context mutation returns an inverse. The runtime records those inverses, then composes them into the component’s teardown.
// creation and recovery stay local
ctx.effect(() => {
bus.on("save", handler);
return () => bus.off("save", handler);
});Across components
Dependencies are explicit specifications. A component starts only while they are satisfied, and reacts when the provider identity changes.
// runs only with a committed database
const reports = {
inject: ["database"],
apply: (ctx) => serve(ctx.database),
};Remember how to undo every mutation, remember who supplied every dependency, and continuously reconcile the two.
03Why ordinary plugins fall short
Processes already give coarse temporal cleanup; orchestrators give coarse spatial wiring. But restarting a process discards caches, connections, and in-flight work just to remove one component. §1.2 · pp. 4–6
The paper’s June 9, 2026 marketplace snapshot says these cannot be individually unloaded from the shared extension host; a restart is required.
p. 5 · paper snapshot, not a live metricSelf-evolving agent harnesses make this more urgent: frequent synthesized changes turn every full restart into cumulative downtime, and a bad update may disable the process needed to recover it.
04The runtime mental model
The clever move is to separate “stop advertising this service” from “actually destroy it.” Existing consumers retain a committed view long enough to tear down safely. §4.3.1 · pp. 34–35
DB provides database. Repository is committed to DB; API is committed to Repository.
05Three objects to keep in your head
The formalism gets much easier once the nouns are fixed. A component is a reusable recipe. A fiber is one runtime instance. The context is the entire mediated world they act through. §4.1 · pp. 28–30
Context
Shared services, component-owned tables, lifecycle registry, ambient state, and accumulated inverses. If a mutation bypasses this boundary, the theorem cannot speak about it.
Component
(d, p, e): required keys, keys it may provide, and a witnessed effect iterator that installs its contribution.
Fiber
It owns an identity, parent, service table, retirement flag, committed provider view, lifecycle state, and undo accumulator.
type Component<W> = {
requires: Set<Key>; // d — what it reads
provides: Set<Key>; // p — what it may write
activate: Iterator<W>; // e — effects + inverses
};
type Fiber<W> = Component<W> & {
id: FiberId;
parent: FiberId | "root";
ownTable: Registry;
retired: boolean;
lifecycle: Lifecycle<W>;
};The vital comparison
database → fiber#17database → fiber#24If provider identity—not merely value—changes, the consumer unloads and may reload against the new provider.
06Programmer layer · effects
The runtime cannot infer how to reverse an arbitrary action. Its structural win is making the inverse local, composing it automatically, and ensuring it runs on every exit path. §3.1, §5.1.1 · pp. 9–17, 56–57
Separated concern
let timer: ReturnType<typeof setInterval>;
export function activate() {
timer = setInterval(refresh, 30_000);
bus.on("message", onMessage);
}
export function deactivate() {
clearInterval(timer);
bus.off("message", onMessage);
// Did we remember every effect?
}Local inverse
export function apply(ctx: Context) {
ctx.effect(() => {
const timer = setInterval(refresh, 30_000);
return () => clearInterval(timer);
});
ctx.effect(() => {
bus.on("message", onMessage);
return () => bus.off("message", onMessage);
});
}Multi-step activation
Each yield is a safe boundary: the forward step has landed, its inverse is now known, and the runtime can stop before the next step if dependencies changed.
ctx.effect(async function* () {
const socket = await connect();
yield () => socket.close();
await socket.subscribe("prices");
yield () => socket.unsubscribe("prices");
const timer = setInterval(() => socket.ping(), 5_000);
yield () => clearInterval(timer);
});
// unload: clear timer → unsubscribe → closeThe paper’s pseudocode and the current 4.0 RC API differ in a few names. This example follows the current public surface; that API is still marked unstable.
07Programmer layer · coeffects
An effect says what a component does to its environment. A coeffect says what the environment must provide to the component. Here, dependency presence is checked again after every context change. §3.2 · pp. 17–22
interface Services {
database: Database;
logger: Logger;
clock: Clock;
}
type Key = keyof Services;
type Value<K extends Key> = Services[K];
type Registry = {
[K in Key]?: Value<K>
};
// A TypeScript approximation of V : K → Typenotifyd(before, after)
Satisfaction means every declared key is present. A changed value with the same provider identity can remain neutral by design.
A real provider / consumer pair
When the database is disposed, Report stops before the database closes. Its teardown may still call ctx.database.flush() because context access resolves through the committed view.
The paper simplifies provision to ctx.set. Cordis 4 RC uses ctx.provide to establish a service and ctx.set to change a value.
export const DatabasePlugin = {
name: "database-provider",
apply(ctx: Context) {
return ctx.effect(async function* () {
const db = await openDatabase();
yield () => db.close();
yield ctx.provide("database", db);
});
},
};
export const ReportPlugin = {
inject: ["database"],
apply(ctx: Context) {
const timer = setInterval(runReport, 60_000);
return async () => {
clearInterval(timer);
await ctx.database.flush();
};
},
};Isolation changes what resolves
const tenantA = root.isolate("database");
const tenantB = root.isolate("database");
tenantA.plugin(DatabasePlugin, { url: "db://a" });
tenantB.plugin(DatabasePlugin, { url: "db://b" });
// Same logical key, different realm, different value.
tenantA.plugin(ReportPlugin); // receives A
tenantB.plugin(ReportPlugin); // receives BInterception changes how it may be used
const constrained = root.intercept("filesystem", {
root: "/srv/community-data",
writable: false,
});
constrained.plugin(ThirdPartyPlugin);
// The filesystem provider must enforce this policy.
// Interception is mediation, not a security sandbox.08The theory bridge
The paper assumes type theory and category theory. Its core, however, mostly needs functions, composition, a monoid of state transformations, typed maps, recursive types, and observational equivalence. §2 · pp. 7–8
Γthe context typethe type of the whole mediated worldγ, δparticular context statestwo snapshots of that worldf : Γ → Γa state transformation(world) => changedWorldg ∘ fcompositionrun f, then gidΓidentitya no-op transformationA × Bproduct type[A, B] or { a, b }A ⇀ Bpartial functionmay throw or return undefinedMaybe(A)optional valueA | undefinedEither(E, A)error or valueResult<A, E>μX. F(X)recursive typean interface containing its own shapeσ ⊧ dcontext satisfies needsevery required key is present≃observational equivalenceno allowed operation can tell apartCategory basics
For this paper, think of types as objects and functions as arrows. Arrows compose when outputs and inputs match. Associativity lets us ignore parentheses; identity arrows do nothing.
The monoid actually used
All arrows from Γ back to Γ are closed under composition, composition is associative, and idΓ is the unit. That is a monoid—the algebra behind sequencing effects and their inverses.
Monads and effects
A monad wraps values with computational structure: Maybe<A> for failure, State<S,A> for state, IO<A> for interaction. The paper reviews this lineage, then reifies effects as runtime state transformations instead of adding static annotations.
Comonads and coeffects
If effects describe what computation produces, coeffects describe context it consumes. The Environment comonad pairs a value with environment E × A; Cordis turns that idea into a live service table and dependency specification.
Type families
V : K → Type means each dependency key maps to its own type: database maps to Database, clock to Clock. A dependent partial map keeps those associations type-correct.
Witnesses and refinements
A witnessed effect is not just code returning an inverse; its type carries the condition that the inverse recovers the state where it was created. The implementation trusts authors to meet that condition.
A returned g is a one-sided, state-local inverse. The paper requires g(f(γ)) ≃ γ where the effect ran—not necessarily f(g(γ)) = γ, and not necessarily a globally invertible computation.
09Formal layer · revertible effects
The effect context pairs the current state with an accumulator. Each new inverse is composed onto that accumulator in the opposite order of its forward action. §3.1 · pp. 9–17
(γ, φ) stores the current world and the recovery program so far.
Apply the forward map; append its inverse to recovery.
Run the accumulated inverse and reset the tape.
One tracked witnessed effect does not change where recovery leads.
A sequence can always be reversed in LIFO order when each inverse meets the state its own action produced.
Any removal order works only when effects are pairwise independent.
09BThe independence test
Equal final states are not enough. Every forward and inverse map must commute across components, and foreign work must not change which inverse or continuation the other effect returns. Def. 19 · p. 16
Each operation owns a distinct key. Forward maps and removals commute; one receipt does not change when the other route exists.
map.set("/a", handlerA);
const undoA = () => map.delete("/a");
map.set("/b", handlerB);
undoA(); // B remains10The context paradigm
The recursive context folds effect tracking and the coeffect table into one self-similar type. Parent contexts own the disposers of child contexts, so teardown composes hierarchically. §3.3 · pp. 22–27
Why exact equality is too strong
free need not restore the heap’s physical layout; closing and reopening a resource may produce a fresh handle. Two states count as equal when no operation exposed by their coeffects can distinguish them.
If handles cannot be compared by any published operation, the renaming is observationally irrelevant.
11The calculus
The authors begin with atomic load/unload, then add four realities: dependent-first withdrawal, multi-step activation, asynchronous inertia, and failure. Ten rules define every legal transition. §4 · pp. 28–53
Insert creates an inactive fiber with a fresh name. Retire irreversibly requests removal. Remove deletes only a retired, inactive, childless entry.
Begin commits a target provider view. Iter lands one effect and records its inverse. Finish lands the last iteration and exposes the fiber as Active.
Divert detects a stale target and routes partial work to teardown. Raise records an error only after accumulated work is recovered.
Leave stops provider discovery without destroying the service. Unload runs the accumulator only after no committed consumer relies on the fiber.
A target changes during slow activation
fiber is Reloading against DB #17
target now names DB #24; promise is already in flight
capture its close() inverse; never expose the stale fiber as Active
run close(), become Inactive, then reload against DB #24
The proof atlas
12The implementation
Cordis fixes the semantics of dynamic composition, not an application domain. A core runtime, a declarative loader, and application frameworks form three layers. §5 · pp. 54–67
Koishi server, Koishi web console, agent harnesses, plugin hosts
desired-state config, reconciliation, grouping, inclusion, HMR
contexts, effect tracking, coeffect resolution, fibers, lifecycle
Effect tracking
Every context-mediated mutation reduces to ctx.effect. A disposer is prepended into the current fiber’s accumulator and, recursively, into its parent’s lifetime.
Context access
A proxy resolves ctx.database through the accessing fiber’s committed provider map. Undeclared or inactive access throws instead of silently returning a stale global value.
Reactive notification
A binding change refreshes fibers that declared the key and resolve the same isolation realm. Refresh is idempotent; provider identity drives lifecycle.
Desired-state loader
Stable entry IDs let the loader diff a persistent tree. Missing requirements simply leave a fiber pending, so modules may load concurrently without hand-authored topological ordering.
id / urlrebuild entry and fiberisolatereassign managed realmsinterceptupdate metadata in placeconfigcomponent-specific keyed diffdisabledunload or reload- id: storage
url: ./plugins/postgres.ts
isolate: { database: production }
intercept: { database: { readonly: false } }
config: { url: $DATABASE_URL }
disabled: false
- id: reports
url: "@cordisjs/group"
config:
- id: daily
url: ./plugins/daily-report.ts
config: { hour: 6 }The paper uses url. Cordis 4 RC currently uses name for the module locator; the two should not be mixed as exact API documentation.
Hot module replacement
No component-specific hot-accept code is needed: dispose the old fiber, invalidate its accepted module closure, import the replacement, then instantiate it inside a clean lifecycle boundary.
Propagate accepted and declined status; unresolved import cycles default to declined.
Traverse imports up to declined boundaries and expand accepted cache invalidation coherently.
Back up caches, dispose stale fibers, import new code. On import error, restore caches and reconstruct the old fibers.
Case study · Koishi
The paper reports more than 4,000 community plugins. Koishi’s server and browser console are separate Cordis applications, evidence that the composition model is not tied to one domain.
Koishi currently uses Cordis v3 while the paper specifies v4. The study is one ecosystem, observational, and reports no controlled overhead or productivity comparison.
§5.3 · pp. 66–6713Where rollback ends
The guarantee applies only inside the system boundary: locations the runtime exclusively mediates and can restore up to the chosen equivalence. Acquisitions can often be reversed; emissions usually cannot. §6.1 · pp. 67–68
ctx.effect(async () => {
const socket = await connect(); // reversible acquisition
await socket.send(payload); // irreversible emission
return () => socket.close();
// closes the handle; cannot unsend payload
});Withhold until commit. Buffer an outbox and emit only after the transition is accepted.
Compensate. Register a refund, delete, or counter-message under a coarser domain equivalence. The paper is explicit that its metatheory would need to be reproved for this weaker notion.
14Useful extensions
The discussion explores service multiplexing, capability-like access, language and OS co-design, mutual-dependency refactoring, and versioned dependency typing. These are directions around the core, not all solved by it. §6 · pp. 68–74
Consumers inject one long-lived broker while backends register and drain behind it. Provider churn no longer changes the consumer’s provider identity—useful for load balancing and rolling updates.
inject is an authority request and the proxy is a mediation point. But ordinary TypeScript can bypass it, so untrusted code still needs a sandboxed runtime or process.
A dependency cycle stays inactive rather than deadlocking unpredictably. Split mutually dependent services into independent cores plus integration components—at a possible O(n²) authoring cost.
A language could make contexts implicit and unforgeable; an OS could grant only declared coeffects and track file descriptors or memory per component. The current library cannot enforce either.
15The assumption ledger
The paper’s guarantees are conditional and carefully scoped. This checklist is the shortest route to applying the model without overselling it.
The runtime records a closure; it cannot verify that the closure really restores the effect.
Untracked globals, raw Node APIs, and shared external state sit outside the formal boundary.
Arbitrary component removal needs commuting forward maps, inverses, and stable cleanup receipts—not just LIFO.
Progress assumes the provider relation has no cycle. Cycles remain inactive and should be reported.
Termination excludes infinite self-registration and assumes each activation has bounded iterator length.
A schedule may fail where another succeeds. Failed fibers contribute no state, but their outcomes differ.
Confluence assumes every successful provider installs every key it declared it may provide.
The final state can be canonical while logs, network messages, emails, or metrics along the way differ.
Cordis restarts the component from a clean slate. State survives only if externalized into a longer-lived dependency.
Isolation and interception shape resolution and policy metadata; they do not sandbox malicious code.
Cordis 4.0.0 RC is marked unstable. The paper and current repository differ in some loader/API names.
The Koishi case shows adoption and existence, not causal productivity gains or measured runtime overhead.
17Read next
These references are selected from the paper’s bibliography. Start with Pierce and Pretnar, then follow coeffects and categorical duality as far as your curiosity takes you. References · pp. 80–88
A clear route into judgments, products, sums, recursive types, and operational semantics.
The categorical foundation the preliminaries use for computational effects.
An approachable bridge from exceptions and coroutines to effect handlers.
The cleanest precursor for thinking about what a computation needs.
The categorical dual behind environment- and context-dependent computation.
Why generators provide exactly the step boundaries used by effect iterators.
The classic vocabulary for compensating actions when exact external rollback is impossible.
A mature service-availability model and the closest implementation precedent on the spatial side.
18The final mental model
When building a component: route shared mutations through the context, return a local inverse for every acquisition, declare every dependency, and design same-key operations to commute.
When building the runtime: remember provider identity, split Leave from Unload, let in-flight work land before compensating it, and never destroy a provider before committed consumers finish.
When making claims: name the boundary, independence assumptions, dependency DAG, failure model, and the emissions that no rollback can erase.