精读对象：arXiv:2608.25512《A Programming Paradigm for Spatiotemporal Composability》
作者：Yifan Shi（北京大学 / DeepSeek-AI）、Wei Zhang（北京大学）、Tianyi Cui（DeepSeek-AI）
提交：2026-08-26 · 92 页 · 1 图 2 表 · cs.PL + cs.SE
前情提要：上一篇《DeepSeek Harness 精读》讲了 Cordis 怎么用，这一篇讲它为什么是对的。
0. 一句话速览
这不是一篇 AI 论文，是一篇编程语言（PL）论文。 它给 DeepSeek Harness 的插件内核 Cordis v4 补上了完整的数学地基。
作者名单里的 Yifan Shi，就是 Koishi / Cordis 的作者 Shigma —— 现在在 DeepSeek。论文自己也交代了：Koishi 跑在 Cordis v3 上，论文呈现的是 v4，核心组合模型两版共享。
所以这不是「又一篇 Agent 论文」。它是一次工程实践的回头总结：一个从 2019 年一路长起来的框架、被 4000+ 社区插件压测了四年，终于有人把「它为什么 work」讲清楚了。
三个你在 dsh 里天天见到的东西，论文都给了正式答案：
| 你在 dsh 里看到的 | 论文里的名字 | 它证明了什么 |
|---|---|---|
ctx.effect() 返回 disposer，卸载自动撤销 |
可回滚效应 Revertible Effects |
卸载一个组件时，它撤回的只有它自己的贡献 |
inject 声明依赖，服务就绪才启动 |
响应式余效应 Reactive Coeffects |
provider 撤回绑定之前，所有依赖方一定已经停用 |
reload 不重启进程 |
合流定理 Confluence |
中途怎么折腾都无所谓，最终状态只取决于最终配置 |
1. 问题：动态组合为什么一直没有理论
论文标题里那个拗口的词 —— 时空可组合性（spatiotemporal composability） —— 其实是把「运行时装卸组件」这件事拆成了两个正交的维度。
时间可组合性管的是：组件被卸载时，它对共享环境做的修改必须被完整、安全地撤销。每一次资源分配、事件注册、状态变更都要能被追踪和回收。
空间可组合性管的是：组件必须能声明、发现、解析彼此的依赖，并在依赖出现或消失时协调各自的生命周期。
静态场景下这两件事都有现成答案：时间维度退化成词法作用域（RAII、bracket 模式），空间维度退化成模块导入解析。但一旦组件能在运行时来去，两边同时崩掉 —— 没有哪个词法作用域能框住一个部署后才加载的插件，也没有哪个编译期上下文能预测运行时配置里冒出来的依赖。
论文拿 VSCode 开刀，数据很扎心
插件系统是动态组合最典型的场景。论文挑了 VSCode 做样本，因为它最普及、也最经典：
| 维度 | VSCode 的现状 |
|---|---|
| 时间 | 所有扩展跑在同一个 extension host 进程里。安装量前 100 的扩展里 87 个含可执行代码，禁用或卸载任何一个，都得重启整个 host，影响所有已加载扩展。 |
| 空间 | 虽然提供了 extensionDependencies，但前 100 里只有 7 个声明了非内置扩展依赖。getExtension(...).exports 返回 any，完全没有类型契约。 |
论文对 deactivate 钩子的批评特别值得记一笔：它不只是「不彻底」，而是把效果的销毁（deactivate）和效果的创建（activate）拆到了两个地方，违反了关注的局部性 —— 于是「清理完整吗」这个问题，变成了一件无法验证的事。
顺带，论文也点了现有变通方案的本质：操作系统在「进程」粒度给了时间可组合性，容器编排器在「服务」粒度给了空间可组合性。 代价是每次重启丢掉全部进程内状态（缓存、连接、部分计算），重建要几秒到几分钟；容器编排还无法表达共享地址空间内组件之间的依赖，给本可以是本地函数调用的交互硬塞进一层网络开销。
论文给它起了个名字：粒度错配（granularity mismatch）。现代系统越来越在更细的粒度上组合，而现有机制只在进程和容器的边界上工作。
对 AI agent 来说这事更致命。论文把「自进化 harness」列为头号动机，并指出最危险的一条：没有时间可组合性，一次错误的自我修改可能让恢复所需的那个进程本身瘫痪。
2. 时间维度：让每个函数自带「逆」
经典 effect system 和 coeffect system 都是静态工具：效应在词法固定的作用域内被追踪、由编译期的 handler 处理；余效应注解针对执行前就确定的上下文验证。
论文的关键判断是：与其给静态类型系统继续加注解，不如把效应和余效应的概念结构「具体化」（reify），让运行时能直接操作它们。
落到时间维度上，成果简单到有点意外：一个效应不是「一个函数」，而是「一个函数 + 它自己的逆」。 类型写成这样：
e : Γ → Γ × (Γ → Γ)
↑ ↑
新状态 撤销这次变换的逆运行时把每一步返回的逆累积保存起来（论文叫它累加器）。于是：
「卸载一个组件」就退化成「把累积的逆跑一遍」。
最漂亮的一点是：LIFO 顺序是白送的。逆按应用顺序累积、按相反顺序执行，正好每一次撤销都拿到「当初自己造成的那一个状态」。论文用一条定理把这个说死了（每步撤销都精确回到它自己的起点，且中间每个状态都满足可靠性不变量），不需要额外规则。
论文还点出一个我很喜欢的类比：效应迭代器本质上就是一个「具体化的定界续体」，也就是主流语言用 yield 暴露的那个结构。所以这套模型不是要发明什么新语言特性 —— 它直接落在语言已经给的 generator 上。
翻译成 Cordis 的写法，就是你在 dsh 里天天见的东西
ctx.effect(() => {
const onSignal = () => shutdown()
process.on('SIGINT', onSignal) // ← 正向：做一件事
// 这个返回值就是论文里的「逆」
return () => process.off('SIGINT', onSignal)
})你返回的那个 () => ...，在论文里是有严格类型的对象：运行时持有它，卸载时按 LIFO 跑它。所以你不需要写 uninstall 路径，也不需要记得清理 —— 这不是「方便」，是有证明的结构性保证。
3. 空间维度：依赖操作本身就是效应
依赖这边，论文先用一张部分函数表来建模，也就是 key → 值 的映射，叫余效应上下文。用类型族保证每个 key 关联到具体的值类型，访问依赖时类型是安全的。
然后是全篇最「啊哈」的一步。注册一个依赖的操作签名长这样：
set(k, v) : Σ ⇀ Σ × (Σ ⇀ Σ)
↑ ↑
新状态 撤销这次注册的逆这个类型恰好就是第 2 节那个可回滚效应函数的类型。
也就是说：注册一个依赖，本身就是一次可回滚效应，它返回的逆就是「把 k 从表里删掉」。论文的结论是 —— 依赖注册的追踪和恢复，完全不需要新机制，直接从时间那一半白嫖过来。原文把这称为两种机制之间的 synergy：余效应操作就是效应，而效应是可回滚的。
在这之上才是「响应式」。每次上下文发生变化，都会被对照组件声明的依赖清单（specification）分类成三种之一：
| 分类 | 含义 | 后果 |
|---|---|---|
| activating | 依赖从「不满足」变成「满足」 | 执行组件的效应（自动被追踪） |
| deactivating | 依赖从「满足」变成「不满足」 | 跑累加器回滚（自动撤销） |
| neutral | 满足性没变 | 什么都不做 |
这就是为什么在 dsh / Cordis 里，插件不需要自己轮询依赖、也不需要自己接事件总线 —— 你 inject 声明一下，系统在依赖满足性变化的瞬间驱动你的生命周期。
论文还顺手加了两个机制，都很实用：
隔离（isolation）：同一个 key，不同上下文解析到不同的值
论文说它本质上实现了一个运行时的 ad-hoc 多态系统 —— 而且这种多态可以在运行时动态调整。多租户、测试环境、组件沙箱都用得上。比如同一份「数据库」依赖，给社区插件注入只读实例，给核心插件注入完整权限实例，而两份代码都不用改。
拦截（interception）：给依赖访问挂横切元数据
关键是它的合并规则是右偏的：外层上下文可以覆盖组件自己的声明。这意味着外层可以约束一个组件「如何使用」某个依赖，而不修改那个组件的代码。这个特性在权限控制里会变成主要卖点（第 6 节展开）。
4. 最深刻的一点：恢复不等于「原样恢复」
前面说「卸载把累加器跑一遍就回到初始状态」，论文很快就自己拆台了。
它举了两个例子：free 把内存块还给分配器，但不会恢复 malloc 之前堆的布局；一个「生成名」被丢弃后也恢复不了，因为下次创建会取一个新的。
物理状态根本没法原样恢复。所以论文做了一件很诚实的事：把「相等」降级成「观察等价」。
定义是这样的：两个状态相关，当且仅当没有观察者能区分它们。而「观察者」的定义才是精髓 —— 观察一个值，就是跑它那个 key 提供的操作、读它们返回的结果。
于是这个等价关系是被接口本身生成的。推论非常实用：
论文里那组 POSIX 对照我看了好几遍，实在太漂亮：
mmap允许返回任何未使用的地址，所以没有操作能观察到「用了哪个地址」，两次分配就是可交换的。open必须返回最低可用的文件描述符 —— 单这一条要求，就让两次描述符分配不再可交换。
同一个内核里的两个系统调用，成败就取决于接口多发布了一个结果。
论文还提到一个细节：关于「分配器发出的 handle」，如果它的接口不比较这些 handle，那么两个堆在「handle 重命名」下就是等价的 —— 这正是 CompCert 关联一个程序及其编译结果的内存状态的方式。
这条洞察可以直接拿去用：如果你在设计一个可热插拔的接口，「少发布一个返回值」不只是减少耦合，它直接把更多变更变成了「不可观察」，从而变得可回滚。
5. 从单个组件，抬到整个系统
单个组件能干净装卸还不够 —— 真实系统是一堆组件交错运行。论文为此搭了三层对象：
| 概念 | 是什么 |
|---|---|
| 组件（component） | 一个三元组：它需要的依赖 d、它可能提供的 key p、以及带见证的效应函数 e |
| 纤程（fiber） | 组件的一次实例化，带自己的生命周期状态，和一份 committed view（记录它激活时每个 key 由谁提供）。你在 Cordis 里看到的 fiber 就是这个 |
| 注册表（registry） | 所有纤程按名字挂载，父指针构成一棵树 |
有个设计细节特别能体现作者的谨慎：整个依赖表是「派生」出来的，不是存储的 —— 它就是所有处于激活状态的纤程共同提供的东西。而且不同纤程的「可提供集合」必须不相交，于是每个 key 恰好有一个 provider。
规则一共九条，分两类：编排规则是外部能请求的动作（插入 / 退休 / 移除），生命周期规则是只要前提成立就自发发生的步骤。
其中「退休」（Retire）和「移除」（Remove）是刻意分开的，理由很实在：退休是一个请求，所以无条件；而一个已退休但仍处于激活态的纤程，必须先被停用才能移除 —— 提前移除会丢弃累加器，直接泄漏。
这套演算最终换来六个结果，我用大白话列一下：
| 定理 | 大白话 |
|---|---|
| Preservation | 系统不会「跑坏」：良构性在每一步之后都保持 |
| Recovery exactness | 任意交错之后跑某个纤程的累加器，它撤回的只有它自己的贡献，别人的一丝不动 |
| Ordering | 纤程只在依赖就位的地方启动；provider 只在所有依赖方都停用之后，才撤回绑定 |
| Resolution coherence | 一次过渡所依据的依赖解析，不会在它自己脚下移动 |
| Progress | 不会死锁，而且一定会终止 —— 每个最长的步骤序列都终结于「静止状态」 |
| Confluence | 无论中途怎么折腾、什么顺序，最终静止状态只取决于最终配置 |
前两个就是「时间可组合性」和「空间可组合性」的全局版本 —— 从「一个组件自己成立」升级成「任意交错的一堆组件之间都成立」。
而 Confluence 是最有工程价值的那个，因为它直接回答了：「配置热更新为什么是对的？」 loader 在做增量调和的时候，中途怎么插入、怎么退休、以什么顺序执行，全都无所谓 —— 系统最终会停在「从零加载最终配置」本该在的位置。这就是 §5.2 那套实现的合法性来源。
6. 落地：理论 ↔ 代码的对照
Cordis 的实现分三层：核心库（效应 / 余效应原语）→ 组件加载器（声明式配置、调和、热模块替换）→ 应用框架（Koishi 在第三层）。
论文的 Table 2 是一张理论到代码的对照表，几个有意思的映射：
| 论文里的 | Cordis 里的 |
|---|---|
| 累加器 | fiber.dispose |
| committed view | fiber.committed |
| 插入 / 退休 | ctx.use 及其回调的逆 |
| 生命周期状态 | fiber.state（LOADING 对应 Reloading） |
一个顺带做成的安全特性
访问依赖有两条路：ctx.get(key) 是反射式查找，永远不失败；而 ctx[key] 走 TypeScript 的 Proxy，沿纤程链向上解析 ——
- 遇到第一个 committed view 里绑定了这个 key 的纤程 → 授权，返回
- 遇到一个声明了但还没加载的纤程 → 访问失败
- 一路走到 root 都没人声明 → 直接拒绝
这本身就是一层能力式访问控制：组件只能访问它声明过的东西。而且因为声明是静态的，完整的权限集合在组件运行之前就已知 —— 编排器可以在加载的时候审查，而不是等到访问发生才发现。
Koishi 的四年，就是这套理论的对照组
- 四年开发，积累了 4000+ 社区插件（IM 适配器、数据库驱动、管理控制台、终端功能）
- 论文自己交代：Koishi 目前跑在 Cordis v3 上，论文里的 v4 精炼了效应/余效应语义并重写了 loader，核心组合模型两版共享
- 最有说服力的验证是「时间可组合性没有认知开销」：因为效应被自动追踪、逆被自动组合，一个没经验的插件作者也能拿到有序清理，完全不用写 uninstall 路径
论文说，这才补上了 VSCode 那种「靠每个作者自己勤勉」的缺失 —— 正确性从「每个人的责任心」变成了由抽象一次性结清。
空间侧的验证同样实在：Koishi 的生态里有真实的依赖拓扑。运行时切换存储后端，只会重新激活那些「解析结果真的变了」的依赖方；依赖暂时缺失的插件保持不活动、但不报错。而关键在于，这一切跨独立作者成立 —— 插件和它的依赖通常由不同人写，除了连接它们的那个 key 之外，谁也不认识谁。
7. 作者自己承认的局限
这部分我挺欣赏，写得非常实在，没有硬撑：
| 局限 | 具体说明 |
|---|---|
| 案例研究是「存在性」的，不是定量的 | 只有 Koishi 一个生态、TypeScript 一种宿主语言，是观察性的，没有受控对照。抽象带来的开销、以及对开发效率的影响，论文没有测量，明确留作未来工作 |
| 「无环」是假设，不是结论 | Progress 和 Confluence 两条定理都建立在依赖优先关系无环的假设上。有环的后果只是相关组件永远不激活（好处是从声明就能提前预测，不像并发死锁必须在运行时检测），但「拆环」会让集成组件的数量随组件数二次增长 |
| 版本问题完全开放 | 形式模型只有按名字链接，没有版本或结构化链接。于是有接口漂移（provider 改了接口，消费者还声明同一个 key，依赖「满足」了但值不对）和 key 碰撞（两个独立 provider 用同名 key 表示无关接口，消费者不做检查就接受）。Cordis 现在靠 peer dependencies 兜着，但这依赖大家遵守 semver，而包管理器通常只解析单一版本 |
| 边界外的东西回不了滚 | 论文把环境划成边界内 / 外。一次外部操作分两个阶段：获取在边界内（装描述符、注册条目 —— 是可回滚效应），发射跨到边界外（写出去的字节、发出去的消息 —— 表现为恒等变换）。事后要恢复只能靠扣留（推迟发射，即经典的 output commit 问题）或补偿（退款、删文件），而补偿「元理论不传递」—— 交换性是针对观察等价证的，换成更粗的等价得重新证一遍 |
| 沙箱需要语言之外的机制 | 语言级的访问控制挡不住恶意组件（它能直接够到底层对象），必须靠软件故障隔离、独立运行时、沙箱进程或容器 |
8. 可借鉴清单
认知层
- 「注册即副作用，卸载即撤销」值得当成一条设计纪律。 不只是 Cordis 的做法，而是一个可以迁移的原则：任何「装上去」的东西，都应该在安装的那一刻就定义好「怎么拆下来」，并且让框架替你拆。凡是把清理代码写在另一个地方的设计，迟早会漏。
- 给「接口发布什么」这件事加一层思考。 想让一个组件更容易被替换、被回滚，第一步不是加抽象，而是检查它的接口有没有发布不必要的返回值。发布得越少，可观察的差异越少，能安全替换的实现就越多。POSIX 里
mmap和open的对比是最好的教材。 - 依赖用「声明」而不是「查找」。 组件说「我需要什么」，而不是「我去哪里找什么」。声明可以静态审查、可以推导加载顺序、可以在依赖消失时自动停用 —— 查找做不到这些。
架构层
- 把「撤销」做成一等公民，而不是异常路径。 如果你的系统有任何形式的动态加载（插件、工具、技能、子 agent），先保证两件事：每次注册都返回一个 disposer，且框架在卸载时逆序执行它们。
- 「退休」和「移除」分开。 一个想下线的组件，应该先被标记、等它自然停用，再真正删除。直接删会丢掉它持有的撤销信息 —— 这是论文专门用一条规则强调的坑。
- 热更新要有「最终状态只取决于最终配置」这个性质。 如果你的增量更新做出来的结果，和「拿最终配置重启一次」不一样，那这个增量就是不可信的。Cordis 用一条合流定理把这个性质钉死了，自研系统至少应该把它当成测试断言。
- 能力集合在加载前可知，比在访问时才拦截强得多。 声明式的依赖清单天然就是一张权限表，可以在组件装载前审查。这是「声明式」相对「运行时反射」被低估的一个收益。
可以直接去读的东西
- 论文第 3.4.2 节关于「可交换性」的讨论，是全文最可迁移到日常接口设计的部分，配合 §6.6 一起读。
- Cordis 源码只有 9 个模块（context / registry / fiber / events / service / reflect / logger / utils / index），
fiber.ts是核心 —— 生命周期状态机加 effect 系统都在里面。 - 论文的 Table 2（理论↔实现对照表）值得单独保存，它是一张「读源码时该看哪里」的地图。
9. 风险与观望点
| 点 | 说明 |
|---|---|
| 论文没有性能数据 | 全文没有 benchmark。效应追踪和依赖解析的运行时开销是多少，只能自己压测 |
| 单一生态验证 | 所有实证来自 Koishi + TypeScript，范式本身和其他语言实现的优劣还没有横向对比 |
| 「无环」需要自己保证 | 它不是被证明的，是假设。你的组件设计得自己盯着别写出环 |
| 版本语义还缺一块 | 这是论文明确列为「开放问题」的部分。生态越大，接口漂移和 key 碰撞的代价越明显 |
10. 延伸阅读
- 论文原文：
arxiv.org/abs/2608.25512（92 页，但 §3 和 §4 的定理陈述部分读下来就够了） - Cordis 源码：
github.com/cordiverse/cordis（MIT） - DeepSeek Harness 里 vendor 的版本：
vendor/cordis，发布为@deepseek-ai/cordis - 官方插件入门：
docs/cordis-primer.zh.md - 前文：《DeepSeek Harness 精读：一个「一切皆插件」的 Agent 运行时》
一句话总结：它把 effect 和 coeffect 从编译期的类型注解，变成运行时可操作的一等对象，让「运行时装卸组件」第一次有了完整的理论保证 —— 而这一切，已经被一个 4000+ 插件的生产系统验证了四年。
发表回复