时空可组合性：为什么改一行代码要重启整个软件
「为什么改一行代码，就要重启整个软件？」——这个问题太日常，日常到没人觉得它是理论问题。北京大学与 DeepSeek 的论文《A Programming Paradigm for Spatiotemporal Composability》（arXiv:2608.25512，92 页，2026-08-26 提交）给出的…
「为什么改一行代码，就要重启整个软件？」——这个问题太日常，日常到没人觉得它是理论问题。北京大学与 DeepSeek 的论文《A Programming Paradigm for Spatiotemporal Composability》（arXiv:2608.25512，92 页，2026-08-26 提交）给出的答案很不客气：因为动态组合一直没有形式化基础。静态组合有六十年的理论积累（类型系统、λ 演算、模块系统），而「组件在运行时装上、拆下、重配」这件事，形式化答卷接近空白。工业界一直在用两个粗粒度替身硬扛：操作系统提供进程粒度的撤销（重启），容器编排器提供服务粒度的依赖管理（滚动重建+冗余副本）。论文管这叫 coarse-grained substitute——粗糙替身。
替身有多粗糙，论文给了一组实测画像：VSCode 装机量 top 100 扩展中，87 个含可执行代码——移除任意一个都要重启整个宿主进程，连带所有已加载扩展；依赖声明机制 extensionDependencies 形同虚设，top 100 里只有 7 个在用（Marketplace 2026-06-09 数据）。VSCode 的 deactivate 钩子只是宿主退出时的优雅关闭回调，还把「清理」与「创建」拆在两处，违反 locality of concern——完整清理在结构上就不可验证。
重启不是撤销，是同归于尽式的全量丢弃。这篇论文做的事，是把「撤销」和「依赖」从进程粒度拉回组件粒度，并补上整套形式化。
一、病理解剖：动态组合的正交两维
论文把问题切成两个互相独立的维度：
- 时间可组合性（temporal composability）：组件卸载时，能完整撤销它产生过的一切副作用。改代码之所以要重启，是因为进程内没有任何机制记住「哪个状态是谁改的、怎么改回去」——重启成了唯一的"通用逆函数"。
- 空间可组合性（spatial composability）：组件能声明依赖，运行时能响应式地管理依赖——依赖满足才激活，上游消失则自动失活，装卸顺序永远安全。
二、理论核心：三个概念升级（概念提炼）
论文的方法论一句话：把效应（effect）与共效应（coeffect）这对经典 PL 概念，从类型系统的静态注解提升为运行时机制。
1. 可逆效应（revertible effects）→ 时间维。经典效应系统（Moggi 的单子语义、Plotkin–Power 的代数效应、Koka/Eff/OCaml 5 的 handler）在编译期检查"会发生什么"；Cordis 把每个效应做成自带逆函数的运行时对象：效应函数 𝔈Γ ≔ Γ → Γ × (Γ→Γ)，执行返回新上下文 δ 和逆函数 g，g 由运行时持有，组件卸载时按 LIFO 逆序执行。撤销从"重启"变成"逆放"。有一个精妙的细节：见证义务只要求 g 在"它被应用的那个状态"上是逆（g(δ)=γ），不要求全局可逆——这让"部分可逆"的操作也能被诚实建模。
2. 响应式共效应（reactive coeffects）→ 空间维。共效应（上下文需求，comonad 一脉）从编译期分级变成运行时订阅：上下文每次变化都按组件声明的共效应规格分类为激活/失活/中性，驱动组件的启停。依赖解析带 realm 隔离（组件看不见彼此的私有上下文）与拦截层。VSCode 的 extensionDependencies 之所以没人用，是因为声明了也没有运行时语义；这里声明本身就是执行语义。
3. 上下文范式（context paradigm）→ 统一。把效应上下文与共效应上下文统一为单一上下文类型，一切效应与共效应都经它中介，诱导出观测等价：不同组件的效应交错执行而互不干扰。组件=这两套机制的结合，构成动态组合演算（fiber + 惯性状态机），元理论五件套：类型保持（Th 68）、时间可组合（Cor 69）、空间可组合（Th 70）、终止（Th 73）、配置确定性（Th 80）——最终状态只由最终配置决定，与装卸路径无关。这条"路径无关"是声明式配置的理论保票：配置文件 diff 出什么就挂/卸什么，中间经历多少轮折腾都无所谓。
顺带两个工程亮点：HMR（热模块替换）三阶段——模块分类不动点、陈旧入口检测、带回滚的事务性重载——不需要开发者手工标注 accept 边界（Webpack/Vite 的噩梦）；系统边界理论把操作分成两段：acquisition（open/close、malloc/free、fork/kill——边界内、可逆）与 emission（write/send——字节出了网卡就收不回，诚实记为不可逆）。共效应可以通过"再具体化"外部位置移动边界，但论文明说这是 trade-off 不是免费午餐。
三、动态组合方案对比
| 方案 | 时间维撤销 | 空间维依赖 | 粒度 | 代价/义务 |
|---|---|---|---|---|
| 重启进程 | ✔ 全量丢弃 | ✘ | 进程 | 状态全失 + 中断 |
| VSCode 扩展 | ✘（重启宿主） | 名存实亡（top100 仅 7 用） | 扩展 | activate/deactivate 割裂 |
| Webpack/Vite HMR | 部分，需手工 accept 边界 | ✘ | 模块 | 边界标注义务在开发者 |
| K8s 滚动更新 | 重建副本 | ✔ 服务发现 | 服务 | 冗余副本 + 秒~分钟延迟 |
| Cordis | ✔ 效应级 LIFO 逆放 | ✔ 声明式 + 响应式启停 | 组件（fiber） | 声明效应/依赖 + 见证义务 |
四、从 Koishi 到 dsh：实践先于理论七年
这篇论文最不寻常的地方是方向倒置：不是先有理论再有实现，而是一个跑了七年的社区工程被追认为理论。一作 Yifan Shi（北大&DeepSeek，即 Koishi/Cordis 作者 Shigma）2019 年起做跨平台聊天机器人框架 Koishi（6100+ star），2022 年把插件内核抽出为 Cordis 元框架（7800+ star），在 4000+ 社区插件、四年生产环境里验证——不过是 v3。论文形式化的是重新设计的 v4，Koishi 自己都还没用上。
时间线：8 月 13 日，DeepSeek 发布开源 agent harness dsh（deepseek-ai/deepseek-harness，MIT，Node.js，HN 747 分登顶），论文仓库 cordiverse/paper 同日上线（已 2900+ star）；8 月 26 日论文挂上 arXiv。dsh 的激进之处是 everything-is-a-plugin：模型适配器、工具注册表、会话日志、沙箱、agent loop、UI——全是可装卸的 Cordis 插件。配置文件不是挂在静态系统上的设置面板，而是组合引擎本身的接口。开源的含义因此升了一级：open license 让代码可检查，插件内核让代码可变形——换沙箱、换模型后端、换 UI 是挂插件，不是维护一个 fork。DeepSeek 还开了 dsh-plugin topic 和 Discord 社区，生态意图明显。
五、独立思考
其一，这是「接口丢结构」主线的正面教材。 重启诅咒的病根：进程接口把「哪个状态属于哪个组件」的结构整个丢弃，于是只能全量丢弃。上下文范式是一个让结构在接口处幸存的仲裁层——dispose 累加器记住「谁污染了什么、怎么撤销」，依赖图记住「谁在等谁」。前九次验证都在讲坏接口怎么丢关键结构，这次是反面：当接口忠实地保留归属结构，"撤销"从架构难题坍缩为机械操作。
其二，Agent 自改进闭环补上了运行时层。 此前主线的自改进谱系：Ornith-1.5 在权重层（自己出题自己学）、Chain-of-Experience 在经验层、Metan 在代码层——harness 本体（agent 跑在里面的运行时）始终是空白。论文结论明确点名：self-evolving agent harness——AI 持续生成并替换自己的 harness 组件、几乎无人类监督——是最有吸引力的未来验证场景。而可逆性正是自改安全的物理前提：一个能重配自己技术栈、任务中途给自己加工具的 agent，只有当每次变更都可完整回滚时才值得信任。dsh 把这个前提做成了开源基建。
其三，可逆性经济学：变更成本坍缩。 回接验证带宽主线：当每次尝试都可逆，试验的期望成本≈单次正向成本（失败即逆放），审计被回滚替代——验证从事前审计变成事后试错，这是"生成免费后瓶颈只剩验证带宽"的又一条泄压路径。但要诚实指出边界：逆函数的正确性是作者义务，运行时只保证结构（LIFO 顺序、路径无关），不验证语义——逆写错了，运行时会忠实地执行你的错误撤销。well-formedness ≠ faithfulness 在这里第十次出现：形式验证的最后一公里仍然是人（或未来的形式化逆函数合成）。
其四，遗忘的结构学。 与 Synapse 篇（让 Agent 学会遗忘）正好对位：那是记忆系统层面的遗忘，这是运行时层面的遗忘——而干净遗忘的前提恰恰是记住"如何撤销"。dispose 累加器就是一张 undo 菜单；卸载不是删除，是逆放。系统级遗忘与认知级遗忘结构同构：没有可追溯的写入路径，就没有干净的遗忘。
其五，诚实边界与社区噪音并存。 emission 不可逆（发出去的包收不回）——论文没有假装万物可逆，系统边界就是对物理世界不可逆性的让步。与此同时 HN 上"Spatiotemporal Composability 读起来像 word salad / 广义相对论？"的吐槽与 747 分热度共存：术语玄学是真，痛点共鸣也是真。每个被 VSCode 重启打过脸的开发者都懂后者。
观察点
三个：① dsh-plugin 生态的插件数量与质量（开源 harness 的护城河在插件生态，DeepSeek 已摆明车马）；② 论文标注 under active revision，arXiv 永远是最新版，元理论若有松动值得追；③ 最值得等的是论文自己指出的实证——self-evolving harness 的公开演示。如果年内出现「agent 改写自己的 harness 且完整回滚」的案例，软件就拿到了自己的 GPT-3 时刻门票：变更的定义成本坍缩到"挂一个插件"。
信源：arXiv:2608.25512（92 页，含 VSCode Marketplace 2026-06-09 实测数据）；github.com/cordiverse/paper、cordiverse/cordis、koishijs/koishi、deepseek-ai/deepseek-harness；HN #49285244（747 分）。所有数字经原文核对。转载请注明出处。