English static mirror for SEO/GEO · AI-assisted translation · Read Chinese original

Cordis Deep Dive: The Programming Paradigm and Critique of Spatiotemporal Composability

Forum topic · QianXun · 2026-08-16

Summary

A technical research report analyzing Cordis, a TypeScript plugin meta-framework, and its theoretical foundation, the preprint "A Programming Paradigm for Spatiotemporal Composability" (Shi, Zhang, Cui; Peking University & DeepSeek-AI, Aug 2026). The paper models dynamic composition along two orthogonal axes: temporal composability (revertible effects, formalized via a twisted-composition monoid and LIFO effect rollback) and spatial composability (reactive coeffects, where components stay active only while declared dependencies are satisfied). These are unified into a single recursive context type and a calculus of dynamic composition with metatheorems covering preservation, recovery, ordering, progress, and confluence. The report maps theory to implementation: Proxy-based contexts, reactive inject, fiber state machines, and transactional loaders with HMR. It documents DeepSeek Harness's vendored fork of cordis 4.0.0-rc.7, including 18 patch-log entries with at least six kernel-level concurrency fixes and one undiagnosed deadlock. Critical findings: the framework is often mislabeled an "algebraic effect system"; documentation sovereignty is inverted (no standalone Cordis docs); bus factor is one (one author holds ~97.6% of commits); APIs remain unstable (rc). Verdict: adopt the architectural ideas and vendoring strategy rather than shipping rc in production.

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.
  • 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.

  • 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 lifting trackΓ, a monoid homomorphism (Thm 5).
  • Def 6–7 recoverΓ and the soundness invariant: recovery restores the original state iff g(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.
  • 【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

  • 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) and intercept (cross-cutting metadata merged right-associatively, constraining downstream access without modifying components).
  • 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:

  • #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 disabled state from fire-and-forget renames; short-name alias conflicts.
  • #15 lazy config parsing (upstream PR #41 backport); #7 JSDoc only.
  • 【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

  • 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.org is 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: Effect is just a disposer-returning function; inject is reactive dependency gating. Community criticism of over-abstraction exists (flattening Agent Loop and Memory into peer plugins; unclear demand for runtime plugin unloading).
  • ---

    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)

  • 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
*AI-assisted research; discrepancies with external narratives are listed in the fact-check section.*

Tags

#cordis#spatiotemporal-composability#plugin-systems#effect-systems#coeffects#dependency-injection#deepseek-harness#koishi

This page is an English static mirror generated for search and AI citation. It may be a full translation or structured summary of the Chinese original. Canonical interactive discussion lives on the Chinese page: https://zhichai.net/topic/178633545