# 88 页论文，3 页就能讲明白——读 DeepSeek 的 Cordis 时空可组合性论文

本文面向初次接触 Cordis 论文的读者。前半聊为什么 88 页太多了，后半用更短的篇幅把论文核心思想讲清楚。如果你只想知道「这篇论文到底说了什么」，直接跳到 3 页讲明白。

一篇 88 页的论文，讲了什么呢

DeepSeek-AI 与北京大学相关作者最近放出一篇预印本：A Programming Paradigm for Spatiotemporal Composability（Draft of August 13, 2026）。它讲的是底层插件/组件框架 Cordis 的设计原理：如何在运行时安全地动态装、卸、换组件。仓库写明这是持续修订中的 preprint，引用前请核对最新版本。

我读完的第一反应是：核心思想用很短的篇幅就能讲明白。

这不是贬低。论文确实有真东西——把动态组合的「拔得干净」和「依赖跟得上」提升成可证明的运行时机制，并给出系统级合流性等元理论结果。但这个真东西被包在大量形式化定义、相关工作综述和讨论展望里，像一颗珍珠塞进一床棉被。大多数读者在翻到珍珠之前就已经放弃了。

这篇文章做两件事：先说明为什么 88 页对初次读者过重，再用工程师语言把论文核心对齐讲清楚。它和站内 Harness Engineering 同属「如何约束 Agent 运行时」一族问题；和 复合函数视角的 Harness 则是不同切面——前文抽象外层编排，本文读的是一篇把「动态可插拔」形式化的 PL/系统论文。

为什么 88 页太多了

先说论文的核心思想有多简单

论文自己的轴是两维，工程上可以翻译成三句话：

1. 时间维（temporal）：插件装上去能拔下来，副作用自动回滚——像 GC 回收内存，只是对象换成了副作用。
2. 空间维（spatial）：依赖关系声明式解析；缺依赖就待机，来了就激活，撤走就连带回滚。
3. 合在一起：不管你怎么折腾装拆顺序，最终状态等价于对「当前仍存活的那批组件」做一次静态组装——这就是合流性要担保的事。

有经验的工程师读到这里，通常已经能联想到 undo log、RAII、OSGi、依赖注入。核心思想确实可以短讲。

88 页花在哪了

按目录粗拆（含前后页码重叠，仅供扫读）：

内容	大约位置	对普通读者的价值
形式化定义与演算元理论（含合流性等定理）	§3–§4，约三十多页	除非你要核验证明或跟进相关研究，否则可跳过细节
相关工作（effect/coeffect、插件与热替换谱系）	§7	学术规范；非第一次阅读的重点
Cordis 实现与 Koishi 案例	§5	有工程信息量；注意 v3/v4 脚注
Discussion（边界、沙箱、语言无关等）	§6	有用，但夹杂开放问题与愿景
你真正需要带走的直觉	引言两维 + §3 机制直觉 + 合流性陈述	本文第二节覆盖的全部

为什么写这么长？一部分是 PL 理论写作惯例：概念要有直觉、形式定义、例子、性质、证明，一个概念就能吃掉数页。另一部分是作者的选择：两边都想占——既有理论演算，又有实现与生产案例。两边叠在一起，篇幅自然膨胀。纯理论路线可以更短，纯系统论文也可以更短；两者都放，就有了 88 页。

术语膨胀的问题

「扭曲组合幺半群」（twisted composition monoid）——论文里用来刻画「正向变换 + 逆变换」如何复合。从工程视角，它描述的就是带顺序的、可撤销的复合操作；换个朴素名字也能讲清楚。PL 论文的话语体系不一定故意唬人，但客观上抬高了门槛。

后果是：受众被缩小了。能啃完 88 页 PL 元理论的人，远少于能从 Cordis 工程思路里受益的人。若核心用更短的篇幅对齐讲清，读者至少会多一个数量级。

3 页讲明白论文核心

以下不需要 PL 理论背景也能读。

问题：插件拔不干净

软件系统需要运行时动态加载、卸载、替换组件。这件事行业做了几十年——OSGi、Spring、VSCode 扩展、Erlang 热替换——但有一个共同痛点：

装上去容易，拔干净难。

插件会注册监听器、打开连接、改配置……卸载时要把这些全部撤销。传统做法是让开发者在 stop() / deactivate() 里手写清理。人靠不住。论文给出一组公开数据：VSCode 安装量前 100 的扩展中，87 个带可执行代码，卸载/禁用往往需要重启整个 extension host——不是开发者懒，是副作用太多、太隐式，写全 cleanup 几乎不可核验。

论文把需求拆成两维：

• Temporal composability：组件移除时，它对共享环境的修改必须被完整、安全地逆转。
• Spatial composability：组件之间的依赖要能被声明、发现，并随依赖变化做结构化的生命周期协调。

动机里还写了 self-evolving agent harness：若 Harness 要在不停服的前提下改自己的组件，细粒度的时空可组合性就不再是锦上添花。粗粒度替代方案（整进程重启、整容器编排）成本高，且粒度对不上「同地址空间里的组件」。

Cordis 的方案：两维，三句话

1. 副作用自动回滚（revertible effects）

所有对系统状态的修改，应通过统一接口（实现里是 ctx.effect）进行。每次修改，运行时记录逆操作：

• 注册了监听器 → 记住「注销它」
• 改了配置 → 记住「恢复原值」
• 打开了连接 → 记住「关闭它」

卸载时反向执行这些逆操作，恢复到加载前状态。开发者不需要手写完整 cleanup 路径——只要副作用走了可追踪的口子。

这和 GC 把 free 从职责里拿掉是同一逻辑：GC 管内存；Cordis 管（经上下文中介的）副作用。

2. 依赖自动编排（reactive coeffects）

每个组件声明自己需要什么。运行时按声明管理生命周期：

• 依赖满足 → 激活
• 缺依赖 → 待机
• 依赖撤走 → 先回滚依赖方副作用，再完成卸载

不同作者独立写的插件，协调点主要是各自的依赖规格。类似 Spring IoC，但强调运行时依赖拓扑变化时的反应式通知与回滚，而不是只在启动期注入一次。

3. 乱序安全（合流性）

前两条合在一起，支撑论文元理论里的关键性质：

无论组件以何种交错顺序加入、移除、替换，最终系统状态应与「对最终仍存活配置做静态组装」观测等价。

中间折腾不留脏痕迹——前提是副作用真的拔干净、依赖变化真的协调到位。打个比方：文档里打了又删，最终内容只取决于「还留着的字」；Cordis 要保证的是「删干净了」。

合流性（Confluence）是整篇最值得认真对待的形式化结果之一。旁边还有 Preservation、全局 temporal/spatial composability、Progress 等；乱序安全是工程师最该带走的那一块。

和现有方案的区别

系统	副作用清理	依赖管理	乱序安全保证
OSGi	开发者手写 stop()	Service Registry	无形式化合流保证
Spring	开发者手写 destroy()	IoC 容器	无
VSCode	开发者手写 deactivate()	扩展依赖声明（使用率低）	无；常靠重启 host
Erlang/OTP	开发者手写 code_change 等	无同一套细粒度模型	无同一陈述
Cordis	运行时跟踪并回滚	声明式 + 反应式编排	演算元理论（含合流性）

核心差异在第一列：谁负责把副作用清理干净。 传统方案靠开发者自觉；Cordis 把正确性尽量卸到范式与运行时上。

真正有价值的是什么

那 30 多页形式化有没有必要？

有一条线是必要的：把局部的可回滚与反应式依赖，抬到交错组件系统上的全局性质，尤其是合流性。 动态组合的操作序列可以任意交错；只靠工程直觉说「应该没问题」，很容易在边界情况翻车。先装 A 再装 B 再卸 A 再装 C，和另一条路径最终是否一样——手动推容易错，形式化才给得起保证。

论文在 Koishi 案例里有一句很贴工程现实的概括：原本要靠每位作者 diligence 守住的正确性，被 abstraction 一次性卸下。和 GC 把内存管理从人转移到运行时，是同一个迁移方向。

去掉这条「结构性保证」，论文价值会掉一大截；有了它，「乱序安全」才有数学承重墙。至于其余演算细节，对理解思想不是第一优先——对核验证明才是。

不是没有问题

形式化与生产验证没对齐

这是最该被质疑的一点。脚注写得很清楚：Koishi 当前使用 Cordis v3；论文呈现的是 Cordis v4（细化 effect/coeffect 语义并重做 loader），两者共享核心组合模型，但不是同一精确系统。

你证明的是一套演算/实现叙事，生产案例主要落在前身版本上。把 Koishi 规模直接读成「v4 理论已被同构验证」，过满了。论文自己用脚注交代了这一点，读者却很容易忽略。

单一生态、缺少受控对比

验证主战场是 Koishi（数千社区插件、服务端 bot + 浏览器控制台等），信息量大，但是单一生态、单一语言主线（TypeScript）。与 OSGi、Erlang 热替换、VSCode Extension Host 等，没有同题受控对比实验。你很难从论文里读出「好多少」的量化答案；作者也把部分开销与生产力对比标成 future work。

系统边界之外的副作用

Discussion 承认：只有系统能独占修改、并能恢复修改前状态的 location，才落在可追踪边界内。第三方库若绕开 ctx.effect、直接改全局或原型链，运行时跟不住。保证的强度，取决于有多少副作用愿意走进上下文这扇门——这不是小字，是模型的适用边界。

愿景超前于成果

Self-evolving agent harness 是强动机，不是已交付的验证闭环。细粒度动态组合对不停服自修改确实关键，但「Agent 在生产中改自己的 Harness」仍是方向，不宜当成论文已经证成的产品结论。

给初次读者的建议

1. 先读引言两维 + 动机例子，建立「拔干净 / 依赖跟得上」的问题感。
2. 读 §3 的机制直觉（revertible effects、reactive coeffects、统一 context），跳过你不需要的公式展开。
3. 读合流性等定理的文字陈述（知道它担保什么即可）；证明细节可留到真要核验时。
4. 读 §5 Koishi，关心工程可行性时值得看；同时盯紧 v3/v4 脚注。
5. Discussion 挑着读（系统边界最重要）；Related Work 与大段证明按需跳过。

总评：方向对，理论硬，验证嫩，篇幅长。 真正贡献不在「插件难卸载」这个老问题上，而在把时空可组合性做成可运行的范式，并尝试给出交错动态组合下的形式化承重——尤其是合流性。但形式化对象与生产主线未完全对齐，单一生态验证不够充分，88 页对核心思想过厚。

值得认真读，不适合当作已经闭合验证的结论来引用。若你只关心「它做了什么、为什么对」，本文这一节就够了；若要跟进证明或实现细节，再打开 GitHub 上的 PDF。

参考

• Shi, Zhang, Cui — A Programming Paradigm for Spatiotemporal Composability（cordiverse/paper，预印本）
• 站内：Harness Engineering、AI Harness 作为复合函数