Cordis Deep Research: The Programming Paradigm and Critique of Spatiotemporal Composability
> A responsive microkernel with automatic resource tracking — making reversible plugin unloading and reactive dependency resolution kernel invariants.
Subject: cordis (meta-framework) and its theoretical foundation, *A Programming Paradigm for Spatiotemporal Composability*. Method: formal content of the 88-page preprint plus first-hand code/repository evidence. Inferences are marked 【Inferred】, explicit paper statements as 【Stated in paper】.
---
Feynman view in one sentence
Imagine a LEGO city: removing a building must fill the foundation hole and return borrowed wiring (temporal composability — clean teardown); each building shuts down automatically when upstream power is lost and resumes when it returns (spatial composability — reactive dependencies). Existing solutions either leak (IoC containers assemble but don't clean up) or shut down the whole city (OS/container-level replacement, costly). Cordis's ambition: make teardown and dependency coordination structural laws of the framework, not developer discipline. Cordis is "the physics of plugins" — it doesn't write business logic; it guarantees everything you install can be fully, reversibly unloaded, and that dependencies changing automatically coordinates life and death.
---
1. Basic profile and core concepts
| Item | Content |
| --- | --- |
| Positioning | Plugin meta-framework: core library (effect/coeffect tracking) + declarative component loader (config reconciliation + HMR) |
| Theory | Preprint *A Programming Paradigm for Spatiotemporal Composability* (draft 2026-08-13, under active revision) |
| Authors | Yifan Shi, Wei Zhang, Tianyi Cui (shigma) — Peking University + DeepSeek-AI |
| Version | cordis 4.0.0-rc.x; README: API "may change without notice" |
| Implementation | TypeScript; applied in Koishi (chatbot framework) and DeepSeek Harness (agent runtime) |
| License | Code all MIT; ⚠️ the cordiverse/paper repo has no LICENSE |
Five core concepts (verified):
1. plugin: union type Plugin.Function | Plugin.Constructor | Plugin.Object; no decorators, no annotation scanning; ctx.plugin(fn) and the YAML loader share one code path.
2. context is a Proxy: property reads go through service resolution; three non-mutating derivations — extend(meta), isolate(name, label?), intercept(name, config). Identity uses global symbol branding, not instanceof.
3. inject is reactive and persistent (the key difference): if a required service disappears at runtime, dependent plugins unload and reload when it recovers; unsatisfied dependencies park in PENDING without erroring; load order is purely dependency-topological.
4. Five dispatch modes: 'emit' | 'parallel' | 'serial' | 'bail' | 'waterfall' (⚠️ docs inconsistency: the primer lists 4, omitting bail).
5. effect / reversible registration: effect(execute, label?) collects disposers run in reverse order on unload; generator effects register one disposer per yield; fiber.getEffects() returns a tree of EffectMeta{label, children}.
Plus Fiber (the carrier): state machine PENDING → LOADING → ACTIVE → UNLOADING → DISPOSED (side branch ↘ FAILED); exposes uid, store, inertia, await(), restart(), update(). One plugin mounted multiple times = multiple fibers sharing one Runtime — definition vs. instance separation.
---
2. Problem statement (stated in paper)
Dynamic composition — runtime load/unload/reconfiguration — lacks the formal foundations of static composition. Two orthogonal dimensions:
- Temporal composability: removing a component must completely and safely reverse all side effects on shared state.
- Spatial composability: components declare and resolve dependencies in a structured, verifiable way, coordinating lifecycle as dependencies change.
- Def 1 twisted composition
(f₁,g₁)∘(f₂,g₂) ≔ (f₁∘f₂, g₂∘g₁)forms a monoid (inverses accumulate in reverse). - Def 2–3 effect context
𝜕Γ ≔ Γ × (Γ → Γ)and liftingtrackΓ, a monoid homomorphism (Thm 5). - Def 6–7
recoverΓand the soundness invariant: recovery restores the original state iffg(f(𝛾)) = 𝛾. - Def 8–11 witnessed effect functions form a monoid under effect composition
⋄. - Thm 16 / Cor 21: LIFO rollback restores each step's state at unroll time; under pairwise independence, *any* permutation of inverses returns to the initial state — the key to rolling back interleaved component systems.
- Def 22 coeffect context
Σis a partial function from dependency keys to value types. - Def 23:
set(k,v)is itself a revertible effect — *"coeffect operations are effects, and effects are revertible"* — the synergy of the two halves. - Def 26
notify_d: context changes classified as activating / deactivating / neutral per a specification, driving lifecycle. - Def 28–31:
isolate(per-key realm resolution — ad-hoc polymorphism for multi-tenancy/sandboxing) andintercept(cross-cutting metadata merged right-associatively, constraining downstream access without modifying components). - #6 fiber lifecycle hardening: three re-entrant disposal gaps (effect owner-list registration ordering; rollback of collected cleanup on synchronous setup failure; rejecting effects created during UNLOADING).
- #8 transactional loader/include reconciliation (import before dispose; rollback on failure).
- #12 non-re-entrant group transaction
update; a recorded undiagnosed deadlock (exit 13) from interleaved create/rollback between Include refresh and HMR teardown. - #14/#9 Windows-specific: lost persisted
disabledstate from fire-and-forget renames; short-name alias conflicts. - #15 lazy config parsing (upstream PR #41 backport); #7 JSDoc only.
- 8.1 "Algebraic effect system" is a misnomer — it's a runtime convention of "registration returns a disposer," not typed effects.
- 8.2 "Spatiotemporal composability" is a marketing-flavored term elegantly packaging two old concerns (cleanup, dependency resolution); the novelty is lifting static effect/coeffect theory into a unified runtime calculus.
- 8.3 Tension between "kernel-guaranteed reversibility" and evidence: DeepSeek's patches #6/#12 show re-entrant disposal escapes and an undiagnosed deadlock in rc.7. Production-strength reversibility was *hardened into it*, not built in. Two kinds of "stuck" must be distinguished: dependency cycles → permanent INACTIVE (predictable, honest design boundary, not deadlock) vs. the rc.7 Include/HMR interleaving deadlock (kernel concurrency defect, no diagnostics). Don't equate formal invariants with verified production invariants.
- 8.4 Documentation sovereignty inverted: no standalone Cordis docs; the repo homepage points to the harness docs site (
cordis.js.orgis a 302 placeholder) — the framework's narrative is held by its largest downstream consumer. - 8.5 Bus factor = 1: one author holds 97.6% of commits; plus unstable API and no own docs.
- 8.6 Theory packaging exceeds implementation novelty:
Effectis just a disposer-returning function;injectis reactive dependency gating. Community criticism of over-abstraction exists (flattening Agent Loop and Memory into peer plugins; unclear demand for runtime plugin unloading). - Paper / PDF: https://github.com/cordiverse/paper · raw PDF: https://github.com/cordiverse/paper/raw/main/paper.pdf
- Primer: https://deepseek-harness.github.io/deepseek-harness/reference/cordis-primer
- Tutorial: https://deepseek-harness.github.io/deepseek-harness/develop/cordis-tutorial/
- Koishi: https://koishi.chat
- DeepSeek Harness: https://github.com/deepseek-ai/deepseek-harness
- cordis upstream: https://github.com/cordiverse/cordis · npm:
cordis@4.0.0-rc.8
Motivating examples: VSCode extensions (87 of top 100 contain executable code, unloading requires host restart; only 7 declare extensionDependencies) and self-evolving agent harnesses (component-level self-modification currently forces full process restarts). Coarse-grained OS/container replacement discards in-process state, adds network overhead, and cannot express same-address-space dependencies.
---
3. Theory
3.1 Temporal composability = revertible effects
Effects are modeled as Γ → Γ × (Γ → Γ): apply a transform plus an explicit inverse.
【Inferred】 Spiritually close to reversible computing and Heunen et al.'s inverse arrows, but Cordis only requires caller-provided one-sided inverses at the point of application.
3.2 Spatial composability = reactive coeffects
3.3 Relation to classical effect/coeffect theory (stated in paper)
Effects (Moggi; Plotkin & Power) model how computation *modifies* the environment; coeffects (Uustalu & Vene; Petriclek ICALP'13; graded coeffects ICFP'16) model how it *depends on* it. Classical systems are static; the paper lifts both to runtime-operable mechanisms — the methodological core.
3.4 Unified context type
Def 32 Γ∞ ≔ μΓ. Γ × (Γ → Γ) × Σ — one recursive context type combining state, inverse-accumulator, and coeffect context. Def 33–37: recovery means observational equivalence ≃, since physical state can't be truly restored. Thm 40/42: operations on different keys are independent; per-key commutativity dissolves the independence hypothesis into interface obligations.
3.5 Component model and calculus
Def 43 component ℭΓ ≔ 𝔇Γ × 𝔓Γ × 𝔈Γ∗ (dependencies, provided keys, witnessed effect function). Def 44–45: fibers (instances with state machine, parent pointer, coeffect table) form a registry tree; at most one provider per key. Ten reduction rules (Table 1: O-Insert/Retire/Remove; L-Begin/Iter/Finish/Divert/Raise/Leave/Unload). Metatheory (all "global" — immune to other fibers' interleaving):
| Theorem | Result | | --- | --- | | 59 Preservation | well-formed registries preserved under all rules | | 61/62 Recovery | under pairwise independence, applying a fiber's accumulated inverse removes exactly its contribution | | 63 Ordering | providers activate first; consumers fully deactivated before a key is withdrawn | | 64 Resolution coherence | transitions iterate over a single committed resolution; view changes divert mid-transition (inertia) | | 66 Progress | with acyclic precedence, bounded iteration, finite names — no deadlock, terminates | | 73 Confluence | the system settles to the same state as loading the final composition from scratch — the license to reason statically |
---
4. Implementation (stated in paper)
Three layers: core library (ctx.effect LIFO rollback; ctx.set/get where provision is an auto-tracked effect; Proxy-mediated access that throws on undeclared keys, unlike lenient ctx.get), component loader (declarative config with transactional reconciliation — safe because of Thm 73; HMR via @cordisjs/hmr with transactional reload and cache rollback, no developer-annotated accept boundaries unlike webpack/Vite), and application frameworks (Koishi). The paper proposes Cordis v4; Koishi currently runs Cordis v3.
---
5. DeepSeek Harness integration (verified)
~50 top-level packages; the main loop flows through agent-loop → session → system-prompt → llm-streaming → tools. Service keys: ctx.tools, ctx.llm, ctx.sessions (append-only event log as single source of truth), etc. A "seam" = Cordis Service class (must be a class, not a TS interface) + Provider + Consumer — one provider swap relocates the whole execution world (e.g., filesystem + subprocess → remote sandbox).
Vendoring strategy — the hardest first-hand evidence: 9 upstream packages inlined and rescoped to @deepseek-ai, core being cordis 4.0.0-rc.7 (commit 56b3d4f7). Stated rationale: fully own the framework layer — auditable, patchable, lockable — plus the pragmatic point that publishing under upstream names would squat them. Of 18 patch-log entries, ≥6 are kernel-level concurrency/correctness fixes:
【Inferred】 Upstream rc's reversibility semantics are insufficiently validated under high concurrency + re-entrant disposal + Windows FS; DeepSeek performed the kernel hardening.
---
6. Ecosystem (data verified)
| Repo | Stars | Notes |
| --- | --- | --- |
| koishijs/koishi | 5903★ | MIT; the only empirical ecosystem |
| cordiverse/cordis | 4071★ | 550 commits, shigma alone 537 (~97.6%) |
| cordiverse/paper | 1629★ | No LICENSE |
| deepseek-ai/deepseek-harness | 115544★ | 0.1.0-rc.5 |
| npm cordis | — | latest 4.0.0-rc.8 |
| cordiverse org | — | other repos max 39★ |
【Inferred】 cordis's 4071★ largely postdate the Harness release (DeepSeek halo); its real pre-Harness community was on the order of dozens.
---
7. Horizontal positioning
1. (a) Cordis resembles OSGi Declarative Services, not Spring: a component's *existence is derived from environmental conditions* (PENDING/ACTIVE), not fixed at assembly.
2. (b) The only true differentiation: side-effect rollback. VSCode's subscriptions.push and Fastify's onClose are voluntary discipline; Cordis makes disposers, fiber ownership, and reverse-order rollback kernel invariants. Isolation is Proxy + labels (light, in-language) vs. OSGi ClassLoaders (heavy, JVM-specific).
3. (c) The loader layer carries real engineering weight: stable id, disabled tombstones, nested groups, patch overlays, lazy !!js expressions — nearest analogue is OSGi Config Admin.
Two judgments: tapable's SyncWaterfallHook/SyncBailHook naming likely influenced Cordis's waterfall/bail 【Inferred】; and calling Cordis an "algebraic effect system" is inaccurate — no type-level effect rows, no continuations. Accurate positioning: a responsive microkernel with automatic resource tracking.
---
8. Fact-checks and critique
---
9. Maturity and risk
| Metric | Assessment | | --- | --- | | API stability | ❌ may change without notice; 4.0.0-rc.x | | Bus factor | ⚠️ =1 | | Known kernel defects | ⚠️ ≥6 kernel fixes, incl. one silent deadlock | | Docs | ⚠️ sovereignty inverted | | Downstream | ❌ harness 0.1.0-rc.5 | | Ecosystem breadth | ⚠️ near-zero general; Koishi strong but chatbot-bound | | License | ✅ code MIT; 📄 paper repo unlicensed |
Learning curve traps (verified): silent PENDING as the normal state (inverting fail-fast intuition); HMR plugins implicitly requiring timer/logger services (missing → silent PENDING); YAML entries without id are remounted on any config edit.
Suitability 【Inferred】: long-lived processes + runtime capability add/remove + strict resource reclamation (agent runtimes, IM bots, dev tool hosts, multi-tenant plugin platforms), or as an *architectural thought source*. Not for short-lived request-response services or enterprise deliveries needing API stability. If used, copy DeepSeek's vendoring strategy (pin commits, inline source, maintain a patch log) rather than npm i cordis@4.0.0-rc.x and hoping.
---
10. Limitations of this study
Single primary source (unreviewed 88-page preprint); Koishi validation is observational, not controlled; Cordis was not run independently (evidence via Harness's vendor copy); theory/engineering notes were produced by two parallel research agents.
---
11. Conclusion
Cordis is not another IoC container; it is a paradigm that elevates reversible unloading and reactive dependencies from developer discipline to kernel invariants. Its theory (revertible effects + reactive coeffects → unified context type → a dynamic-composition calculus with six metatheorems) fills a long-missing formal gap; its engineering track record (Koishi's four years and 4000+ plugins; DeepSeek Harness) shows real value in long-lived, hot-modifiable systems. But the price: unstable API, bus factor 1, inverted documentation sovereignty, and an upstream rc that still exhibited deadlock gaps under kernel-level concurrency until patched by DeepSeek. Cordis is currently an early meta-framework usable only after hardening by a major lab, not an out-of-the-box silver bullet. Take its architecture and vendoring strategy; don't ship rc to production.
---
References
> Yifan Shi, Wei Zhang, Tianyi Cui. "A Programming Paradigm for Spatiotemporal Composability." Draft of August 13, 2026. Peking University & DeepSeek-AI. https://github.com/cordiverse/paper (preprint; cite the latest version)