DeepSeek × 北大的 92 页 PL 论文（arXiv:2608.25512，2026-08-26 提交）：为动态组合（运行时增删/替换组件）给出形式化基础。把经典 effect/coeffect 从编译期静态分析提升为运行时机制——可逆 effect 解决时间维度（卸载即完全回滚），响应式 coeffect 解决空间维度（依赖声明+反应式生命周期），统一为 context paradigm，再给出动态组合演算与五条元定理，实现即 cordis，生产验证是 Koishi 的 4000+ 社区插件。
| 维度 | 事实 |
|---|---|
| 作者 | Yifan Shi（北大 / DeepSeek-AI，即 Koishi 作者 Shigma）、Wei Zhang（北大）、Tianyi Cui（DeepSeek-AI） |
| 分类 | cs.PL / cs.SE，92 页，1 图 2 表 |
| 实现 | Cordis（cordiverse/cordis，~7.8k stars，MIT），DeepSeek Harness 的理论底座 |
| 前身 | 理论来自已在 Koishi 生产运行 4 年的插件内核，论文是”先有代码后有形式化” |
1. 问题：动态组合缺形式化基础
传统组合是静态的（函数调用/模块导入/继承，编译期定死）。现代软件需要运行时加载、卸载、重配置组件，但实践只能退回到粗粒度机制。
两个正交维度：
- 时间可组合性（Temporal）：组件移除时，它对共享环境做的所有修改必须被完全、安全地逆转——要追踪每一次资源分配、事件注册、状态变更并保证有序回收
- 空间可组合性（Spatial）：组件能以结构化、可验证的方式声明、发现、解析彼此依赖——要管理依赖拓扑并在依赖变化时协调生命周期
静态设定下这两者分别退化为词法作用域（RAII/bracket）和模块导入解析；动态设定下显著变难：副作用不再受词法边界约束，依赖会在执行中出现/消失/换身份。
动机案例（论文用数据说话）：
- 插件系统（VSCode）：所有扩展跑在共享 extension host，无法运行时卸载单个扩展——禁用必须重启整个 host。Top 100 扩展中 87 个含可执行代码，卸载都要重启；
deactivate钩子只是进程终止时的优雅关停，且把清理逻辑与注册逻辑分离，违反 locality of concern。空间侧：extensionDependencies几乎没人用（Top 100 中仅 7 个声明），跨扩展 API 返回无类型any，无结构化契约。 - 自进化 Agent Harness：未来 harness 会在持续服务请求的同时生成并部署对自身组件的修改（模型合成工具是组件级自修改的窄前驱）。每次修改都是一次动态组合。没有时间可组合性，每次自修改都要全进程重启、丢弃累积状态，坏修改甚至能瘫痪恢复进程本身；没有空间可组合性，每个模块得自己 ad hoc 地探测依赖变化，朴素代码替换会悄悄弄坏依赖方。
- 粗粒度替代方案的代价：OS 以进程粒度提供时间可组合性、容器编排以服务粒度提供空间可组合性，但每次重启丢弃缓存/连接/中间状态（重建要秒到分钟级），冗余副本浪费资源，容器编排表达不了同地址空间内的组件依赖。粒度错配正是本文要填的坑。
2. 核心形式化：把 effect / coeffect 提升为运行时机制
理论支柱是类型论中经典的 effect（程序如何改变环境）与 coeffect（程序需要环境什么）：
- effect system：
Γ ⊢ t : T_effect——结果类型带上效应代数标注（Lucassen-Gifford → Moggi 单子 → Plotkin-Power 代数效应/处理器） - coeffect system：
Γ_coeffect ⊢ t : T——上下文带上余效应代数标注（comonad、graded coeffects）
关键洞察：经典系统都是静态工具（词法固定作用域、编译期解析），而动态组合要求这些保证对运行时到达/离开的组件、对持续演化的上下文成立。本文的转向：不加更多类型标注，而是把 effect/coeffect 的概念结构 reify 成运行时可直接操作的一等实体。
2.1 Revertible Effects（时间）
把不纯函数纯化：f : X ⇝ Y 变成 f : Γ × X → Γ × Y，所有副作用都是对上下文 Γ 的变换。可撤销的效应建模为 Γ → Γ × (Γ → Γ)：返回新上下文外加一个显式逆变换。逆变换交回运行时，就是”可追踪”。
核心构造：
- 扭合成幺半群 𝔗Γ：变换对
(f, g)的乘法(f₁,g₁) ∘ (f₂,g₂) = (f₁∘f₂, g₂∘g₁)——逆变换按相反顺序累积（LIFO 回卷的代数本质）。撤销是单边的：只要求g ∘ f，不要求f ∘ g - effect context
∂Γ = Γ × (Γ → Γ)：状态 + 累加器（到目前为止所有已执行效应的逆的复合，即可把上下文恢复到初始态的函数）；迭代 ∂ 得到塔 Γ, ∂Γ, ∂²Γ, …（对应层级化组合） - track / recover：
track(f,g)(γ,φ) = (f(γ), φ∘g)把一次效应记入账本；recover施加累加器恢复上下文。有定理保证 recover ∘ track = id（观测等价意义下） - effect 迭代器：激活过程是多步序列，每步 yield（新上下文、逆变换、续体）；续体依赖前步结果。实现里对应回调的四种形态：普通函数 / 返回 disposer / 生成器 / 异步生成器
2.2 Reactive Coeffects（空间）
依赖表形式化为依赖部分函数 Σ = (k : K) ⇀ 𝒱ₖ（每个 key 带自己的值类型——比 IoC 容器的 key-value map 多了类型安全）：
get(k)/set(k, v)：set 返回新表 + 逆（删除该绑定）——set 本身就是 effect function，因此直接复用 2.1 的全部追踪/恢复机器。“coeffect 操作是 effect，effect 是可逆的”——两个维度的协同点- 满足谓词
σ ⊧ d ≔ ∀k ∈ d. k ∈ dom(σ)，可判定 - 通知分类
notify_d(σ, σ′)∈ {activating, deactivating, neutral}：按组件的依赖规格对每次上下文变化三分类，驱动激活/去激活。这是响应式的代数基础 - 隔离（isolation）：Σiso 双层映射
k → ρ(k) realm → σ(ρ(k))值，同一逻辑依赖在不同上下文绑定不同值（多租户/测试/沙箱），本质是运行时 ad-hoc 多态 - 拦截（interception）：Σinter 给依赖访问挂横切元数据 ℳₖ（每 key 一个幺半群），组件声明的元数据与上下文携带的元数据合并（右偏向，上下文优先）——外层上下文可以不改组件代码就约束它如何使用某个依赖（权限控制的基础）
2.3 Context Paradigm（统一）
- 统一上下文类型
Γ∞ = μΓ. Γ × (Γ → Γ) × Σ：递归结构 + 依赖表，自相似地统一了 ∂ 塔。任何需要跨组件共享的状态都可编码为依赖——Σ 囊括全部共享可变状态。组件与环境的一切交互都经过这唯一实体 - 每个 key 携带 (𝒱ₖ, 𝒜ₖ)：值类型 + 允许的操作集，操作本身是 𝒱ₖ 上的 effect function；上下文中介迭代器 ℑ 限制组件只能做”在声明的 key 上执行操作”或”在 provision 的 key 上安装绑定”两种 stage——形式化了”一切经过 context 中介”的纪律
- 观测等价 ≃：物理状态不可能原样恢复（free 不会恢复堆布局、生成式名字不会复原），所以所有相等都在”任何操作序列都无法区分”的观测等价下读。≃ₖ 由 key 自己的操作生成，是最粗的相容等价
- effect 独立性 + coeffect 交换性：不同 key 上的效应天然交换；同 key 上的操作要求组件提供”成对独立”的见证（witness）——由 key 的表示选择来履行
3. 动态组合演算与五条元定理
把系统分解为 component = (d, p, e) 三元组：依赖规格（读什么）、provision（可能提供什么）、带见证的 effect 迭代器（做什么）。组件的实例化叫 fiber，携带生命周期状态：
∅ ⇄ Inactive ⇄ Loading ⇄ Active ⇄ Unloading
（+ 退休标志 τ；O-Remove 移除空条目）
9 条规则：3 条编排规则（O-Insert / O-Retire / O-Remove，外部唯一输入，编排者只请求存在/不存在，从不直接设生命周期状态）+ 6 条生命周期规则（L-Begin / L-Iter / L-Finish / L-Divert / L-Leave / L-Unload，前提成立时系统自发执行）。驱动机制是 target view（应该按哪个依赖解析运行）与 committed view（实际按哪个解析激活的）的比较——两者一致则静默，不一致则触发转换。卸载守卫（L-Unload 的 ¬relied 前提）保证提供方只在所有依赖方都卸载后才撤绑定。
五条元定理（论文最有价值的部分）：
| 定理 | 内容 | 工程含义 |
|---|---|---|
| Preservation | 任何 load/unload/reload 步骤保持注册表良构 | 系统始终满足自身规则 |
| Recovery exactness（时间全局） | 运行累加器后，系统状态 ≃ “该组件从未运行过、其余步骤照常” 的状态 | 撤销是精确的，即使其他组件期间交错运行 |
| Ordering + Resolution coherence（空间全局） | 组件只在依赖全部就绪时激活；提供方在依赖方全部退出后才撤绑定；转换期间读到的依赖解析不会在脚下移动 | 不会半运行、不会抽走正在使用的依赖 |
| Progress | 依赖图无环时，系统不死锁且必然终止于静默态 | 变更不会卡在半途 |
| Confluence | 无论中间经历多少次加载/卸载/替换/回滚，只要最终期望配置相同，静默态 ≃ 从零按依赖顺序一次性装配的态 | 热改 50 次的系统 ≠ 状态脏，行为等价于干净安装 |
Confluence 是王冠：它让编排者可以像推理静态装配一样推理被反复热改的系统。
四个扩展（实现均已落地且不破坏元理论）：
- 异步/惯性（inertia）：异步宿主中迭代/逆返回 future，一旦进入转换就跑完（L-Divert 只取 landing 分支），步边界仍可中断
- 失败：迭代可抛错，走 aborting L-Divert 路由——回卷已装效应、回到 Inactive 且什么都没装（Cor 69），错误记录在 fiber 上阻止盲目重试；失败不外溢，兄弟组件照跑。实现的 FAILED 态即此
- 隔离：多 realm 读法 = 把 key 集扩成 K × R，规则原样适用
- 配置修订：禁用 = O-Retire；其他修订 = 退休→去激活→移除→同名重插。依赖方无需人工干预自动跟随
4. 实现：Cordis 逐符号对应
论文第 5 节给出理论↔实现对照（Table 2 摘录）：
| 理论 | Cordis 实现 |
|---|---|
| Γ∞ | ctx（一等上下文） |
| effectΓ | ctx.effect(callback)——一切上下文变更的唯一原语，LIFO 复合逆 |
| Σ / Σiso / Σinter | ctx[@@store] / ctx[@@isolate] / ctx[@@intercept] 三个 symbol 槽 |
| set / get | ctx.set(key, value) / ctx.get(key)；set 就是带 notify 的 ctx.effect |
| fiber ⟨d,p,e,π,σ,τ,θ⟩ | fiber：fiber.inject（d）、fiber.apply（绑定配置后的 e）、fiber.state、fiber.committed（ω）、fiber.target、fiber.inertia |
| O-Insert/O-Retire | ctx.use(component, config) 及其回调的逆——实例化本身是父纤维的普通 effect，卸载父自动级联卸载子 |
| L-规则 | refresh/reload/unload 互递归状态机（Algorithm 5）：refresh 重算 target，变了且无在途转换就发起 reload/unload；reload 完成时 target 仍匹配则 ACTIVE 并 notify，否则链式转 unload（惯性） |
| L-Unload 守卫 | unload 第一行：await all(notify(...).map(f => f.await()))——先等所有依赖方排空，再跑自己的逆 |
运行时不校验见证：回调提供的逆是否真的能撤销、同 key 操作是否真的交换，是组件作者的义务而非运行时检查——这是形式模型与实现之间诚实标注的缝隙。
三层架构：核心库（effect 追踪 + coeffect 解析）→ 组件加载器（声明式配置协调 + HMR）→ 应用框架（Koishi / DeepSeek Harness）。
- 声明式配置：条目 = {id, url, isolate, intercept, config, disabled}，恰是 support set（τ, π, d, p）的忠实规格。协调按字段分派最小扰动操作：id/url 变 → 重建；intercept → 原地更新（读时生效）；config → 交给组件自己 diff；disabled → 卸载/重载。元理论保证协调只需发出请求、不必排序加载顺序（依赖只约束何时激活，不约束何时取模块，所以可并发加载）
- HMR 三阶段：模块分类（accepted/declined 不动点，环上模块默认 declined）→ 陈旧条目探测（依赖树与 accepted 相交）→ 事务性重载（备份缓存，任何模块导入失败则全量回滚，绝不出现半重载态）。因为 fiber 已界定组件全部效应，HMR 不需要 webpack/Vite 那种开发者标注的接受边界
5. 案例研究与有效性边界
Koishi：4 年 4000+ 社区插件，服务端与 Web 控制台两个独立 Cordis 应用（证明表达力与运行时无关性）。三个实证点：控制台禁用插件即原地回卷效应（无需重启）；HMR 保存即热替换且保住其他插件的连接/缓存；依赖不可用的插件安静停留 Inactive 而非报错，跨独立作者的依赖拓扑在运行时保持自洽。
论文明确的 threats to validity：单一生态、单一宿主语言、观察性而非对照实验——是存在性与采纳性结论，不是量化结论。
6. 讨论要点（工程价值密度最高的部分）
- 系统边界：逆的语义由边界划定。边界内 = 系统能独占修改并恢复 → 可追踪可逆；边界外 = 操作视作 id，不追踪。获取（acquisition）在内、发射（emission）在外：open/malloc/fork 装的记录可逆，write/send 推出去的数据不可逆。跨越边界的恢复只有两条路：withhold（延迟发射直到状态确定持久，即 rollback-recovery 的输出提交问题）或 compensation（应用自定义的更粗等价下的补偿动作，如删文件、退款，同样 LIFO 复合）
- 服务多路复用：exclusive binding（换实现要扰动全部消费方）vs service broker（broker 本身是注入点，后端提供方更换不触发消费方重载）——由此派生负载均衡、应用层滚动更新（provider transition 取代蓝绿部署）、跨进程调用（需按异步契约设计接口）
- 访问控制：inject 声明 = 能力请求，context proxy = 能力中介——结构上就是 capability-based security；interception 元数据可做细粒度策略（如只读数据库授权），运行时可调且不触发重载。沙箱仍需外部机制（SFI/独立运行时/容器），桥接后对组件透明
- 循环依赖：不产生死锁，而是相关组件永久 Inactive——可从声明静态预测并报错。任何双向交互都可拆成单向绑定（server-core + access-control-core + 两个集成组件），代价是集成组件数可能随 n 二次增长，靠打包/约定布线/脚手架缓解
- 依赖类型与版本：key 身份是纯名义链接，独立开发场景下有 interface drift 与 key collision 两病。三条路：key 命名空间化（K × P）、peer dependencies（Cordis 现状，依赖语义化版本约定）、结构兼容性（理想但行为契约层面不可判定）
- 语言/OS 协同设计：隐式上下文（免传参 + 防止误持他人 ctx）、编译器可见的效应迭代器（单个状态机替代每步闭包分配）、类型系统接纳依赖规格（编译期报环、行类型做结构兼容）；OS 侧把资源作为 coeffect 发放并归属记账，事务性持久写/CoW 存储可让部分 emission 也可回滚
7. 相关工作定位
| 对照系 | 区别 |
|---|---|
| ZIO / Effect-TS | 需要单子嵌入（代码必须写在效应类型里）；需求被”解释”而非反应式重解析，服务撤走其操作后果仍留在原地 |
| Effekt（代数效应即能力） | 静态类型级、能力是二等的受词法作用域约束；Cordis 是运行时纪律、目标移除时完全恢复 |
| Heunen 等可逆效应语义（dagger arrows） | 最接近的形式化对照：都是”效应配对逆”。但那是全局可逆、双侧逆、从范畴结构导出；Cordis 只要每个原子效应带单边逆、调用点提供、复合推出整体 |
| Granule / graded types | 统一 effect+coeffect 但全在类型层；本文与之正交：同一对概念提升到运行时 |
| COP / AOP | COP 的”context”是环境情境、层不追踪效应；Cordis 的激活由依赖满足驱动且去激活完全回卷。AOP pointcut 是 oblivious 的；Cordis 横切面被限制在组件声明的 coeffect 上，可审计可治理 |
| DSU（Kitsune/Erlang OTP/webpack HMR） | 状态前向迁移更优雅但需手写迁移函数；Cordis 零迁移函数、支持彻底卸载。组件内存态不跨重载存活（除非放进更长寿命的依赖）——叠加前向迁移是 future work |
| OSGi | 服务模型呼应，但清理靠开发者回调 |
8. 评价
为什么重要（对 agent 工程师）：这是第一份给”自进化 agent 的插件运行时”写形式语义的工作。自进化场景是这套理论最尖锐的应用——组件替换频率高、无人监督、坏修改必须能被完全撤销且依赖方自动跟随，正是 temporal+spatial 保证的直接翻译。DeepSeek Harness “一切皆插件、无特权核心”的架构主张，由这 5 条定理背书：热改收敛到干净安装态（Confluence）、不卡死（Progress）、卸载零残留（Recovery exactness）。
局限要清醒：
- 见证（逆真的可逆、操作真的交换）不被运行时校验，全靠组件作者纪律——形式保证是条件性的
- emission 不可回滚是原理性边界：发出去的消息、写出去的外部状态只能 withhold/compensate，agent 的工具调用副作用大多在这条边界外
- 验证只有 Koishi 单一生态的观察性证据；且 Koishi 还在 Cordis v3，论文写的是 v4
- 论文形式化了组合脚手架，不保证组件本身的正确性——插件内部逻辑错了，系统照样”正确地”装载它
与本知识库的连接：工程侧的五概念（插件/上下文/inject/事件/effect）、fiber 状态机、HMR 实操，见 cordis 与 README 系列教程；本文是其理论层的补全。对照 agent-harness-anatomy 的 harness 组件观，以及 2605.18747_code-as-agent-harness 的 harness 综述——本篇提供了”agent 如何安全地修改自己”这一子问题的最严格现有答案。
资源
- 论文：https://arxiv.org/abs/2608.25512（本地存档
~/6ai/opensources/cordis-paper/paper.pdf） - 实现：https://github.com/cordiverse/cordis（clone 存档
~/6ai/opensources/cordis） - 官方入门文档：https://deepseek-harness.github.io/deepseek-harness/reference/cordis-primer
- DeepSeek Harness：https://github.com/deepseek-ai/deepseek-harness