Skip to main content

Cordis：用可逆效应与响应式余效应，把运行时换组件变成有定理兜底的乐高

Paper Info​

Overview​

  1. 论文身份：DeepSeek Harness 的理论地基论文，作者来自北京大学与 DeepSeek，理论落在开源元框架 Cordis 上；DeepSeek 开源的 DSH 在仓库文档中声明由 Cordis 驱动。

  2. 核心问题：运行时动态组合（加载、卸载、替换组件）长期缺少形式化基础，论文把它拆成时间可组合性（卸载后副作用完整回收）与空间可组合性（依赖声明与响应式管理）两个正交维度。

  3. 方法一句话：把程序语言理论里的效应与余效应从编译期静态分析改造成运行时机制——每次环境修改自带逆变换（可逆效应），每份依赖写成声明式规格并随上下文变化分类响应（响应式余效应）。

  4. 关键机制一：逆变换由调用方在执行点当场构造并满足见证约束，运行时把各步逆变换按相反顺序复合成后进先出的累加器，组件卸载即调用累加器把环境还原到加载前。

  5. 关键机制二：提供者卸载分两阶段，先让服务对外不可见、等所有消费者完成清理，再执行累加器释放资源；加载按效应迭代分步推进，目标变化在迭代边界分流卸载，在途异步操作落地后即转卸载，失败回滚并记录在组件实例上。

  6. 形式化保证：保持性、恢复精确性、保序性、进度、合流性五条元定理，分别依赖良构注册表、操作两两独立、依赖无环且迭代有界、无失败且静止等明确前提；合流性明确不覆盖失败情形。

  7. 观测等价：恢复是"外部观察者无法区分"意义的等价，不是字节级还原，由此内存分配布局、生成性名称等实现差异被吸收，多组件交错修改下的效应独立性才成立。

  8. 实现与案例：Cordis 用单原语 ctx.effect 跟踪全部上下文修改，插件作者无需另写卸载路径；事务式热模块替换导入失败可整体回滚；Koishi 生态四年积累四千多个社区插件，属单一 TypeScript 生态观察性案例而非受控对比。

  9. 系列定位：Meta-Harness、AHE、Continual Harness 回答 harness 能否被自动搜索与演化，Autogenesis 给出协议层直觉，本篇回答每一次热替换的正确性由什么保证，可视为 harness 自动优化系列的形式化地基篇。

  10. 边界判断：发射型操作（写共享文件、发网络数据）不可恢复，只能靠延迟提交或应用层补偿；键的可交换性是提供者接口义务；暂无抽象开销的定量数据；不可信代码仍需外部沙箱。

核心内容解读​

为什么重启已经不够用了​

插件系统与自进化智能体 harness 都要在运行时加载、卸载、替换组件，但正确性长期靠工程经验兜底。论文给出两个扎眼数字：VS Code 装机量前 100 的扩展中 87 个含可执行代码却无法单独卸载，而声明了扩展间依赖的只有 7 个，跨扩展拿到的接口还是无类型的 any。换句话说，主流插件生态的"动态组合"在工程层面其实是"半动态组合"——能装不能拆、或者拆得干净与否全凭作者自觉。

把代价拆开看：时间上重启把进程里积累的缓存、长连接、算到一半的任务全部丢弃，重建成本从几秒到几分钟不等，这段时间要么服务中断、要么靠冗余副本硬顶；空间上容器编排只能管到服务粒度，同一进程里两个模块的依赖它表达不了，本来一次函数调用被迫走进程间通信。论文进一步指出，自进化 harness 把这个问题推到了临界点——如果 harness 在服务请求的同时还在生成并替换自己的组件，每次自修改都是一次动态组合，重启代价会放大到不可用；更糟的是，一次错误的自修改若把负责恢复的进程也搞挂了，系统连自救的机会都没有。

程序语言理论的旧工具为何被改造​

效应（effect）描述计算如何修改环境，余效应（coeffect）描述计算依赖环境的什么。这两个概念早已存在于程序语言理论中，但都只服务于编译期静态分析：作用域在写代码时就已经固定，运行时才加载的插件没有词法作用域可套，运行时才冒出来的依赖编译期也算不到。论文的取舍很直接——把这些概念从编译期分析对象实体化成运行时能直接操作的对象，把"分析"换成"机制"。

时间维度上的核心机制叫可逆效应：系统里每一次对环境的修改（注册路由、加事件监听、注入服务）都不能只交出新状态，必须同时交出逆操作说明这一步怎么撤。运行时把这些逆操作按相反顺序复合成一条后进先出的撤销链，论文里叫累加器。组件卸载即调用累加器，环境回到加载前的状态。逆操作必须由调用方在执行点当场构造并满足见证约束——怎么撤取决于执行时的现场（分配的句柄、注册时占用的键），框架统一生成的逆操作覆盖不了这种执行上下文。

观测等价与多组件交错的独立性​

单个组件的撤销链好理解，但多个组件交错改环境时，A 的逆操作执行时状态已经被 B 动过了，还测得准吗？这引出效应独立性：如果两个组件的操作两两可交换——你先注册我再注册和反过来结果一样——任意顺序撤销都能回到初始状态。论文用观测等价放宽了恢复标准：两个状态只要对外提供的服务行为一致就算等价，不要求内存逐字节相同。比如 free 之后堆的布局不会回到 malloc 之前，但只要没有任何操作能看出区别，就算恢复成功。借助这层放宽，内存分配器换块地址这类实现差异才不会破坏可交换性。

可交换性既是判别条件也是接口义务：网络路由、事件监听列表里加条目顺序无关则可交换；中间件链有先后则不可交换；好在组件之间注册依赖这件事本身天然可交换，因为不同组件提供的键被要求互不重叠，谁先注册谁后注册都不打架。

空间维度：声明式依赖与响应式余效应​

时间维度讲清楚后，空间维度转向依赖管理。组件把依赖写成声明式规格："我需要哪些键"。系统维护一张全局依赖表记录谁在提供什么服务，每次表有变化就用每个组件的规格去比对，把变化分成三类：让组件从缺依赖变齐了的激活它、让它失火的反向变化、其余中性不动的中性变化。组件只在依赖全部就绪时才激活，依赖消失时被带着走，卸载流程不会等到运行时才撞上缺失的依赖。

同一个键在不同子上下文里可以解析成不同实例（隔离），访问键时还能被外层附加一层元数据做约束（拦截），比如只给社区插件只读的数据库权限。

两阶段卸载：避免"提供者先撤、消费者还在用"​

空间维度最容易出事故的是卸载顺序——提供者先撤了，消费者还在用怎么办？论文给了一个看起来"会死锁"但实际上安全的设计。

两阶段卸载的过程是：第一步，提供者要退出时只宣告自己提供的服务立刻从全局表撤下，新组件再也解析不到它，但他自己的资源先不释放，激活时记下的依赖解析结果也保留，这样依赖它的消费者还能正常跑自己的清理代码（关连接池时能把连接还回去）；第二步有个守护条件，等所有引用它的消费者都退场了，才执行累加器真正释放底层资源。

死锁担忧的解除靠两点：关键在第一阶段已经服务从全局表撤掉了，不会再有新的解析指向它；已经在引用他的消费者因为依赖没了各自都在卸载的路上，他们走完守护条件自然放开。配套有个进度定理，在依赖关系无环、组件数量有限、每次激活的迭代步数有界的前提下，系统总能走到所有组件都到达目标的静止状态，不会卡住。

组件激活不是一口气完成的，是一串效应迭代，每步之间都有检查点；目标变了就在最近的检查点分流进卸载路径，把已经积累的那部分撤掉；异步场景再加一条惯性规则，已经发出去的操作必须落地，落地后立刻转卸载，不允许一次转换跨着两个不同的依赖解析混着用；加载中途报错就把已做的部分回滚，错误记在这个组件实例上，不传染给父组件。

五条元定理与它们的诚实边界​

这套机制最后拼成一种递归的上下文类型：每层上下文带三样东西（自己的状态、能撤销本层修改的累加器、一张承载依赖的余效应表），组件是静态定义，跑起来的实例叫先城，带生命周期状态（未激活、加载中、激活、卸载中），整个演算只有十条规则。证据形态与一般系统论文不同，主证据是五条带明确前提的元定理：

  • 保持性：每条规则执行完，系统的注册表结构依然良构。
  • 恢复精确性：在操作两两独立的前提下，跑一个组件的累加器，撤掉的正好是他的贡献，而且只撤他的。
  • 保序性：提供者的存活区间严格包含消费者的，所以从结构上不存在访问已销毁依赖。
  • 进度：在依赖无环、组件有限、激活迭代有界的前提下，系统必然走到静止状态。
  • 合流性：同一组编排动作不管中间怎么交错执行，最终结果在重命名和观测等价的意义下相同。

要警惕的是合流性的前提最硬——要求执行到静止状态、无组件失败、操作两两独立、组件在自己提供的服务上处处有定义。论文明确把失败排除在这条定理之外：一旦出现失败（而真实系统天天有失败），合流性就不适用。论文诚实地标出了形式化保证的边界：恢复精确性和保序性覆盖失败，合流性不覆盖。

实现与生产案例​

理论落到代码里非常克制。Cordis 的所有上下文修改都走唯一一个原语 ctx.effect，传一个回调进去，回调里每做一步修改就交出一个逆操作，框架自动把它们复合成累加器，组件作者不用单独写卸载路径，因为卸载逻辑是从加载过程推导出来的。

热模块替换比 Webpack HMR 强在边界从哪来：Webpack/Vite 的热替换需要开发者在代码里标注哪个模块接受热替换、旧状态怎么交接，Cordis 里每个组件的全部副作用和依赖本来就被先城圈住了，替换模块就是换线程（销毁旧的、装上新的），分三步：先按导入关系把改动模块分类，再找出受影响的组件入口，最后做事务式重载——中途任何模块导入失败（比如新代码有语法错误）就恢复快照，系统不会停在换了一半的状态。

生产环境的验证是 Koishi 这个案例。它是基于 Cordis 的开源聊天机器人框架，4 年积累了 4000 多个社区插件，从消息平台适配器到数据库驱动都有。两个观察最说明问题：一是插件作者不写卸载路径也能得到有序清理，因为逆操作是运行时自动跟踪复合的；二是运行时切换存储后端这类重配置只会重新激活依赖真正变了的插件，依赖暂时不可用的就安静等着不报错。论文自己也说这是单一 TypeScript 生态的观察性案例，证明的是"存在且被采用"而不是"和其他架构的受控对比"。

边界判断：保证到哪里就不成立​

论文把操作分成两种：获取型（打开文件、分配内存）在环境里建了记录，能跟踪能撤；发射型（写共享文件、发到网络）数据一旦出去就收不回来，不在保证范围内。要补救只有两条路：要么等状态确定持久再发，要么用应用层补偿（退款、删掉自己创建的文件），补偿可以按同样的后进先出组合但定理要重新建立。另外如果组件绕过上下文直接去摸底层对象，语言层的管控拦不住，需要真正的沙箱。

在 Harness 系列中的位置​

回到之前几期讲的 harness 自动优化系列：Meta-Harness 回答 harness 能不能被自动搜索优化；AHE 讲 coding agent 的 harness 怎么在证据和回滚约束下自动演化；Continual Harness 讲智能体在不中断的轨迹里在线改写自己的组件。这三期都在回答 harness 能不能自动演化，Autogenesis 则用协议把 prompt、tool、memory 统一成带生命周期和回滚接口的资源，算工程直觉。这一篇问的是更底层的问题：这些系统里每一次热替换、每一次组件增删，正确性到底由什么保证？HEE 的回滚靠 git 版本和工程约定，这里的回滚是有定理的运行时语义。可以说前几期在研究会自己改装的汽车，这一篇在给改装车间立安全规范。

Resources​

Last updated on by Kimi Gao