第一层 · 理念与论文

论文精要：时空可组合性

论文 A Programming Paradigm for Spatiotemporal Composability（Yifan Shi、Wei Zhang、Tianyi Cui；Peking University & DeepSeek-AI；2026 年 8 月 13 日预印本）是 Cordis 的设计依据，也是 DSH "一切皆插件"的理论根基。本章把它的核心贡献转译成可读讲解。

论文与仓库的关系

论文 PDF 在上游仓 cordiverse/paper，本仓库不含 PDF 原文，但以两种形态"同步发布"了它的实质：① vendor/cordis 等是论文机制的参考实现；② docs/cordis-primer.md + docs/cordis-api/ 是论文机制的可读 API 文档。本章依据论文原文与仓库实现共同整理。

问题：两个正交维度（§1.1）

论文先指出：现代软件（从插件系统到自演化 Agent 框架）越来越需要动态组合，但其形式基础薄弱。它把问题分解为两个正交维度：

维度	含义	白话
Temporal composability（时间可组合性）	组件被移除时，能完全撤销它的副作用	卸载一个插件后，它注册的回调/监听/定时器能被干净地全部撤回，不留残留
Spatial composability（空间可组合性）	能声明并反应式管理组件间依赖	插件 A 说"我需要 B"，B 没就绪时 A 自动等待，B 出现/消失时 A 被通知

两个维度是正交的——它们各自独立，需要各自的形式化。论文用经典 effect（效果）和 coeffect（协效果）概念分别对应这两个维度，但把它们提升为运行时机制。

动机示例（§1.2）

插件系统（§1.2.1）：装一个插件往全局注册表加项，卸载时要干净撤回——典型的时间可组合性问题。
自演化 Agent 框架（§1.2.2）：Agent 运行时自己装载/卸载能力（工具、技能），既要撤回干净（时间），又要按依赖装配（空间）。这正是 DSH 的场景。
粗粒度补丁（§1.2.3）：传统做法靠重启整个进程或粗粒度隔离来"近似"动态组合，代价大、粒度粗。论文要做细粒度的。

问题深入：插件卸载为什么难

问题不在"装"（装很容易），而在"撤"——而撤回在普通代码里是不自动、易出错的。看朴素写法：

export function apply(ctx) {
  ctx.tools.register(myTool)        // 副作用①：注册表加项
  ctx.on('some/event', handler)     // 副作用②：挂监听
  const t = setInterval(ping, 1000) // 副作用③：起定时器
  // 卸载时？没写 cleanup
}

卸载后：myTool 仍在工具列表（模型可能调到已不存在的实现）；handler 仍挂着（下次事件触发引用已卸载闭包，报错/泄漏）；定时器仍在跑——幽灵行为与泄漏。难点有四：副作用不自动撤销（registry.add(x) 后系统不会记住"将来该撤 x"）；易漏易错序；多插件副作用交织（A 注册 a1→B 注册 b1→A 再注册 a2，卸 A 要精确撤 A 的、不碰 B 的）；失败处理（某 cleanup 抛错会不会卡在半撤销）。

"每个组件有构造+销毁、定义好依赖图"在受限场景够用，但插件系统踩破它三个隐含假设：

副作用不是构造时一次性发生——它在生命周期内动态、事件驱动地增长（某命令触发再注册、配置变更重注册），一个固定批次的"构造+销毁"覆盖不了。
卸载顺序 ≠ 依赖加载顺序的逆。依赖图管"谁需要谁在场"（加载拓扑），撤销要的是"运行时副作用实际发生序列的逆"——这条序列是事件驱动的，dep 图不记录它。
组件不拥有私有对象图——副作用改的是共享全局状态（注册表、事件总线），活在别人的表里，"销毁插件对象"定位不到它们。

一个让"构造+销毁+依赖图"失效的例子：

A 加载：register(foo)                  构造时
运行中：某命令触发 A 再 register(bar)    动态，不在构造函数里
B 加载：on('event', handler) 引用 foo
配置变更：A 重注册 foo（先卸旧再加新）    又一对副作用
现在卸载 A

A 的 destroy() 要 unregister foo 与 bar，但 bar 是运行中动态加的——destroy() 要么只知 foo（漏 bar），要么 A 得自己维护一张"我加过哪些、按什么顺序"的列表再逆序删。而那张列表，就是运行时的 (effect, 逆) 追踪栈——你以为省掉了"逆"，只是把它退化成"每个插件手写一个 mini 运行时"。

"逆"是什么，为什么不是手写 init/destroy

论文把它形式化为 revertible effects（§3.1，Definition 8 + Theorem 7）：每次上下文变换带一个"逆"，且逆由运行时跟踪。Cordis 的解法是把责任从程序员挪给运行时：

export function apply(ctx) {
  const t = setInterval(ping, 1000)
  ctx.effect(() => () => clearInterval(t))          // disposer = "逆"
  ctx.effect(() => ctx.on('some/event', handler))    // ctx.on 也返回 disposer，交 effect 嵌套管顺序
}
// 卸载时：运行时按注册逆序自动跑所有 disposer（Theorem 7：逆序恢复精确）

"逆"（disposer）本质上就是销毁/cleanup 函数——你还是得写它。几条副作用的逆长这样：

副作用                         逆
ctx.tools.register(tool)   →   返回的 disposer / unregister
ctx.on('e', handler)       →   返回的 off
setInterval(fn, 1000)      →   clearInterval(t)
打开连接                    →   关闭它
改 ctx 属性 旧→新           →   改回旧值

分工是：你写每条副作用的逆；运行时管何时调、按什么顺序调、保证一定调到、交织时只撤自己的、抛错不影响其余。

手写 init/destroy vs ctx.effect

	手写 init/destroy	ctx.effect(()=>disposer)
do 与 undo 距离	两方法/可能跨文件，加副作用易忘补 cleanup	写在同一调用里，结构上不能漏
谁调 destroy	每条拆卸路径都得记得调你的	运行时绑 fiber 寿命，所有路径自动跑
setup 半途抛错	泄漏前几步，须手写 rollback	已收集 effect 自动逆序回滚=事务（mod #6）
粒度	per-plugin 全有全无	register() 返回 disposer，可单撤一个换新
拆卸顺序	自己排谁先谁后	运行时按栈逆序，可嵌套表达"我须在 X 之前"

"逆"把撤销从命令式 cleanup 代码升级成与正向副作用严格对偶的一等对象：e 把状态 γ₀→γ₁，逆 e⁻¹ 把 γ₁→γ₀ 精确还原；运行时在副作用发生那一刻就记成 (e, e⁻¹) 一对、增量收集，卸载时按实际序列逆序应用。销毁函数与正向副作用没有可证明的对偶关系，叠加/交织/动态增长时无法证明"还原精确"——"逆"让"撤干净"从约定变成可证明的运行时保证。

形式化是什么 · 熵视角

形式化：把靠直觉/约定/审查的机制，用精确数学对象与规则（定义/定理/证明）固定，使性质可推理、可证明、可机器校验。论文把副作用建模成 Γ→Γ 的 effect 函数 e+逆 e⁻¹、组合 ⋄、track、recover——这些就是形式化。

熵原则在此应验：插件作者侧每插件都要正确处理 do/undo 配对、撤销顺序、调用时机、失败回滚、跨 fiber 不冲突，是跨插件都一样的重复熵；形式化+运行时把它抽象成一份统一处理，作者只剩 ctx.effect(()=>disposer)。熵没消失，搬到两处：①论文形式模型（一次性、难、可证）；②Cordis 运行时（一次性、统一、被所有插件复用）。简化是真的，熵被搬到一次性的形式模型+运行时统一付了，没凭空消失。

形式化的逆在 DSH 非平凡处真的承重：agent 工厂的创建事务（prepare→yield detach→announce）靠有序复合 effect + 逆序回滚，让"session 在 agent 关闭事件提交后才拆"。手写 init/destroy 会让竞态兄弟 effect 先撤掉发布钩子——丢事件（session.md 明说的坑）。

结论：单插件手写 init/destroy 够；50 个插件在 HMR+配置重载+错误回滚+跨 fiber 拆卸下，手写=在每个拆卸点重写"谁先谁后/失败怎么回滚"=手写 mini 运行时且无可证保证。晦涩的数学在底层证明可组合；你日常只碰 ctx.effect(()=>disposer)。"逆"的必要是给系统的可证可组合性的，不是给单插件的。

逆会不会"失真"？会不会死锁？

会产出逆并存起来吗——会。Definition 8 区分 effect 函数 𝔈Γ 与带逆的 witnessed effect 函数 𝔈Γ∗：应用一个 effect 时运行时同时拿到正向 delta 与其逆，把这对存起来。

逆会不会随动态执行失真——关键看它是不是快照。论文存的不是"冻结旧值快照、撤销时还原快照"（那确实会失真），而是与正向变换对偶的逆变换：

独立 effect（§3.1.3 Def 19）——作用在不重叠键上。逆"把键 X 减 1"无论键 Y 发生什么都对当前状态有效。Theorem 20 / Corollary 21：独立 effect 可任意顺序撤销、交织不失真。
重叠 effect——作用在同一键上，朴素"各自记逆"会冲突。论文用 transformation track（Def 3-5）+ effect composition ⋄（Def 9/Thm 10）+ effect transformation effectΓ（Def 12/Thm 13）把正向变换组合起来并重新计算组合后的逆，保证存的逆始终是"实际已应用的组合正向变换"的正确逆。Theorem 14/15 证明组合后仍精确恢复。

一个让朴素逆崩掉的重叠例子

设 A: K1 1→3（绝对赋值）；B: 若 K1==3 则 +1 否则不动（条件）；C: K1 减 1（相对）。三者重叠于 K1、且可能乱序、多次执行。先如实定义逆——绝对赋值/条件的逆不是"当前状态的纯函数"，得带 witness（这正是 𝔈Γ 与 𝔈Γ∗ 分开的原因）：

effect	正向	逆（带 witness）
A 绝对	K1:=3	K1:=〈A 应用时捕获的旧值〉（绝对赋值本身不可逆）
B 条件	if K1==3 then +1	if B 当时动了→恢复3；否则 identity（须捕获"B 是否动了"）
C 相对	K1:=K1-1	K1:=K1+1（真·相对逆，无需快照）

论文承诺：从不承诺"任意序、任意次、完美还原"。重叠于同键：Theorem 7/16 按序应用+严格逆序撤销才精确；Theorem 20 仅独立时撤销序任意。

走一遍（应用序 A→B→C，K1 从 1）：应用后 K1=3,4,3；逆序撤 C⁻¹(3→4)→B⁻¹(4→3)→A⁻¹(3→1)=1 ✓。但若乱序先撤 A⁻¹(3→1)→B⁻¹(1→3)→C⁻¹(3→4)=4 ✗。乱序一撤就崩——这正是论文要求逆序、且运行时强制 LIFO 的原因。重复执行：每次应用各带自己的 witness 存一条栈帧，LIFO 仍精确。

靠什么设计排除"混乱"：① 运行时强制 LIFO，你不选撤销序；② 每应用即刻捕获 witness，之后发生的事不污染它；③ 重叠用 transformation track 重算组合逆；④ 跨 fiber 重叠用无环优先关系（Def 65）+ 串行化（§4.3.1 Withdrawal）。诚实边界：撤销中途插入与同键重叠的新正向应用，不是论文保证场景。

Cordis 实现怎么兑现：disposer 是命令式闭包，但不是还原快照，而是"按身份移除我加的那条"——packages/core/scope 的 NamedEntries/AnonymousEntries 提供 exact-entry undo（按条目身份幂等撤销），只删自己的、不碰别人的，故交织鲁棒。实践中 DSH 注册几乎都是"加一条/删那一条"——不同条目天然独立（Thm 20），重叠难情形从构造上回避。

死锁——形式侧：Progress（Theorem 66）在无环优先关系下保证总能前进、无全局死锁；Confluence（Theorem 73）不同迁移顺序收敛到等价静寂。实现侧（vendor/README.md 本地修改即治死锁的实证）：fiber 生命周期硬化（mod #6：UNLOADING 拒建 effect、setup 内发起卸载等 setup 与已收集 cleanup）；mod #12 序列化 Include 子树变更 + HMR 主 watcher 抑制初始扫描——后者修的是"退出码 13 无诊断"的死锁：失败 initial apply 的 rollback disposed HMR，而 HMR teardown drain 在等排在同一 apply 后的 queued refresh。

机制一：可逆效果 Revertible Effects（§3.1）

论文形式化"每次上下文变换都带一个逆，且这个逆由运行时跟踪"。具体三块：

Effect Context（§3.1.1）：把上下文建模为状态 Γ，一次 effect 是 Γ→Γ 的变换。
可逆 effect 函数（§3.1.2，Definition 8）：一个 effect 不仅做正向变换 (δ, g)，还自带逆 g⁻¹。恢复精确性定理（Theorem 7）证明：按 LIFO 逆序应用各 effect 的逆，能精确还原之前的状态。
effect 独立性（§3.1.3，Definition 19）：当两个 effect 作用在不冲突的键上，它们独立，可乱序恢复仍正确（Theorem 20）。

对应到 Cordis 代码 · 可逆效果

ctx.effect(() => disposer) 的 disposer 就是论文里的"逆"。Fiber 卸载时按注册的逆序跑所有 disposer（见 docs/cordis-api/fiber.md 的 Effect/Disposable 类型）。这把论文的 Theorem 7（逆序恢复精确）直接实现成运行时行为。

机制二：反应式协效果 Reactive Coeffects（§3.2）

论文形式化"每次上下文变化，按组件的协效果规约通知该组件"。具体：

Coeffect Context（§3.2.1，Definition 22）：上下文是一组键→值，get/set 操作（Definition 23）。
规约与通知（§3.2.2，Definition 25/26）：一个 coeffect 规约声明组件需要哪些键，以及这些键的值变化时如何反应。
Isolation 与 Interception（§3.2.3，Definition 28/31）：可以创建独立服务作用域（isolate，同一键在不同 scope 解析到不同实现），可以对子上下文的配置做拦截合并（intercept）。

对应到 Cordis 代码 · 反应式协效果

ctx.inject(['llm','tools'], (ctx) => {...}) 就是协效果规约——声明依赖的键，等这些服务都就绪才激活。ctx.get(name, strict=true) 默认只返回"当前处于 active 的提供 fiber"的实现，这正是"反应式"：服务提供者一卸载，依赖它的组件会被唤醒重排。ctx.isolate() / ctx.intercept() 直接对应论文的 isolation/interception。

统一上下文范式 The Context Paradigm（§3.3）

这是论文的核心主张：把 effect context 与 coeffect context 统一为单一上下文类型 Γ∞（Definition 32），就构成一种编程范式。

统一的关键是观察等价（observational equivalence，§3.3.2）：因为生成式名字、堆布局等对程序不可观察，等价关系（≃）让 effect 与 coeffect 能在同一类型下共存而不冲突（Definition 34/37 把 effect 函数读作"满足 ≃"）。一句话：同一个 ctx 既是"我注册了什么"的载体，又是"我依赖什么"的载体。

为什么这很关键

传统框架把"我注册的服务"和"我需要的服务"放在不同的系统里处理。论文让二者共享一个上下文，于是一个组件的注册（effect）天然成为另一个组件的依赖（coeffect）的通知源，运行时自动联动。这就是 DSH 不需要手动编排加载顺序的原因。

动态组合演算 Calculus of Dynamic Composition（§4）

论文把上面的机制组装成"组件"并给出形式演算：

组件与 Fiber（§4.1）：组件（Definition 43）= 协效果规约 d + 配置 p + effect 函数 e，三者都在统一上下文 Γ 上。Fiber（Definition 44）是一个组件的一次实例化——它有自己的注册表条目、生命周期状态。
基础演算（§4.2）：注册表 F_γ 记录每个名字→其提供者；目标视图（target view, Definition 46）给出每个声明键解析到哪个 fiber。
进行中的迁移（§4.3）：组件在生命周期中经历 Withdrawal（撤回，§4.3.1）、Iteration（迭代，§4.3.2）、Asynchrony（异步，§4.3.3）、Failure（失败，§4.3.4）。论文用 effect 迭代器（Definition 52）保证"累加器按 LIFO 应用各逆"。

元理论 Metatheory（§4.4）

论文证明：从单组件的时空可组合性，可以提升到一整个交错组件系统。五条主定理：

定理	说了什么
Preservation（Theorem 59，§4.4.1）	每一步迁移后，注册表仍是良构的——系统不会自我破坏结构
Temporal Composability（§4.4.2，Theorem 61）	恢复精确性：按序应用、逆序回滚，能精确还原状态
Spatial Composability（§4.4.3）	依赖解析的连贯性：一个 fiber 只在其依赖都已提供时才开始
Progress（Theorem 66，§4.4.4）	系统总能前进——不会整体卡死（无死锁，依据无环优先关系）
Confluence（Theorem 73，§4.4.5）	合流性：不同迁移顺序到达等价的静寂状态——最终结果一致

对学习者的意义

你不必读懂形式证明。要记住的是：Cordis 不是靠"约定"来保证卸载干净和依赖正确，而是有形式化证明的运行时保证。所以你在 DSH 里写 ctx.effect() 返回 disposer、用 ctx.inject() 声明依赖，可以信赖它们的行为符合上述定理。

实现：Cordis（§5）

论文把上述理念实现为 Cordis——一个时空可组合性的元框架，分两部分：

核心库（§5.1）：effect tracking（效果跟踪）、coeffect operations（get/set/isolate/intercept）、component lifecycle、context access。对应仓库 vendor/cordis/。
声明式组件加载器（§5.2）：声明式配置（cordis.yml，§5.2.1）+ 热模块替换 HMR（§5.2.2）。对应仓库 vendor/loader/、vendor/include/、vendor/hmr/。

论文还用 Koishi（§5.3）做了案例研究。

论文 → 仓库映射

论文概念	仓库落点
统一上下文 Γ∞（Definition 32）	`vendor/cordis/src/context.ts` → `docs/cordis-api/context.md`
Fiber / 组件实例（Definition 44）	`vendor/cordis/src/fiber.ts` → `docs/cordis-api/fiber.md`
可逆 effect / disposer（Definition 8, Theorem 7）	`ctx.effect()` + `Disposable` 类型（fiber.md）
协效果 get/set/isolate/intercept（Definition 23/28/31）	`ctx.get/provide/set/isolate/intercept`（context.md）
反应式依赖解析（Spatial §4.4.3）	`ctx.inject()` + `ctx.get(strict)` active 判定
声明式加载器 + HMR（§5.2）	`vendor/loader`、`vendor/include`、`vendor/hmr`
注册表良构/优先关系（Definition 58/65）	DSH 各注册表（tools/session/agents）的 scope 解析

为什么这对 Agent 框架重要

Agent 框架是"动态组合"的极端场景：运行时要装/卸工具、技能、模型适配器，还要能热改配置而不重启。论文提供的形式保证意味着：

卸载一个工具插件，它注册的 schema、监听器、效果会全部干净回滚（Theorem 61）。
换一个 LLM 适配器，依赖 ctx.llm 的循环会自动重排，不会跑空（Spatial + Progress）。
不同迁移顺序最终等价（Confluence），所以你不用纠结插件加载的精确顺序。

下一节我们把 Cordis 的这些机制拆成五大核心理念，配上最小可运行代码。