时空可组合性：DeepSeek 给「一切皆插件」写的形式化地基
深读北大 + DeepSeek《时空可组合性编程范式》：动态组合缺的不是插件机制，而是可证明的插拔。可逆效应让卸载变成结构保证，响应式余效应让依赖跟着运行时醒停，汇合定理保证热插拔停下来长得像从零装好——Cordis / Koishi / DeepSeek Harness 共用的那层地基。
上一篇写 DeepSeek Harness时，有一句话几乎被当成口号反复引用：「一切皆插件」。底下真正撑住这句话的， 不是又一个 IoC 容器，而是一篇 88 页的预印本——北京大学与 DeepSeek-AI 的 Yifan Shi、Wei Zhang、Tianyi Cui 合写的A Programming Paradigm for Spatiotemporal Composability（时空可组合性编程范式，草稿日期 2026 年 8 月 13 日）。仓库明确写着：内容还在大幅修订， 引用以最新版为准。这一篇就把这篇论文读透：它到底在解决什么、两套机制怎么咬合、 演算里最硬的那句保证是什么，以及为什么自进化 Agent harness 会把它当成地基。
一句话先放在这儿：时间上，拔掉一个组件，它改过的环境要能收回； 空间上，组件之间的依赖要能声明，并且跟着运行时的变化自动醒、自动停。论文把这两件事从「靠作者自觉」变成「运行时的结构不变量」，实现就叫Cordis。
一、缺的不是插件机制，是动态组合的地基
软件工程最老的原则之一是组合：用更小的零件拼出更大的系统。传统组合是静态的—— 函数调用、模块 import、类继承，编译期就钉死，跑起来不再改拓扑。现代软件越来越不吃这一套。 插件要热装热卸，Agent harness 要在服务请求的同时改自己的工具、权限、记忆和子代理。 论文把这种「零件在运行时到达、离开、换身份」叫做 dynamic composition（动态组合）。
麻烦在于：静态组合有类型论、模块系统、代数效应这些厚实的形式化工具；动态组合在工程里到处都是， 理论上却一直偏薄。常见做法是把问题推给更粗的粒度——进程一崩就重启，服务依赖丢给容器编排。 论文认为这是粒度错配：今天真正在组合的，已经是同一地址空间里的组件， 不是进程，也不是 Pod。
1. 插件系统：VSCode 几乎拔不掉正在跑的扩展
论文拿 VSCode 当典型。扩展跑在共享的 extension host 里，activate 一旦执行， 禁用或卸载单个扩展通常要重启整个 host，别的扩展一起遭殃。主题、快捷键这类纯声明扩展可以随便卸； 但 2026 年 6 月 9 日他们统计过 Marketplace 安装量前 100 的扩展：87 个带可执行代码，卸掉就要重启。官方的 deactivate 只是进程退出时的礼貌回调， 不是热卸载。更糟的是，创建副作用在 activate，清理在 deactivate， 两头分离，完不完整全靠作者记得。
空间这边同样稀薄。VSCode 有 extensionDependencies，但前 100 里只有 7 个对非内置扩展声明了依赖。 扩展主要通过宿主提供的固定扩展点（命令、视图、语言功能）往上挂，而不是彼此依赖； 跨扩展交互走 vscode.extensions.getExtension(...).exports，默认还是 any。 论文说，这不是 VSCode 独有的病，插件系统里反复出现，只是程度不同。
2. 自进化 Agent：改自己的时候，重启是付不起的税
更尖锐的场景是论文反复点名的 self-evolving agent harness。现代 Agent 要组合工具、沙箱、会话、记忆、 子代理和工作流；未来的 harness 还可能自己生成、部署对自己组件的修改，同时不停服务。 每一次这样的修改，都是一次动态组合。
没有时间可组合性：每次自我修改都得整进程重启，缓存、连接、进行中的任务全丢；改得勤，不可用时间会叠成灾难； 更狠的是，一次错误的自我修改可能把用来恢复的那个进程也弄死。没有空间可组合性：每个模块都得自己侦测依赖的出现、消失、换人， 只能靠临时约定；天真的「换一段代码」会悄悄弄坏依赖方，或者把环状依赖留到重载那一刻才爆。
3. 粗粒度替身：进程和容器能顶，但顶得很贵
操作系统在进程粒度上给了时间可组合性（杀进程等于收回它碰过的大部分内核资源）； 容器编排在服务粒度上给了空间可组合性。多数软件就靠这两招凑合：模块坏了重启进程， 依赖坏了交给编排器。论文把代价写得很具体：重启会丢掉进程内状态，重建要数秒到数分钟； 为了中间还能服务，还得冗余副本。容器也表达不了「共享地址空间的组件依赖」， 本可以是一次本地函数调用的交互，被逼成跨网络。
所以这篇论文的野心很明确：在组件自己的粒度上，把效应和依赖管起来， 而不是每次都逃到进程和 Pod 的边界外面去。
二、两个正交维度：时间收回，空间响应
论文给动态组合补了两个正交维度。说正交，是因为它们管的不是同一件事，也不能互相替代。
| 时间可组合性 Temporal | 空间可组合性 Spatial | |
|---|---|---|
| 问的是 | 组件卸掉后，它对共享环境的修改能不能完全、安全地反转 | 组件之间的依赖能不能被声明、发现，并随变化被解析 |
| 静态世界里 | 词法作用域：RAII、bracket | 模块 import 解析 |
| 动态世界难在 | 副作用活得比词法作用域长，范围事先圈不住 | 依赖会在运行时出现、消失、换身份 |
| 论文的机制 | 可逆效应 revertible effects | 响应式余效应 reactive coeffects |
| 类型论祖宗 | 效应系统：计算改了环境什么 | 余效应系统：计算需要环境什么 |
经典效应 / 余效应是编译期工具：效应在固定词法范围里被跟踪、被 handler 消掉；余效应标注对着执行前就定好的上下文做检查。 插件是部署之后才装上的，依赖是配置跑起来才长出来的——没有固定作用域能框住它。 论文的策略因此不是「再给类型系统加几个注解」，而是把效应和余效应的结构变成运行时真的能操作的对象。
三、可逆效应：每次动手，都给运行时一张撤销单
时间可组合性要的是：组件卸掉之后，共享环境回到组合之前。论文把一次效应写成：
拿到当前上下文 Γ，产出新的上下文，以及一个逆（inverse）。 类型是
Γ → Γ × (Γ → Γ)。逆是运行时跟踪的，不是作者另外写在deactivate里的义务。
这张「撤销单」只要求左逆：g ∘ f 在这次应用发生的那个状态上成立就行， 不要求整个计算处处可逆。这一点把它和「整段程序都必须可逆」的可逆计算区分开—— 你不需要让一次网络发送在数学上可倒放，你只需要让「打开连接」这件事带一个「关闭连接」。
运行时把这些逆攒进一个累加器 φ。加载组件，就是执行一串效应、把逆按顺序叠上去；卸载组件，就是跑 φ。 后进先出永远成立：后做的事先撤，每张单都会回到它自己当初下手的那个状态。 如果两个组件的效应独立（它们的正向变换和逆彼此交换，谁也不改对方会交出的那张单）， 那还可以按任意顺序卸，卸掉一个不会把另一个的贡献一起卷走。
独立从哪里来？论文后半给出纪律：组件之间共享的位置，都要收成一个余效应键； 每个键上的操作如果可交换，两个组件的效应就独立。碰不到同一把钥匙的插件，本来就可以任意顺序拔。 碰得到、但操作不可交换的钥匙，顺序不能靠效应自己换，而要靠余效应的依赖序来排—— 这正是下一节的事。
对写插件的人，红利非常具体：你只给原子操作配逆，组合的逆由复合自动生成。 用已经可逆的操作再拼更大的操作，不用再写一遍卸载路径。论文拿 React 的 useEffect 对比： 它也让你返回 cleanup，结构上最接近；但 hook 不能进分支、循环、嵌套函数，也不能是 async / iterator， 因此拼不出「复合的逆」。VSCode 那种 activate / deactivate 分家就更远——漏写一个清理，资源就静默泄漏。
四、响应式余效应：依赖是规格，不是一张不会动的查找表
余效应是效应的对偶：效应说「我对外界做了什么」，余效应说「我需要外界给我什么」。 论文把组件的依赖写成规格 d（一组键），上下文 Σ 是一张带类型的偏函数表。 规格满足，当且仅当这些键都在表里。每次效应把 Σ 改成 Σ′，系统按规格把这次变化分成三类：
- 激活 activating：刚才不满足，现在满足 → 执行组件的效应（带着完整跟踪）；
- 停用 deactivating：刚才满足，现在不满足 → 跑累加器，收回效应；
- 中性 neutral：满足与否没变 → 什么都不做。
关键的咬合在这里：往表里 set 一个依赖，本身就是一个可逆效应。 登记服务会被自动跟踪；提供方卸载时，这条登记会作为逆被删掉，并再次 notify。 效应管收回，余效应管通知，两套机制用同一条轨道。
只保证「自己的规格」还不够。全局还要管别人：提供方撤绑定之前，所有已经解析到它的依赖方必须先停用； 一次加载过程中，组件对着哪份解析在装，装到一半不能偷偷换成另一份。论文后半的演算把这两条写成定理； 实现上对应三个很具体的动作：
- 提供方一进入卸载，就先停止对外提供，依赖方立刻看到规格不再满足；
- 依赖方在提供方的绑定都还在的时候完成自己的拆除——拆除过程中还能读到自己当初认准的那份依赖；
- 提供方等依赖方都停干净，再跑自己的累加器。
翻译成人话：不是提供方一卸，依赖方抓到空指针；而是依赖方先有序下班，提供方再关门。
隔离与拦截：同一把钥匙，可以指向不同的房间，也可以在门口加政策
扁平的一张表不够用。论文又加了两样，都不改共享表本身，而是派生一个子上下文：
- 隔离 isolation：逻辑键先映射到 realm，再取真正的值。同一把钥匙
database，测试沙箱和生产可以绑到完全不同的实例。这是运行时的特设多态。 - 拦截 interception：访问时叠一层元数据（路径白名单、只读、配额），不改依赖值本身。 外层上下文的元数据优先，所以编排器可以给社区插件加「只能读某些目录」，不用改提供方，也不用改插件源码。
两者都是「派生实现」：父上下文不动，扔掉子上下文，隔离和拦截就一起消失，不必再攒一张逆。
五、上下文范式：一个 ctx，同时是「我改了什么」和「我需要什么」
效应上下文是「当前状态 + 累加器」，余效应上下文是「依赖表」。论文把它们焊成同一个递归类型 Γ∞： 每一层都带着自己的状态、自己的撤销累加器、自己的依赖表。父上下文聚合子上下文的效应，形成一棵树。 「插件」这个词在这里不是比喻，论文写的就是字面意思：
- 加载 = 执行效应 = 插上；
- 卸载 = 收回效应 = 拔掉，而且原则上不影响旁边还在跑的组件；
- 不同层的组件可独立插拔，父级负责把孩子的账收齐。
这被明确称为一种编程范式，夹在两条老路中间：
| 函数式（显式穿状态） | 命令式 / OOP（隐式乱改） | 上下文范式 | |
|---|---|---|---|
| 效应怎么走 | State monad，层层传递 | 随便改共享状态 | 所有修改都经过 ctx |
| 依赖怎么走 | Reader / 环境参数 | 服务定位器、全局单例 | 声明 inject，从 ctx 读 |
| 好处 | 可追踪、可等式推理 | 写起来省事 | 可追踪，同时不必把 ctx 手工传到每个纯计算里 |
| 代价 | 调用链被状态参数淹没 | 改一处，远处的不变量静默碎掉 | 原子效应仍要作者给对逆；共享位置都得收成键 |
还有一个诚实的细节：数学定理里的「收回后状态相等」在物理世界里做不到。free 不会把堆布局恢复成 malloc 之前；生成式的名字丢掉以后，下一次会拿到新的。 论文因此改成观测等价：两个状态，如果通过余效应上那些操作看不出差别，就算同一个。 没绑到任何键上的内部细节（堆布局、一次性名字）被故意忘掉。你收回的不是宇宙的每一个比特， 而是观察者还能观察到的那一层。
六、演算里最硬的一句：热插拔走遍所有路，停下来长得一样
单看一个组件的效应和规格，还只是「局部」保证。要把保证抬到「一堆组件交错着装、卸、重载」， 论文给了一个动态组合演算。组件是三元组 (d, p, e)：声明要什么、可能提供什么、以及带着逆的效应函数。 一次实例化叫 fiber，带着自己的生命周期。
| 生命周期 | 在干什么 |
|---|---|
| INACTIVE | 未激活；规格不满足，或者已经被卸干净 |
| LOADING | 正在执行效应（论文里叫 Reloading） |
| ACTIVE | 在服务；对外提供自己挂上的键 |
| UNLOADING | 已经停止对外提供，正在等依赖方，再跑累加器 |
真实运行时还有三件静态理想化里没有的事：过渡不是原子的、中间会异步、还会失败。 论文用 惯性 inertia 处理：reload 或 unload 一旦开始，先跑完，再看目标有没有变； 变了就链式切到下一趟，而不是半路改主意。加载过程中如果依赖的提供方换人了， 当前这一步可以落地，但整段过渡会被 divert，已经装上的用累加器退回去。
元理论里，对人最有用的是这几条（编号按论文）：
- 恢复精确（定理 61 / 推论 62）：卸掉一个 fiber，拿走的只是它自己的贡献。 旁边组件在这段时间里做的事还在。失败的 fiber 对外贡献也是零。
- 依赖有序（定理 63）：组件只在规格满足时开始过渡；提供方的生命周期包住依赖方的生命周期； 依赖方在整段插拔期间读到的是同一份绑定。
- 解析不漂移（定理 64）：一次加载认准的提供方集合，中途要么一直对着它装完， 要么整段回滚。不会出现「前半用 A 的 llm、后半用 B 的 llm」。
- 进展（定理 66）：依赖图无环时不会死锁，过渡次数有限，系统会停到静止态。
- 汇合（定理 73）：这是整篇最值钱的一句。任意装、卸、换提供方之后，只要停下来、没有失败，得到的状态（在换名意义下）等于：按依赖序，把最终还该活着的组件从零装一遍。动态历史不留痕迹。
汇合的工程含义：你可以按「最终配置」思考一个 Cordis 应用，而不必回放它热更新过多少次。编排器加一个组件、去掉一个、换掉提供方再换回来，停稳之后的世界，和一开始就写成最终那份配置是一样的。
论文自己划了边界：保证的是状态，不是沿途发出去的那些副作用（打到网上的包、写到别人也能写的文件）。 那是下一节的系统边界，不是演算在偷懒。
七、Cordis：把定理收成一组很小的 API
Cordis 被写成元框架：不规定你在做聊天机器人、Web 还是 Agent，只提供通用的动态组合语义。 分三层：核心库、组件加载器、以及像 Koishi 这样的领域框架。理论和代码的对应，论文用一张大表钉死， 这里只留写代码时会碰到的那几个名字：
| 你调用的 | 它在理论里是 |
|---|---|
ctx.effect(callback) | 把效应函数抬到带累加器的上下文上，返回 dispose |
ctx.set / ctx.get | 余效应的登记与读取；set 本身走 effect |
ctx.use(component) | 登记一个 fiber，父级卸载会级联收回孩子 |
ctx.isolate / ctx.intercept | 派生隔离域 / 访问元数据 |
ctx.llm 这种属性访问 | Proxy 按 fiber 的 committed view 鉴权，未声明就报错 |
fiber.dispose | 累加器 φ |
核心不变量仍然是：凡是经过 ctx 的修改，卸载时都会被跟踪并收回。运行时并不证明你给的 inverse 一定对——那是组件作者的义务，演算的恢复定理建立在「逆真的能撤」之上。 漏写或写错原子逆，结构保证帮不了你。论文把这条讲得很干净，没有假装类型系统已经替你验了逆。
加载器面向编排器，不面向插件作者。你写一份声明式配置（id、模块 URL、isolate、intercept、config、disabled）， 加载器把它变成 fiber 操作。配置一改，不是整棵拆掉重建，而是按字段做最小动作： url 变了才重建，intercept 可以原地改（读时才看），disabled 只触发卸/装。 汇合定理在这里变成一句产品语言：不管中间怎么调和，停下来等于从零加载最终配置。
热模块替换（HMR）把同一套模式用到模块级。因为 fiber 已经圈住了组件的效应和余效应， 换模块 = 丢掉旧 fiber（收回一切）+ 用新模块再 ctx.use。 不需要 Webpack / Vite 那种手写 accept 边界。失败则整笔事务回滚，系统不会停在半更新状态。
案例是 Koishi：在 Cordis 上长了四年的聊天机器人框架，社区插件超过 4000 个。 论文用来说明三件事：这套原语够撑一个完整生产系统；同一模型既能跑在 Node 服务端，也能跑在浏览器控制台； 开源生态里，插件和它的依赖常常不是同一作者写的，双方只约定余效应键，响应式解析仍然能把装配维持住。 控制台里禁用一个插件，效应当场收回；开发时保存文件，HMR 只重放被编辑的插件，别处的缓存和长连接还在。
论文也承认这是存在性证据，不是对照实验：目前主要是 TypeScript 上的一个生态， Koishi 用的还是 Cordis v3，论文讲的是语义更干净的 v4。开销和开发效率对比，留给未来工作。
八、边界、互依赖，以及它真正想撑住的东西
1. 系统边界：能收回的，和只能补偿的
不是所有副作用都住在 Γ 里。论文用系统边界切开：系统能独占修改、并且能恢复到修改前的位置，算里面，跟踪、可收回； 做不到的，算外面，作用等价于恒等变换，不跟踪。余效应可以把外面的位置「收编」进来—— 例如只把文件访问收成一组带逆的操作——但那是权衡，不是免费午餐。
一次对外操作通常分两截。获取 acquisition（open、malloc、fork） 在边界内：拿到描述符、装进表，卸载时 close / free / kill。发射 emission（write 出去的字节、send 上的数据包）穿过边界， 别人已经读到了，逆不了。真要处理发射，只剩两条路：先扣住，等内部状态确定会留下来再发出去； 或者补偿（删掉刚创建的文件、退掉刚扣的款）。补偿可以按同样的后进先出排，但观测等价更粗， 交换律要重新证。
2. 互依赖不是死锁，是「永远醒不来」
A 要 B 提供的键，B 要 A 提供的键，两边的满足谓词永远不会同时为真，两个组件会永久 INACTIVE。 这和并发死锁不同：它从声明就能看出来，加载时就能报。论文的建议是拆细：双向交互拆成两个单向绑定， 用更小的集成组件去接两边的核心。组件变多，但不影响正确性和运行时性能；用户还能只加载自己要的那几条绑定。 代价是认知负担，要用打包、约定连线和脚手架来擦。
3. 论文自己点名的下一站：会改自己的 Agent
结尾把未来验证方向写得很直：不只是人维护的插件生态，而是自进化 agent harness——AI 持续生成并替换自己的 harness 组件，几乎没有人盯着。 那正是 DeepSeek Harness 把「模型、工具、记忆、loop、甚至 UI」全部做成插件的原因： 插拔如果只是工程约定，自我修改第一次写错就会把现场搞脏；插拔如果是可证的收回和可证的依赖序， 自我修改才有资格发生在还在服务的进程里。
上一篇里 DSH 的几条硬规则，其实都能在这篇论文里找到影子。 「先记录意图，再执行副作用」是把不可逆的发射尽量推到边界之外、让边界之内保持可收回； 「模型可见即已记录」是给会话状态一条可重建的获取记录； 「一切皆插件、没有特权内核」就是 Γ∞ 那棵上下文树：没有一块效果可以逃出 fiber 的累加器。 论文没有把 DSH 写成案例——案例是 Koishi——但它把自进化 harness 写成了这套范式该去证明自己的地方。
小结
这不是一篇教你怎么调 Agent 的教程，是一篇给「运行时还能安全拆装的软件」补地基的理论文章。 它从 VSCode 拔不掉扩展、进程重启太贵、Agent 不敢热着改自己出发，把类型论里的效应和余效应抬到运行时， 收成两句话：
可逆效应让卸载变成结构保证，而不是 deactivate 里的自觉； 响应式余效应让依赖拓扑跟着运行时变，而不是重启后再解析一遍。两者焊在同一个上下文里，交错加载的系统仍然能停在「仿佛从零装好最终配置」的状态上。
落地不神秘：ctx.effect、ctx.set、ctx.use， 再加一份声明式配置和一次不需要 accept 边界的 HMR。Koishi 的四千插件证明它能在开放生态里活； DeepSeek Harness 则是同一套思想被推到 Agent 执行层之后的样子。
读这篇论文最值得带走的，不是那些交换图表，而是一个判断：当软件开始自己改自己，插件就不再是产品功能，而是必须被证明的运行时不变量。时空可组合性，就是 DeepSeek 给这条不变量写下的那套语言。