论文链接：A Programming Paradigm for Spatiotemporal Composability（GitHub PDF） 代码仓库：cordiverse（GitHub 组织，含 Cordis 框架） 发表时间：2026 年（88 页技术报告，未标注会议） 机构：北京大学、DeepSeek-AI 合作。第一作者 Yifan Shi 同时隶属北大与 DeepSeek-AI（学生 + 企业合作模式），Wei Zhang 属北大，Tianyi Cui 属 DeepSeek-AI。值得注意的是，Cordis 的前身已驱动开源聊天机器人框架 Koishi 四年，本文是该工程实践的理论升华 领域标签：编程语言 / 软件工程 / 形式化方法（效应系统、操作语义、组件模型）
一、论文背景
1.1 什么是「动态组合」？
组合（composition）——把复杂系统从简单零件拼装出来——是软件工程最古老的原则（1972 年 Parnas 的经典论文就在讲怎么分模块）。传统组合是静态的：函数调用、模块导入、类继承在编译期就定死，程序跑起来之后不再变化。
但现代软件越来越需要动态组合：组件在运行时被加载、卸载、重新配置。两个典型场景：
- 插件系统：VSCode、浏览器扩展、IDE 插件、聊天机器人框架——功能以插件形式随时装卸；
- 自进化 Agent Harness：大模型 Agent 的运行时底座（harness）需要在持续服务的同时，加载新工具、替换自身组件、修改工作流——每一次自我修改都是一次动态组合。
1.2 动态组合为什么难：两个正交维度
论文的关键洞察是：动态组合的难点可以精确地拆成两个互相独立的维度——
| 维度 | 名称 | 含义 | 静态世界的对应物 |
|---|---|---|---|
| 时间维 | 时间可组合性（temporal composability） | 组件被移除时，它对共享环境做过的一切修改（分配的资源、注册的事件、改动的状态）必须被完整、安全地撤销 | 词法作用域（RAII、bracket 模式） |
| 空间维 | 空间可组合性（spatial composability） | 组件之间必须能结构化、可验证地声明、发现、解析彼此的依赖，并在依赖变化时响应 | 模块导入解析 |
静态世界里这两件事都容易：出了作用域自动析构，导入在编译期解析。可一旦组件在运行时来了又走，两个维度同时爆炸——
时间维爆炸的实例（论文给出的硬数据）：VSCode 把所有扩展跑在一个共享的 extension host 进程里，没有任何机制能在运行时卸载单个扩展的代码。作者统计了 2026 年 6 月 9 日 VSCode 插件市场下载量前 100 的扩展：87 个含可执行代码，卸载它们全都要重启整个 host。VSCode 提供的 deactivate 钩子只是进程关闭时的优雅停机回调，而且它把"清理"和"创建"拆在两个函数里（activate 里创建、deactivate 里清理），破坏了关注点局部性，没人能验证清理是否完整。
空间维爆炸的实例（同一组数据）：VSCode 有 extensionDependencies 字段可以声明扩展间依赖，但前 100 名扩展里只有 7 个用了它。原因在于 VSCode 的 API 形状：扩展通过宿主提供的固定扩展点（命令、视图、语言特性）贡献功能，而不是互相依赖；跨扩展取值的 getExtension(...).exports 返回 any 类型，没有结构化契约。
1.3 业界的「粗糙绕路」及其代价
为什么学界长期没认真研究这个问题？因为操作系统和容器编排器提供了一个粗糙的替代品：操作系统以「进程」为粒度提供时间可组合性（杀进程即回收一切），Kubernetes 这类编排器以「服务」为粒度提供空间可组合性（管理服务依赖）。
代价是：
- 时间维：每次重启丢掉进程内全部累积状态（缓存、连接、半成品计算），重建要几秒到几分钟；为了维持可用性还得配冗余副本；
- 空间维：容器级编排无法表达共享地址空间内组件间的依赖，本来可以是本地函数调用的交互被迫走网络。
粒度错配（granularity mismatch）是根本矛盾：现代系统在进程/容器边界之内组合得越来越细，而回收与依赖管理工具只在边界之上工作。自进化 Agent Harness 让矛盾尖锐化——每次自我修改都重启的话，累积不可用时间不可接受，飞行中的任务反复被打断；更糟的是，一次错误的自修改可能弄坏恢复所依赖的那个进程本身。
二、论文定位和关联工作
这篇论文站在两条理论传统与四条系统传统的交汇点上。理解它的定位，需要知道每个传统离它「差一步」在哪里。
2.1 理论支柱一：效应系统（Effect Systems）
- 单子效应（Moggi 1991，Wadler 推广）：用单子
T(A)把带副作用的计算封装成值，Maybe/State/IO都是实例。工业界的 ZIO、Effect-TS、fp-ts 都属此系——但程序必须整体写进效应类型里才被跟踪，且服务撤走后它做过的事原地留存，不会回滚。 - 代数效应与处理器（Plotkin & Power、Plotkin & Pretnar）：效应接口与实现解耦，Koka、Eff、OCaml 5 采用了。Effekt 语言（Brachthäuser 等）最接近本文——它把效应类型重释为「能力」（capability），效应类型表达的是计算需要上下文提供什么。但 Effekt 是编译期、词法作用域的纪律：能力被限死在词法范围内；Cordis 则在运行时纪律化效应，目标是组件移除时的完整资源回收。
- 可逆效应（Heunen 等的 dagger arrows / inverse arrows，2018）：形式上最接近本文「可逆效应」的工作——每个效应配一个撤销手段。区别在于：Heunen 在范畴语义层要求整个计算可逆、双逆、由结构导出；Cordis 只要求每个原子效应带一个单侧逆，由调用点现场提供，组合的逆由复合自动导出——要求低得多，因此能落地到真实运行时。
2.2 理论支柱二：协同效应系统（Coeffect Systems）
- Petricek、Orchard、Mycraft 2013/2014 提出 coeffects：与效应对偶——效应标注「计算对环境做什么」，协同效应标注「计算需要环境什么」（
Γ_{coeffect} ⊢ t : T，注解挂在上下文而非类型上）。用例包括数据流语言的缓存需求、隐式参数、平台资源依赖。 - Orchard 等的 Granule（分级模态类型）统一了分级效应与分级协同效应，证明单一类型系统能同时跟踪「做什么」和「要什么」。
- 关键共性：以上全部是编译期、词法固定作用域上的静态注解。而动态组合要求保证在「组件运行时来去、上下文持续演化」下依然成立——没有固定词法作用域能框住部署后才加载的插件，没有编译期上下文能预见运行时配置产生的依赖。这就是本文的立足点：不是给静态类型系统加更多注解，而是把效应/协同效应的概念结构「具体化」（reify）为运行时可直接操作的一等实体。
2.3 系统传统一：开发者手写恢复（四大流派中的三个）
论文第 7 章把「时间可组合性」的已有方案分成四族，定位极其清晰：
| 流派 | 代表 | 恢复方式 | 根本局限 |
|---|---|---|---|
| 状态前向迁移 | DSU（Hicks、Kitsune）、Erlang/OTP、webpack/Vite HMR | 手写迁移函数把旧状态搬到新版本 | 迁移函数必须手写；不支持彻底卸载组件回收资源 |
| 开发者手写清理 | OSGi、Eclipse、VSCode 生命周期、Command 模式、Saga、事件溯源、React useEffect | 卸载回调/补偿动作 | 逆是未被强制的义务，忘了就静默泄漏。React useEffect 最接近结构化配对，但 hook 只能在顶层调用、不接受 async/迭代器——效应不能由其它效应组装、不能与控制流交织，复合的逆无从导出 |
| 静态作用域反转 | STM、可逆计算（Janus）、可逆进程演算（RCCS）、线性类型/RAII/Rust 所有权 | 由构造自动反转，但作用域预先固定 | 反转的 reach 由语义定死，不能覆盖组件整个生命周期的任意上下文操作 |
| 界面拦截式回收 | Nooks、shadow drivers、Akeso（内核扩展恢复） | 运行时在受控接口上记录获取，据此回收 | 平台固定了能记录什么；组件只能持有平台已知的资源。本文称其为「系统层面最接近的先例」，但 Cordis 组件可自带新效应并为每个原子效应配逆，且回收跨越组件整个生命周期并传播给依赖者 |
2.4 系统传统二：空间可组合性
- 初始化时接线：Spring/Guice/Angular 的依赖注入、Vue
provide/inject、React Context——初始化时注入，不响应式重解析：提供者运行时被替换/移除，既有依赖者既不失效也不重初始化。 - 可用性响应式组件模型：OSGi Declarative Services 与 iPOJO——最直接的先例，服务出现/消失时自动激活/钝化组件，iPOJO 的 Gravity 项目明确面向运行时自适应，其 provide/require 模型直接预示了 Cordis 的模式。局限：钝化靠手写回调（同前述泄漏问题）且回调是同步的——若拆解需要与正在离开的依赖做异步交互，框架无协议可等，只能对着可能已失效的引用阻塞。
- 值级响应式：FRP、signals（SolidJS/Vue/Angular）——值粒度传播变更，无组件级异步生命周期语义；反之 FRP 的 glitch freedom 一致性也是 Cordis 没有的（两者互补）。
2.5 定位总结
| 之前各路线 | 本论文 | |
|---|---|---|
| 保证来源 | 开发者纪律 / 平台预知 / 静态作用域 | 结构保证：逆的复合自动导出 |
| 生效时机 | 编译期或初始化期 | 运行时，组件来去时持续成立 |
| 时间维 + 空间维 | 各自为战 | 统一在一个上下文类型里 |
| 形式化程度 | 各流派有局部理论 | 完整操作语义 + 五组元定理 |
| 验证 | 各自场景 | 88 页理论 + TypeScript 实现 + 4000 插件生态四年运行 |
一句话定位：这是第一篇把「插件装卸 / Harness 自我修改」这件事从工程技巧提升为带全套元理论的编程范式的工作——它不是某个更好用的依赖注入库，而是给「动态组合」补上了相当于静态组合世界里「词法作用域 + 模块系统」级别的形式基础。
三、问题定义
3.1 从具体场景到抽象问题
剥掉「插件」「Agent Harness」这些具体外壳，所有动态组合系统共享同一个抽象结构：
一个共享环境（context）随时间演化；一组组件（component）在任意时刻到来或离开；每个组件到来时对环境做一串修改、并声明它需要环境中已有的某些东西；要求：
- （时间） 任一组件离开后，环境等价于「它从未来过」——无论其间多少其它组件的修改与其交织；
- （空间） 依赖关系的建立与解除完全由声明驱动、自动协调——提供者就位则依赖者激活，提供者撤走则依赖者先行有序退场，全程无需任何组件手工检测。
3.2 论文找到的深层结构：效应与协同效应的对偶
本文最漂亮的抽象跳跃是发现：上面两个要求恰好对应程序语言理论中一对现成的对偶概念——
| 动态组合的要求 | 程序语言理论概念 | 方向 |
|---|---|---|
| 组件对环境的修改要可撤销 | 效应（effect）：计算如何修改环境 | 向外 |
| 组件对环境的需求要被声明和响应 | 协同效应（coeffect）：环境如何约束计算 | 向内 |
形式化的问题定义：给定上下文类型 Γ，定义
- 可逆效应函数：𝔈*Γ = Γ → Γ × (Γ→Γ)，且带见证条件——作用在 γ 上返回 (δ, g) 时必须 g(δ) = γ。即：每个效应在它发生的那个状态上返回自己的逆；
- 协同效应规范：𝔇 = Set(K)，即键集合上的依赖声明；满足谓词 σ ⊧ d ⟺ ∀k∈d. k∈dom(σ)；
- 求：一套运行时机制与演算，使上述时间/空间两个保证对任意交错运行的组件全体成立（而不只对单个组件孤立成立）。
3.3 这个抽象的精妙之处
- 逆只要求单侧、只要求在应用点上成立（g(δ)=γ，而非 g∘f=id 全局成立）——这让「撤销」的门槛低到工程上处处可满足（删除注册项、归还句柄都做得到），而全局可逆（Heunen 路线）在实践中办不到；
- 两种保证统一在同一数学对象上：后面会看到，协同效应的 set 操作本身就是可逆效应（𝔈*Σ 的元素）——「提供依赖」这个空间动作本身就是「修改上下文」这个时间动作，两个维度在类型层面就融合了；
- 抽象指出了不可逾越的边界：恢复保证只能对「可被上下文编码的位置」成立（系统边界，§6.1），发出的网络包没法收回——论文不假装能撤销一切，而是精确刻画能撤销什么。
四、问题解法
论文的解法分四层：可逆效应（时间）、响应式协同效应（空间）、统一上下文（融合）、动态组合演算（全局化）。最后由 Cordis 实现。
4.1 可逆效应：让每个副作用自带「撤销票」
类比：进游乐园（应用效应）时领一张手环（逆函数），出园（卸载组件）时凭手环核销。运行时不理解每个项目玩了什么，只需要收手环。
核心构造（全部配了定理与证明）：
- 效应上下文 𝜕Γ = Γ × (Γ→Γ)：一个二元组 (γ, φ)——γ 是当前环境状态，φ 是累积器：迄今所有效应之逆的复合。初始态为 (γ₀, id)。
- 扭曲复合：(f₁,g₁)∘(f₂,g₂) ≔ (f₁∘f₂, g₂∘g₁)——前进方向按序复合，逆按相反顺序累积（后做的先撤）。这让 (Γ→Γ)×(Γ→Γ) 构成一个幺半群 𝔗Γ。
- track 与 recover：
track(f,g)(γ,φ) = (f(γ), φ∘g)——执行效应、把逆挂上累积器；recover(γ,φ) = (φ(γ), id)——一口气撤销到初始态。- 定理 7（可靠性不变量）：只要每个 g 在其作用点上真的是逆，则 recover∘track = recover——「随时撤、都能回到原点」是代数性质而非运气。
- 效应函数 𝔈Γ = Γ → Γ→(Γ×(Γ→Γ))：升级版——逆由调用点现场提供（因为实践中逆往往依赖当时状态，比如"删除我这次注册的那个 ID"而非"删除某个固定 ID"），且复合操作 ⋄ 自动保持可逆性（定理 10/11）。
- 独立性（Definition 19，最关键的理论步）：两个效应独立 = 它们的一切变换互相对易 + 一方不扰动另一方产生的逆。在独立性下，推论 21：n 个效应可以按任意置换顺序撤销并回到原点。这解决的是多组件交错场景：A 的逆不需要等 B 先撤——撤销顺序不再被锁定为 LIFO。
- 观测等价（Definition 33-39）：物理上不可能逐比特恢复状态（free 之后堆布局回不去了）。于是把「相等」放宽为「观测等价」≃：两个状态在所有协同效应操作能观测的范围内不可区分。堆布局这类无人观测的部分被故意遗忘。论文证明：如果每个键的操作满足交换性（commutative key），则基于这些操作的效应自动独立（定理 40/42）——路由注册、事件监听这类"往表里加条目"的操作天然满足。
4.2 响应式协同效应：依赖的声明—通知—隔离—拦截
类比：传统 IoC 容器像前台寄存处（键值存取）；响应式协同效应像带合同审查的供应商管理系统。
四层机制：
协同效应上下文 Σ = (k:K) ⇀ 𝒱ₖ：类型化依赖表——每个键 k 绑定特定类型 𝒱ₖ 的值，静态类型安全。核心操作
get(k)（读）与set(k,v)（写 + 返回"删除该绑定"的逆）。注意 set 本身就是 𝔈*Σ 的元素——提供依赖是可逆效应，效应机器自动接管其追踪与回收。这是两个维度的第一次融合。规范与通知：组件声明规范 d ⊆ K。任何状态迁移 σ→σ′ 对照 d 分类：
- activating（从不满足→满足）→ 触发组件激活（执行其效应）；
- deactivating（从满足→不满足）→ 触发钝化（应用累积器恢复）；
- neutral → 什么都不做。
由于一切 σ 的变更都经过效应函数（其逆恢复旧域），每次变更都可在效应边界被观测——响应性是效应系统的代数副产品。
隔离（isolation）：Σiso 引入域（realm）表 ρ: K⇀R 两层解析 k→ρ(k)→σ(ρ(k))——同一个键在不同上下文可解析到完全不同的绑定。论文称其为「运行时 ad-hoc 多态」：多租户、测试环境、组件沙箱的直接基础。
拦截（interception）：每个键挂一个单元半群元数据 (ℳₖ, ⊕ₖ, εₖ)，组件声明元数据、上下文携带元数据、两者合并（右偏向，外层可覆盖内层）后交给提供者函数。用途：不改组件代码就能约束它怎么用某个依赖（比如把社区插件的数据库依赖降级为只读）。
4.3 统一上下文：一个递归类型即一个编程范式
定义 32：Γ∞ ≔ μΓ. Γ × (Γ→Γ) × Σ——递归的「当前状态 × 累积器 × 协同效应表」。效应映射 𝔈 把 Γ∞ 映到自身，整个「∂ 塔」折叠为单一自相似类型。
论文把它定位为与「显式状态穿线（函数式）」和「隐式可变（命令式）」并列的第三种范式——上下文范式：效应与协同效应都经一个显式上下文参数中介，兼得函数式的可追踪与命令式的人机工学——开发者为每个原子操作提供逆，任何复合操作的逆由复合自动导出；组件只声明需要的依赖，运行时在提供者增删换时自动重接线。「本来依赖开发者纪律的正确性，变成了范式的结构性质。」
4.4 动态组合演算：从单组件保证到全系统保证
第三节的机制只给出「局部」保证。要证明全系统（多个组件交错）下依然成立，论文构造了一个操作语义演算：
对象：
- 组件 ℭ = (d, p, e)：依赖声明 d + 供给声明 p（声明它可能提供哪些键；不同组件的供给必须两两不相交——单源原则）+ 见证效应函数 e；
- 纤（fiber）：组件的一次实例化，携带生命周期状态 θ（Inactive / Reloading / Active / Unloading）、自己的累积器 g、已提交视图 ω（激活时依赖的提供者名单）；
- 注册表：纤按名字索引，父指针成树；全局协同效应表 = 所有 Active 纤的表之并。
规则（共 10 条）：编排规则 O-Insert / O-Retire / O-Remove（外部请求插入/退休/移除），生命周期规则 L-Begin / L-Iter / L-Finish（激活：迭代执行效应，累积逆）、L-Divert（目标视图变了→中途中止并回滚已做的）、L-Raise（迭代抛错→走卸载路径恢复）、L-Leave / L-Unload（钝化：先停止供给、等所有依赖者退场、再应用累积器）。
三个特别精彩的设计：
- L-Unload 的守卫：
¬reliedₙ(γ)——还有别的纤的已提交视图指向你，你就不许真正撤走。它不会死锁的原因很妙：L-Leave 先把纤标记为 Unloading，它的表立即退出全局并集 σγ，于是所有依赖者的目标视图立即失效、各自走上卸载路——依赖图的消退是按需级联的，不需要预先全局分析。 - 效应迭代器：激活建模为可分步执行的迭代器（每次迭代产出：新状态、逆、续体）——本质是「具体化的限定续体」，直接映射到主流语言的 generator/
yield。这让「在任意两个效应之间可以检查环境是否已变、变了就中止回滚」成为可能（对应 Theorem 64 的分辨率一致性：任何迁移不会横跨两个不同的依赖解析）。 - 惯性与失败：已在飞行中的迭代必须落地（不能中途撤销异步操作）；失败先恢复再记录——任何失败路径都经过 L-Unload，纤带着错误结局回到 Inactive 且不自动重试（其效应函数已被证明在当前环境下不可靠）。
元理论五支柱（第 4.4 节，全带证明）：
| 定理 | 内容 | 直觉 |
|---|---|---|
| 保持性（Thm 59） | 注册表良构性（树、供给两两不交、已提交视图指向存活提供者）在所有规则下不变 | 状态空间不被破坏 |
| 恢复精确性（Thm 61 + 推论 62） | 在成对独立下，任意时刻应用纤的累积器，得到的正是「这个纤从未来过、其它纤照常运行」的状态 | 时间可组合性的全局形式 |
| 次序（Thm 63） | 依赖者只在依赖就绪后激活；提供者只在所有依赖者退场后撤走；且依赖者在自己整个钝化过程中仍能读到那个正在撤走的依赖 | 空间可组合性的全局形式 |
| 活性（Thm 66） | 依赖无环 + 迭代长度有界 ⇒ 无死锁、必终止、系统静息（quiescent） | 守卫最终一定释放 |
| 合流性（Thm 73） | 系统静息态只由最终配置决定，与装载/卸载的中间历史无关——等价于「从头静态装配」 | 动态历史不留痕迹 |
4.5 Cordis 实现：三层架构
| 层 | 内容 | 对应理论 |
|---|---|---|
| 核心库 | ctx.effect(callback)（唯一突变原语，一切经过它即自动被追踪恢复）、ctx.get/set/isolate/intercept、ctx.use（实例化组件）、Proxy 介导的属性访问（沿纤链上行解析，未声明的访问直接报错） | 第 3、4.1-4.3 节 |
| 组件加载器 | 声明式配置树（条目：id/url/isolate/intercept/config/disabled）+ 增量协调（按字段分派最小破坏操作）+ 事务式热更新（HMR：模块分类不动点 → 陈旧条目检测 → 失败则整体回滚缓存，永不停在半重载状态） | 合流性/活性定理直接为协调与并发装载提供正确性依据；HMR 不需要开发者标注边界（对比 webpack/Vite） |
| 应用框架 | Koishi 等领域框架只补领域词汇 | 元框架「不预设场景」的证明 |
实现细节里最见功力的是理论-实现对照表（论文 Table 2）：𝜕Γ→ctx、ω→fiber.committed、L-Leave→refresh 标记 UNLOADING、守卫→unload 等待被通知依赖者……每条理论构造都有精确的运行时对应物。
五、评估指标与实验证据
这是一篇系统+理论论文，没有基准测试式的实验。它的证据结构是「定理 + 实现存在性 + 生产生态观察」，评估要按这三类分别审视其证明力。
5.1 定理体系（主张的主要证据）
- 定理不是装饰：恢复精确性直接就是「卸载组件=它没来过」这一核心主张的数学陈述；合流性直接就是「怎么装都收敛到静态装配结果」的主张。证明覆盖了含异步、失败、部分回滚的完整演算（而非只证明理想化核心），这是证明力的关键——很多形式化工作只证玩具核心，真实语义（异步落地、错误恢复）另行打补丁，元定理就断了；本文的十个规则就是实现所实现的那些规则。
5.2 量化观察：VSCode 生态数据
| 数据 | 数值 | 支撑的主张 |
|---|---|---|
| VSCode 前 100 扩展中含可执行代码者 | 87 个 | 现有插件系统的时间维缺陷不是边缘情况而是常态（卸载即重启） |
| 前 100 中声明 extensionDependencies 者 | 仅 7 个 | 现有插件系统的空间维支持形同虚设 |
数据取自 2026-06-09 的 VSCode Marketplace。这组数据的设计意图是排除「纯声明式扩展（主题/快捷键）可自由移除」这一反例，把问题精确限定在含代码扩展上——证明力扎实。
5.3 案例研究：Koishi
- 规模：基于 Cordis（当前 v3，论文呈现 v4，核心组合模型共享）的开源聊天机器人框架，四年开发、4000+ 社区插件，覆盖 IM 适配器、数据库驱动、管理控制台到终端功能；
- 表达力与通用性证据：Koishi 服务端的每个功能都是上下文原语之上的插件，宿主只贡献聊天机器人领域词汇；其 Web 控制台是第二个独立的 Cordis 应用（浏览器运行时）——同一模型横跨服务端与前端两个迥异环境；
- 时间维证据：从控制台禁用插件 → 效应就地撤销；开发中 HMR 保存即重载，保留缓存与其它连接——没有经验的插件作者不写任何卸载代码也能得到有序清理（对照第一节 VSCode 的 87/100）；
- 空间维证据：适配器提供平台接入、数据库驱动提供存储、功能插件声明并消费——由不同作者独立编写、除协同效应外零协调的代码在开放生态中保持装配一致。
5.4 证据的边界（论文自陈，值得肯定）
作者明确承认（Threats to validity）：证据来自单一生态、单一宿主语言，观测性而非对照实验，因此是「存在性+采用性」结果而非定量结果；抽象的性能开销与开发者生产力对比留作未来工作。判断：定理部分证明力完备；生态部分作为存在性证明成立，作为「优于现有方案」的定量证明不成立——论文对此诚实，没有越界宣称。
六、效果优势的根源解释
本论文的「效果」= 相比于第 2 节四流派 baseline（VSCode 式手写清理、OSGi 式响应式组件、React useEffect 式结构化配对、静态作用域反转）所能给出的保证。按因果链逐条解释为什么是结构上必然更好，而非「用了 X 所以好」。
6.1 时间维：为什么「完整的卸载恢复」从不可能变成结构保证
baseline 的根本局限在信息的局部性：VSCode/OSGi 把创建放在 activate、清理放在 deactivate，两段代码在空间上分离、在时间上隔着整个生命周期——清理代码要正确，必须完整记住创建代码做过的一切，而人脑和代码审查都无法维持这个跨度（87/100 需要重启是制度化的认输）。
本文的因果链：
- 构造差异：效应函数在应用点现场返回逆（𝔈Γ = Γ → Γ×(Γ→Γ)）；
- 机制变化：逆的产生与效应的执行在词法上同址——写效应时逆就在手边，遗忘它的可能性被类型签名消灭；
- 瓶颈消除：复合效应的逆不需要写——由 ⋄ 复合与扭曲幺半群结构自动导出（定理 10/11），复杂度从 O(效应数) 的手写清理降为 O(原子效应数) 的就地配对；
- 全局化：独立性条件（commutative key 自动满足，定理 42）+ 恢复精确性（定理 61）⇒ 多组件交错下撤销任意置换成立。
反事实验证：去掉「逆在应用点返回」这一条设计（退回 (f,g) 对预先给定），track 就要求一个 g 服务所有状态——而实践中逆几乎总依赖状态（删除"我注册的那个"ID）——这正是 baseline 清理代码难写的本质。论文在 3.1.2 节明确论证了这个升级的必要性。
6.2 空间维：为什么依赖协调从「各自检测」变成「结构驱动」
baseline 的根本局限：DI 框架的接线是一次性的（初始化后不重解析）；OSGi 响应了服务可用性，但钝化是手写同步回调——异步拆解（连接池要先把连接还给提供者）无协议可等。
本文的因果链：
- 构造差异：依赖满足谓词 σ ⊧ d 是可判定的（dom 有限），且一切 σ 变更都经过效应函数——变更在效应边界必然可观测；
- 机制变化：观测即可分类、分类即驱动状态迁移——响应性不是外加的观察者模式，而是效应系统的代数副产品；
- 关键新增——Unloading 中间态 + 守卫：提供者先停供给（表退出全局并集）再等依赖者退场（¬relied），使依赖者在整个自身拆解期间仍能读到正被撤走的依赖（定理 63(3) 的内容，闭连接池场景的直接答案）；而守卫不死锁（定理 66）的根源是「停止供给」这个动作自动让所有依赖者的目标视图失效——级联退场由数据流自己驱动，无需全局调度；
- 异步拆解成为可能：惯性状态机（reload/unload 链式互递归）允许过渡中等待，OSGi 的同步回调瓶颈被机制性消除。
6.3 范式层：合流性为什么重要
合流性（定理 73）不是锦上添花：它意味着装载历史不影响终态——开发者调试时反复装卸插件、HMR 反复热替换、Agent 反复自我修改，都不用担心系统悄悄漂移。这把「重启解决一切问题」的粗糙但可靠的直觉，替换为「任何装卸序列都等价于干净启动」的精确且同样可靠的保证。对于自进化 Harness 这种修改频率极高、又无人监督的场景，这是能信任自修改结果的前提条件。
6.4 不回避的边界
论文明确说出保证的不覆盖范围（§6.1）：越过系统边界的发射（emission，如已发出的网络包、已扣的款）不可逆，只能扣留或补偿；依赖循环只是静默不激活（可从声明静态检测）；非 commutative 的键（有序中间件链）不满足独立性、必须走 LIFO 累积器或协同效应排序——这些诚实的边界本身就是论文可信度的一部分。
七、必要知识反推
假设让一个聪明但零背景的人重做这项工作，他至少需要哪些知识？
7.1 领域知识层（研究对象如何运作）
- 插件系统与扩展宿主的实际架构：必须知道 extension host 的进程模型、activate/deactivate 生命周期——否则提不出「87/100 需要重启」这样精准的动机数据；
- 依赖注入与 IoC 的演化史：从 Spring 到 OSGi Declarative Services 到 signals，知道每一代解决了什么、卡在哪——否则找不到「初始化时接线 vs 响应式重解析」这个精确的分界；
- Agent Harness 的工程现实：工具组合、沙箱、状态持久、子 Agent 编排——论文把它列为第一驱动场景（自进化），不知道这些系统的运行时修改频率与无人监督特性，就无法论证粒度错配的严重性。
7.2 方法论知识层（理论工具）
- 效应系统谱系：Lucassen-Gifford 效应注解 → Moggi 单子 → Plotkin-Power 代数效应 → handler——尤其是对偶侧的 coeffect 文献，「效应描述修改、协同效应描述依赖」这个对偶是全文的骨架，不知道它就只能在工程层面打转；
- 范畴论基础：幺半群、同态、群作用——「扭曲复合构成幺半群」「track 是幺半群同态」这类表述让所有构造性定理可以紧凑陈述与证明；
- 操作语义与进程演算技艺：标注迁移系统、良构性不变量、活性和合流性证明（局部交换引理、删除引理、换位引理的标准组合拳）——定理 59/61/63/66/73 的证明密度在近年系统论文里罕见；
- 可逆计算与迹理论：RCCS 的因果一致性、Mazurkiewicz 迹等价——独立性-交换-合流的技术路线直接承自这里；
- 观测等价与商类型：CompCert 内存状态比较、Pitts-Stark 动态名字生成——「把相等放宽到可观测范围」是让恢复保证从不可能变为可能的关键一跳。
7.3 工程知识层（落地能力）
- TypeScript 深度：Proxy、模块合并、generator、双模块系统缓存清除（ESM+CommonJS）——HMR 事务引擎的每一步都是这类知识的实战；
- 运行时调度语义：eager（Promise）与 lazy（Python 协程、Rust future）调度的差异及其对状态机的约束；
- 大规模开源社区运维：Koishi 四年、4000+ 插件的治理经验——没有它，「存在性证明」无从谈起。
7.4 知识融合的关键节点
真正的创造发生在三类知识的交汇处：
- 节点一（对偶的运行时化）：范畴论对偶（效应/协同效应）× 插件系统痛点 → 「把静态注解提升为运行时机制」——这是范式级的翻译，不是新定理而是新视角；
- 节点二（set 即效应）：发现协同效应的 set 操作类型上就是 𝔈*Σ——空间维的原子操作就是时间维的效应——统一上下文 Γ∞ 因此水到渠成，而不是硬拼两个系统；
- 节点三（观测等价买独立性）：把可逆计算的全局可逆要求，用「协同效应接口可观测范围内的等价」放宽到工程可满足——理论严格性与工程可行性的折中点找得极准；
- 节点四（守卫与级联）：Unloading 态 + 表退出并集 → 依赖者目标视图自动失效 → 守卫必然释放——用一个数据流设计同时解决死锁与异步拆解，是演算设计与实现算法（Algorithm 5）之间最漂亮的往返。
八、论文中可以提取的通用性灵感
灵感 1：把「撤销」做成创建的返回值，复合的撤销由结构导出
核心思想：任何「改世界」的操作都应在修改发生的当场返回自己的逆；复合操作的逆不需要单独设计——按相反顺序复合即得。 论文证据：𝔈Γ 类型签名 + 定理 10/11（复合封闭）+ Koishi 中无经验作者零卸载代码获得完整清理。 推广场景：① 数据库 schema 迁移工具（每次迁移自动生成 down 脚本）；② 基础设施即代码（Terraform 状态管理的形式化基础）；③ 编辑器/设计软件的无限撤销栈；④ LLM Agent 的行动回滚（每个动作配补偿，复合行动的补偿自动导出）；⑤ 分布式事务的 Saga 编排自动生成。
灵感 2：把「需求声明」做成可判定的满足谓词，响应性由观测点保证
核心思想：与其让每个模块各自轮询环境变化，不如让（a）需求是有限声明、（b）一切环境变更都流经单一咽喉点——这样「变更通知」就是结构性质而非外加基础设施。 论文证据：σ ⊧ d 可判定 + 一切变更经效应函数 → notify 分类（Definition 26）；OSGi 因回调同步而做不到的异步拆解被 Unloading 惯性态解决。 推广场景：① 微服务依赖健康度编排（服务网格的控制面设计）；② 前端依赖注入容器；③ 团队管理——把「谁需要谁」显式声明出来，变更自动传播责任边界；④ 实验管理系统的环境配置（声明式依赖 + 自动启停依赖服务，如 docker-compose 的反应式升级）。
灵感 3：粒度对齐原则——管理机制必须与被管理对象同粒度
核心思想：当回收/协调机制（进程、容器）天然比被管理对象（组件、函数）粗时，一切性能与正确性问题都是粒度错配的症状；把机制下沉到对象自身的粒度是范式机会。 论文证据：§1.2.3 的论证——进程级时间可组合性与容器级空间可组合性的代价分析；这正是「meta-framework」的立身之本。 推广场景：① 数据库连接池内单连接的隔离与回收；② GPU 显存的对象级生命周期管理；③ CI 流水线从「整库重建」到「受影响子图」的演进；④ 记忆系统的条目级遗忘（LLM Agent 记忆管理）。
灵感 4：用「观测等价」为不可严格恢复的事物定义足够的恢复
核心思想：物理上无法逐比特还原时，问「谁能观测到差异」，把等价收缩到观测接口范围内——严格性让位于可满足性而不失可证明性。 论文证据：Definition 33 + 引理 38——堆布局、生成名被有意遗忘；CompCert 同款思路用于内存模型。 推广场景：① 缓存失效策略的形式化（什么程度的旧是可接受的旧）；② 隐私合规的差分定义（观测者视角界定信息泄露）；③ 增量计算的一致性标准（Adapton/Salsa 的迹有效性）；④ 协作文档 CRDT 的收敛定义。
灵感 5：「合流性」是信任自动化修改的前提
核心思想：让一个不断自我修改的系统可信，最强杠杆是证明「修改历史不留痕迹」——终态只由最终配置决定。有了它，调试、回滚、审计全部简化为「看当前配置」。 论文证据：定理 73 + 推论（唯一范式形），以及它如何直接支撑组件加载器的增量协调（§5.2.1 四条理由逐条引用元定理）。 推广场景：① 自进化 Agent 的安全护栏（MOSS 类系统的正确性基线）；② 声明式配置系统（Kubernetes 的 reconcile 循环理论化）；③ 数据管道的幂等重放设计；④ 个人知识库的增量重构。
灵感 6：理论-实现对照表作为研究方法论
核心思想：形式系统与工程实现之间维护一张逐构造对应表（本文 Table 2 把每个符号、每条规则映射到运行时名字），是防止理论与实现「两张皮」的低成本高收益实践。 论文证据：Table 2 全表 + 案例研究反复回指具体行号（Algorithm 5 的三行代码分别对应定理 63 的三个子句）。 推广场景：① 任何带形式模型的系统论文写作；② 大型重构的迁移映射文档；③ 规范与代码的双向追踪（需求工程的可追溯性矩阵）。
结语
这篇论文做的事情，用一句话概括：为「软件在运行时改变自己」这件事，补上了词法作用域之于静态语言、进程之于操作系统那个级别的形式基础。它从两个具体的工程痛点出发（VSCode 的 87/100、自进化 Harness 的重启困境），穿过效应/协同效应这对范畴论对偶，落到一个递归上下文类型、一个十规则演算、五组元定理，最终收束在一个已经跑了四年、养着 4000 个插件的框架上。对 Agent 领域的读者，它的意义尤其直接：当 Harness 真的开始自我修改时，这篇文章提供的「完整恢复 + 依赖协调 + 历史不留痕」三件套，就是那份目前唯一存在的数学底座。