A Programming Paradigm for Spatiotemporal Composability

0.导读：怎么读这篇论文入门

这是一篇"理论 + 工程"双线并行的论文：前半部分（§1–§4）建立形式化模型，后半部分（§5–§7）讲实现、案例与相关工作。两半可以分开读，但它们的连接点非常清晰——第 5 章开头有一张"理论 ↔ 实现对照表"，把每个数学符号对应到一行代码。

如果你只想了解"这东西是干什么的"，读 §1 动机 + §12 总结 就够；如果你想知道"它为什么是安全的"，重点是 §3 的两个机制 + §4.4 的六条定理；如果你想读懂 DeepSeek Harness 的底层（Cordis），重点是 §5 的五个算法。

本页面的讲解按七个深度层级组织，每一层的难度都用彩色标签标出：入门 不需要任何前置知识；进阶 最好懂一点函数式编程概念（会用就行，我会补直觉）；深入 涉及操作语义和证明，我会把每条定理翻译成"人话"再给形式化定义。

1.动机：动态组合的难题入门

为什么"把组件装进程序"这件事，静态时很容易，动态时却很难？

组合（composition）是软件工程的根基：把简单部件拼成复杂系统。传统上，组合是静态的——函数调用、模块导入、类继承，在编译期就定死了，运行期一成不变。但现代软件越来越多地要求动态组合：组件在运行时被加载、卸载、重新配置。

两类最典型的场景：

• 插件系统：浏览器扩展、编辑器插件、游戏 Mod，用户在运行期安装/禁用；
• 自进化的 Agent Harness：现代 AI Agent 依赖运行时 harness 来组合工具、管理权限、维护会话状态、编排子代理。论文特别指出——未来的 harness 会在持续服务的同时，由模型生成并部署对自己组件的修改（§1.2.2）。每一次自修改，都是一次动态组合。

问题在于：与静态组合丰富的理论（类型系统、模块系统）相比，动态组合几乎没有形式化基础。实践中大家都用一个"粗糙的替代品"，下面两个例子说清楚代价有多大。

1.1案例一：VS Code 插件系统

VSCode 的扩展都跑在一个共享进程（extension host）里。论文给出了一组 2026 年 6 月的实测数据：

• 时间维度的问题：扩展可以动态安装，但 host 没有任何机制能在运行时卸载单个扩展的代码。一旦扩展的 activate 执行过，禁用/卸载它就必须重启整个 host——影响所有已加载的扩展。纯声明式扩展（主题、快捷键、代码片段）没有代码、可以自由移除；但安装量前 100 的扩展里有 87 个包含可执行代码，移除它们全都需要重启。VSCode 提供的 deactivate 钩子只是进程退出时的"优雅关闭回调"，不支持活卸载；而且它把"清理"和"创建"拆在两个函数里，违背了关注点局部性——完整清理几乎无法验证。
• 空间维度的问题：VSCode 有 extensionDependencies 机制，但几乎没人用——前 100 名里只有 7 个扩展声明了对非内置扩展的依赖。原因在于 API 形态：扩展通过命令、视图、语言特性这些固定扩展点与宿主交互，而不是相互依赖；跨扩展交互的唯一通道 getExtension(...).exports 返回的是无类型值（any），没有任何结构性契约。

1.2案例二：自进化 Agent Harness 为什么"必须"要它

一个未来 harness 可能：组合各种工具套件、治理权限与沙箱、维护会话状态与持久化、提供上下文管理与记忆、编排子代理与多代理工作流。当它开始自我修改（模型生成新组件、替换旧组件）且这种修改"持续发生、几乎无人监督"时：

• 没有时间可组合性：每次自修改都要全量重启 → 丢弃进程内积累的全部状态（缓存、连接、半成品计算），进行中的任务被反复打断；更糟的是，一个坏的自修改可能把恢复所需的那部分进程本身也弄死。
• 没有空间可组合性：每个模块都得自己用临时手段（ad hoc）探测依赖的消失/出现/换身份；幼稚的代码替换可能静默破坏依赖者，或者引入只在重载时才暴露的循环依赖。

1.3现状：大家都在用"粗糙粒度"的替代品

为什么这个问题长期没被认真对待？因为操作系统和容器编排器已经提供了一个粗粒度的替代品（§1.2.3）：

代价是实实在在的：重启丢弃全部进程内状态，重建要几秒到几分钟，期间要冗余副本维持可用性；容器层级无法表达同一地址空间内组件之间的依赖，本可以是本地函数调用的交互被迫走网络。而现代系统恰恰在比进程更细的粒度上做组合。粒度错配——这就是论文要补的洞：需要一个"在组件自身粒度上管理效应与依赖"的抽象。

2.两个维度：时间与空间入门

整篇论文的地基：把"动态组合"拆成两个正交（互不干扰）的维度。

一个很漂亮的对照（§1.1）：在静态世界里，这两个维度各自早已有成熟的答案——

比如 Python 的 with open(file) as f：文件在 with 块结束时必然关闭——因为块是静态写死在代码里的。但一个插件在运行了三天之后被用户禁用，它注册的事件监听、占用的数据库连接、挂载的路由，没有任何静态结构能"框住"它们。

记住这两个词：时间 = 效应的可逆化，空间 = 依赖的响应式解析。后面五章全是这两句话的展开。

3.预备知识：效应与协效应进阶

论文的两根理论支柱。放心，这里只讲"直觉 + 结论"，够用。

3.1效应（Effect）：程序对世界的影响

类型系统里，Γ ⊢ t : T 表示"在上下文 Γ 中，项 t 有类型 T"。效应系统把类型再细化一步，标注这个计算会产生什么副作用：

-- 普通类型：只说了结果是什么
f : Int -> Int

-- 效应系统：还说了计算会"搞出什么事"
f : Int -> Int ! {IO, State}   -- 会做输入输出、会改状态

两个代表性流派：

• Monadic effects（Moggi / Wadler）：把"有副作用的计算"包装成一个值（monad），比如 Maybe（可能失败）、State（可变状态）、IO（外部交互）。Haskell 的 do 语法是它的日常面孔。
• Algebraic effects（Plotkin / Power / Pretnar）：把效应操作（如 get/put）和它们的解释（handler）解耦，同一个操作可以有多种语义。Koka、Eff、OCaml 5 都实现了它。handler 拿到操作参数和定界续延，可以调用零次、一次或多次——异常、协程、非确定性都被统一进一个框架。

3.2协效应（Coeffect）：世界对程序的约束

协效应是效应的对偶：效应标注在结果类型上，协效应标注在上下文上——描述计算需要从环境得到什么：

-- coeffect 系统：上下文带上"需求标注"
Γ!{2×Time, 512MB} ⊢ render : Frame   -- 渲染一帧需要 2 倍时长预算、512MB 内存

一句话对照（这句是全文金句，§2.2）：

两个代表性流派：

• Comonadic coeffects（Uustalu & Vene / Petricek）：用 comonad 组织"依赖上下文的计算"，比如 Environment comonad E × X（依赖固定环境）、Stream comonad（依赖时间序列）。
• Graded coeffects（Gaboardi 等）：用预序半环给每个变量绑定标注"用量"：0（不用）、1（线性，恰好一次）、n（有界次数）、∞（随便用）。能精确跟踪资源、做敏感性分析、信息流控制。

3.3关键转折：这两个概念正好对上两个维度

但经典系统有个致命局限：它们全是静态仪器——效应在词法固定的作用域内被编译期 handler 消化；协效应标注对着"执行前就定死的上下文"做校验。没有任何固定词法作用域能框住一个部署后才加载的插件；没有任何编译期上下文能预知运行期配置里才出现的依赖。

于是论文做出核心转向（§2.3）：不继续往类型系统里加标注，而是把效应/协效应的概念结构"物化"（reify）成运行时可以直接操作的对象。静态系统在编译期保证的东西，改成在运行期动态建立。这就是第 4、5 章的内容。

4.可逆效应（Revertible Effects）进阶

时间维度的答案：每个改动都自带一个"撤销键"，运行时负责把它们串起来。

4.1核心思想：效应 = 变换 + 逆变换

一个副作用，本质上是"把环境从状态 γ 变成状态 δ"。要能撤销它，就得知道怎么从 δ 变回 γ。论文把效应建模成这样一个函数（§3.1）：

-- 效应：吃进当前上下文，吐出【新上下文 + 撤销它的逆函数】
effect : Γ → Γ × (Γ → Γ)
--        ↑状态     ↑逆变换（undo）

这个设计有三个妙处：

• 显式：逆不是"开发者事后记得写个清理函数"，而是效应值的组成部分；
• 就地：逆在效应应用的那个点产生，而不是预先给定——因为撤销动作往往取决于当时的具体状态（比如注册监听器时才知道注册了哪个）；
• 可组合：一串效应的逆 = 各逆按相反顺序复合。这就是大家熟悉的 LIFO（后进先出）：最后装的先拆。

4.2效应上下文：状态 + 累积器

为了让运行时能"跟踪"效应，论文定义效应上下文 ∂Γ = Γ × (Γ → Γ)，它是一个二元组：

• γ : Γ —— 当前上下文状态；
• φ : Γ → Γ —— 累积器（accumulator），到目前为止所有逆变换的复合。φ(γ) 能把上下文一路倒回到初始状态。

两个基本操作（§3.1.1）：

track(f, g) : (γ, φ) ↦ (f(γ), φ ∘ g)     -- 执行变换 f，并把它的逆 g 复合进累积器
recover      : (γ, φ) ↦ (φ(γ), id)      -- 应用累积器：状态倒回，累积器清空

4.3一个必须强调的细节：见证（Witness）

不是随便写个逆就行的。论文用带见证的效应函数 𝔈* 形式化这个要求（定义 8）：

-- e(γ) = (δ, g)，见证条件要求：
g(δ) = γ        -- 逆 g 作用在【被自己那个效应改过之后的状态】上，恰好还原

注意这是单侧（one-sided）的：只要求 g∘f = id，不要求 f∘g = id。撤销是"回去"，不是"可逆双射"。另一个关键点：见证条件只在"效应被应用的那个状态"处成立——逆不需要在任何状态都能用。这个放宽至关重要，第 7 章的撤销守卫（guard）机制就建立在这个观察上。

4.4撤销一个撤销，本身也是一个效应

一个很优雅的自相似结构（定义 12）：把效应 e ∈ 𝔈_Γ 提升到 ∂Γ → ∂²Γ 后，它的逆是 track(g, pr1∘e)——"撤销这个效应"本身是被跟踪的效应，而"撤销撤销"就是"再做一遍原效应"。这就是实现里 ctx.effect 返回 dispose、而子效应的 dispose 又挂到父上下文上的数学对应物。

4.5多个组件交错时：独立性（Independence）

单组件很简单：累积器按 LIFO 一把收回。但真实系统里多个组件的效应交错执行——组件 A 的逆可能在"组件 B 之后又改过"的状态上运行。它还撤得动吗？撤的是不是只属于自己的那部分？

论文的答案（定义 19）：两个效应独立，当且仅当

1. 它们所有可能的变换两两交换（先 A 后 B 和先 B 后 A 结果一样）；
2. 一方的前向变换不改变另一方产出的逆（B 动了状态之后，A 拿到的逆还是原来那个）。

在这个条件下得到漂亮结论（定理 20 + 推论 21）：互相独立的效应可以按任意顺序撤回，每个逆到达的状态 = "这个效应从来没被应用过"的平行世界状态——各撤各的，互不牵连。

那独立性从哪来？答案埋了个伏笔，在第 6 章的观测等价里揭晓：把每个共享位置绑定为一个协效应 key，跨 key 的操作天然独立（定理 40）；同 key 的操作只要这个 key 是"可交换的"（如路由表、监听器表），也独立（定理 42）。换句话说：可交换的部分交给效应（随便什么顺序撤销），顺序敏感的部分交给协效应（用声明依赖来约束顺序）——这就是两个维度为什么"正交又互补"。

5.响应式协效应（Reactive Coeffects）进阶

空间维度的答案：依赖是一张可变的表，组件对表的每个变化做出反应。

5.1协效应上下文：一张带类型的依赖表

传统 IoC 容器把依赖建模成简单的键值映射。论文把这件事形式化（定义 22）：

-- Σ：有限偏函数——依赖键 k 绑定到值，且每个键有自己专属的类型
Σ ≔ (k : K) ⇀ 𝒱ₖ          -- k 只接受类型 𝒱ₖ 的值（静态类型安全）

两个基本操作：get(k) 读值（键缺失则失败）、set(k,v) 写值（键已存在则失败，不能重复供给）。整篇论文最精妙的一笔在这里（§3.2.1）：

5.2一个 key 不只是个值：三元组

每个键的协效应是一个三元组 (𝒱ₖ, ≃ₖ, 𝒜ₖ)（定义 24）：

• 𝒱ₖ：值类型；
• ≃ₖ：值的等价关系（"多大差异算一样"，第 6 章的观测等价用它）；
• 𝒜ₖ：一组运算，每个运算 a : X_a → 𝒱ₖ ⇀ 𝒱ₖ × (𝒱ₖ ⇀ 𝒱ₖ) × B_a——作用于值、自带逆、再返回一个结果。连依赖提供的操作都要求带逆。

5.3规格与通知：响应式的来源

组件访问一个不存在的依赖是运行时失败。所以组件应该先声明、等满足、再激活，而不是乐观地访问然后炸掉。形式化（§3.2.2）：

• 规格 d ⊆ K：组件声明的依赖集合（在实现里就是 fiber.inject）；
• 满足谓词 σ ⊧ d ≔ ∀k∈d. k∈dom(σ)：所有声明键都有绑定；
• 通知分类 notify_d(σ,σ')：任何一次状态变换按"满足性是否翻转"分成三类——activating（不满足 → 满足）、deactivating（满足 → 不满足）、neutral（没变化）。

这给出局部空间可组合性判据：组件只在规格满足的状态激活（从不读缺失绑定）；每次上下文变化都被对照规格分类（满意度丢失当场检出并驱动停用）。注意这里有个"单向性"：依赖者后激活是自动成立的（不满足就不激活），但提供者撤销绑定时"先等依赖者撤完"是全局性质，留到第 7 章的撤回守卫解决。

5.4两个进阶机制：隔离与拦截

基础模型是一张扁平的全局表。实际系统需要更细的控制（§3.2.3）：

两个机制都是派生实现（derived realization，定义 27）：不碰共享表，而是派生一个子上下文——回收 = 丢弃子上下文，无需显式逆。拦截的右偏合并尤其重要：外层上下文可以在不改组件代码的前提下约束组件怎么用依赖（§6.3 用它做权限控制）。

6.上下文范式（The Context Paradigm）进阶

把两半拼起来：一个统一的上下文类型，和它带来的"观测等价"哲学。

6.1统一上下文：自相似的 Γ∞

第 4 章的效应上下文 ∂Γ = Γ × (Γ→Γ) 是"高一层"的抽象。把这个结构做成递归、再拼上协效应表 Σ，得到（定义 32）：

-- 统一上下文：递归、自相似
Γ∞ ≔ μΓ. Γ × (Γ → Γ) × Σ
-- 三个投影：当前状态 · 累积器 · 协效应表

要点：

• 自相似：效应映射 𝔈_{Γ∞} 又回到 Γ∞ 自己——"撤销撤销"的塔式结构收拢成一个类型；
• Σ 收纳一切共享状态：因为值类型族 𝒱 不受约束，任何需要跨组件共享的可变状态都可以编码成一个 key 的依赖——Σ 不只管"组件间依赖"，它收纳了所有共享状态；组件与环境的每一次交互都经过这个实体；
• 层级树：父上下文聚合子层效应，形成树状控制结构。加载 = "插上"，卸载 = "拔下"（不影响别的组件），任意层级嵌套。

6.2观测等价：恢复到"看起来一样"就够

一个诚实的哲学问题（§3.3.2）：recover 保证"状态恢复原样"，但物理上做不到——free 一块内存不会还原堆的布局；一个生成式名字（fresh name）被丢弃后，下一个名字还是新的。所以第 3 章所有"相等"都要读成"在一个等价关系 ≃ 下等价"。

≃ 取成观测等价：两个状态相关，当且仅当没有任何观察者能区分它们。观察者手里有什么？——协效应。于是（定义 33）：

-- 两个协效应上下文相关：绑定同样的键、键上的值各自相关
σ ≃ σ′  ⇔  dom(σ) = dom(σ′) 且 ∀k∈dom(σ). σ(k) ≃ₖ σ′(k)
-- 两个状态相关：它们的协效应投影相关（其余部分被"忘掉"）
γ ≃ γ′  ⇔  σ_γ ≃ σ_γ′

妙处：没有任何 key 绑定的状态部分被自动遗忘——堆布局、生成名恰好都在那里，所以"恢复到观测等价"是可达的。而满足谓词和通知分类恰好只依赖 dom(σ)，所以反应性不受影响。

每个 ≃ₖ 还要"名副其实"（定义 34、引理 35）：对值跑测试（用该 key 运算的生成元组成的有限序列），所有测试在两边都定义/都不定义且结果相同 ⇒ 不可区分 ≈。≈ 恰好是运算所尊重的最粗等价。独立性的定义也"读到 ≃ 为止"——两个运算把值改到 ≃ 认不出的程度，就算交换（引理 38）——这就是第 4 章伏笔的答案：所有共享位置绑定为 key，跨 key 运算天然独立（定理 40），同 key 运算在该 key 可交换时独立（定理 42）。

6.3范式定位：两个极端之间的第三条路

7.动态组合演算：组件、纤维与生命周期深入

把前两章的机制装进"组件"这个概念，给整个系统的运转写一套操作语义。

7.1组件与纤维（Fiber）

一个组件是一个三元组（定义 43）：

-- 组件 = (声明 d, 供给 p, 带见证的效应函数 e)
(d : Set K,   -- 声明：从环境读什么（coeffect 规格）
 p : Set K,   -- 供给：向环境写什么（效应函数只写 p 内的键）
 e : 𝔈*)      -- 激活时执行的效应 + 撤回它们的逆

一个组件可以被实例化多次，每次实例称为一个纤维（fiber），记录：组件、父纤维、自己的协效应表、退休标记 τ、生命周期状态 θ。所有纤维登记在注册表（registry）里，父指针构成一棵以 root 为根的树。关键设计：

• 协效应上下文是"派生"的（定义 45）：σ_γ = ⋃{σ_n | θ_n = Active}——所有激活纤维的表之并。一个键恰有一个"可能提供者"（供给集不相交）。只并激活纤维这一条，是后面"撤回守卫"成立的基石。
• 目标视图 vs 提交视图：target_n(γ) = "这个纤维现在应该以什么解析运行"（退休或不满足 → ⊥；否则每个声明键 ↦ 它的提供者）。ω_n = "它实际激活时锁定的是谁"。整个生命周期就是拿两者做比较。
• 静默（quiescent）：所有纤维都达到了目标视图。系统"安定下来"的状态。

7.2基础演算：五条规则

先做理想化：每步原子、即时、不失败。五条规则分两组（§4.2）——编排规则（O-）是外部输入，生命周期规则（L-）是系统自发行为：

两个要点：实例化原语（定义 47）——组件的效应可以注册子组件（= 一次 O-Insert，π 指向自己），其逆 = 退休子组件。所以卸载父组件会自动级联卸载子孙。限制性（confinement，定义 48）——每个效应函数只许写自己的表 σ_n、只许读自己声明的键。这个纪律让后面的证明能把"每一步写了什么"完整列成一张表（论文表 1）。

7.3四个现实性补丁：真实的转换不是一步

真实运行时里，"激活/停用"不是原子瞬间，规则被扩展成四状态机（定义 49）：

四个补丁逐一对应现实约束（§4.3.1–4.3.4）：

7.3.1撤回（Withdrawal）：先"停供"，再"等"，最后才"拆"

§3.2 要求：依赖者先激活；提供者等依赖者都停用之后才真正撤回绑定。后半句是难点——正在被拆除的组件跑自己的清理代码时，可能还需要用那个正在消失的依赖（关连接池 = 把连接还给提供者）。解法：把一步拆成两步（定义 50 + L-Leave/L-Unload）：

1. L-Leave：进入 UNLOADING，立即停止供给（自己的表离开 σ_γ，依赖者马上发现自己目标视图没了，开始自己的拆除）——但绑定还在、自己的提交视图还在；
2. L-Unload：带上守卫 ¬relied_n——没有任何已安装纤维还把它解析为提供者时，才跑累积器真正撤回绑定。

7.3.2迭代（Iteration）：激活是一串效应，可以在边界中止

效应迭代器 𝔈iter = μℑ. Γ → Γ×(Γ→Γ)×Maybe(ℑ)：每步产出（新状态、逆、续体）。它本质上是物化的定界续延——主流语言的 yield/generator 结构（§4.3.2）。规则 L-Iter 逐步推进；L-Divert：目标视图在迭代边界变了，就把已累积的逆一把回滚、转去卸载。中止粒度 = 迭代边界，这就是实现里 ctx.effect 回调写成 generator 的原因。

7.3.3异步（Asynchrony）：惯性（Inertia）

效应可能返回 Future(A)——提交和落地之间，外部状态会变。这一层的全部内容是惯性：一旦发射，迭代就必然落地，不能拒绝。目标视图在飞行中变了，也只能"先落地、再卸载"——不能让纤维在卸了一半时还短暂供给依赖、骗依赖者激活（§4.3.3）。实现里的 reload/unload 互相链式（chain）就是它。

7.3.4失败（Failure）：先回收，再记账

效应会失败：端口被占、文件不存在、对端不应答。迭代器改成可 raise（Either(Ξ, ...)）。规则 L-Raise：失败先路由进 UNLOADING——用累积器把已装的一半效应全部回收——然后才把错误记到纤维上（INACTIVE(ξ)）。失败纤维不阻塞任何东西（无提交视图、不进 relied），兄弟组件完全不受影响——这正是插件宿主想要的行为；错误记录在纤维上而不是冒泡给父组件。失败后不会自动重试（L-Begin 要求 INACTIVE(⊥)），因为"重试一个对未变环境已证明不健全的效应"没有意义。

8.元理论：六条定理意味着什么深入

形式化的回报：把"单组件安全"升级成"整个系统安全"。每条定理先给"人话"，再给形式。

8.1保持性（Preservation，定理 59）

人话：好系统不会变坏。注册表始终满足四条结构纪律：父指针合法成树；供给集两两不相交；每个已安装纤维的提交视图完整且指向真实纤维；每个解析指向的提供者都已安装。

8.2恢复精确性（Recovery Exactness，定理 61 / 推论 62）

人话：时间可组合性的全局形式。在任何交错之后运行 n 的累积器，得到的状态 ≈ "n 从未开始过"的世界里、其他纤维照常运转所能达到的状态——卸载恰好撤回自己的贡献，别的组件分毫不动。前提：组件的效应两两独立（定义 60，把定义 19 推广到迭代器）。

8.3有序性（Ordering，定理 63）

人话：空间可组合性的全局形式，三段保证：

1. 纤维只能在依赖被提供时开始激活（L-Begin 的前提就是 γ⊧d）；
2. 如果 m 把 k 解析到 n：n 的激活严格早于 m（b < b′），且 n 的卸载严格晚于 m（u′ < u）——提供者永远比消费者活得长；
3. m 的整个 episode 期间，σ_n(k) 恒定——消费者读到的绑定值不会半路消失/变脸。

这就是"依赖者拆除期间仍能读依赖"的形式保证，第 7.3.1 节的守卫机制就是它的实现载体。

8.4解析一致性（Resolution Coherence，定理 64）

人话：一次激活要么全程跑在同一个解析 ω 上，要么完整回收。因为跨多步的激活可能装进"对着一个已经过期的解析算出来的"效应。二分支：

1. 顺利走完 → ACTIVE(ω)；
2. 中途目标视图变了 → L-Divert / L-Raise 转入卸载，推论 62 保证完整回收。

加上异步层的惯性：飞行中的迭代不受此限（只能先落地再卸）——所以该定理是"析取式"，而 L-Iter/L-Finish 的前提 target=ω 与 L-Divert 的否定前提正好拼出这个保证。

8.5进展（Progress，定理 66）

人话：系统不会卡死，而且一定安定下来。两部分：

• 无死锁：只要不静默，就必然有规则可走——尤其撤回守卫必然释放（沿 ≺ 无环链论证）；
• 终止：每个纤维的步数有上界 S(n) ≤ (K+4)(V(n)+1)（K = 迭代器长度上界，V = 目标视图翻转次数），而 V 自身沿 ≺ 下降有界（前提：≺ 无环、名字有限、组件不会无界地注册自身实例）。

它同时证明了一件工程上重要的事：一个只在 L-Begin 等待"依赖就绪"的纤维不会占着资源空转——加载顺序无所谓，谁后到齐谁后激活。

8.6汇流（Confluence，定理 73）

人话：全文最有"哲学感"的一条：动态历史不留下痕迹。无论系统经历了怎样颠三倒四的加载/卸载/替换，它最终安定到的状态，和"一开始就把最终配置按依赖顺序静态装配好"所得到的状态一样。两条结论：

1. 规范形式：任何序列都能重排成"编排步骤保持原序 + 每个幸存组件按依赖拓扑序各激活一次"的规范序列；
2. 汇流：输入相同（编排步骤相同），则所有调度收敛到同一个静默状态（相差名字重命名，由引理 56 equivariance 处理）。

9.Cordis 实现：从公式到代码进阶

理论到实现的映射非常直接——这是本文最"工程友好"的部分。

Cordis 是元框架（meta-framework）：不像 Web 路由/ORM/UI 框架那样绑定具体领域，它只提供"通用动态组合语义"。三层结构：核心库（§5.1，实现效应/协效应系统）→ 组件加载器（§5.2，声明式配置 + HMR）→ 应用框架（§5.3，如 Koishi）。论文表 2 给出了完整的理论↔实现对照：Γ∞↔ctx、fiber↔fiber、累积器↔fiber.dispose、提交视图↔fiber.committed、L-Begin/L-Iter/L-Finish↔execute 的迭代循环、L-Leave↔refresh 标 UNLOADING、守卫↔unload 等待被通知的依赖者。

9.1核心原语：ctx.effect

所有上下文突变都流经一个原语（§5.1.1，算法 1）：

// ctx.effect(callback) —— callback 是效应迭代器（generator），
// 每一步 yield 一个逆；返回 dispose 闭包。
const dispose = ctx.effect(function* () {
  const timer = setInterval(tick, 1000)          // 正向效应
  yield () => clearInterval(timer)               // 返回它的逆

  ctx.set('logger', newLogger)                      // 提供依赖（set 本身也是效应）
  yield () => ctx.set('logger', oldLogger)          // 逆
})
dispose()   // 卸载时调用：按 LIFO 顺序跑全部逆

引擎 execute 驱动迭代器、把每步 yield 的逆前插（LIFO）复合；每步之前查守卫 guard()——守卫一跳，迭代停止、只保留已累积的逆（这就是 §4.3.2 的迭代边界中断）。ctx.effect 包装加两件事：自处置（armed 标志：dispose 至多触发一次，且立刻停止飞行中的迭代——逆绝不在"不是自己效应产出的状态"上跑第二次）；父组合（子效应的 dispose 前插到父上下文累积器——∂²Γ 的递归结构）。

9.2协效应操作与通知

三个符号槽（§5.1.2）：@@store（值表 σ）、@@isolate（realm 表 ρ）、@@intercept（元数据表 ι）。ctx.get(key) = 两跳解析 σ(ρ(k))。ctx.set 是 ctx.effect 调用（安装与删除都触发 notify）。通知（算法 3）遍历所有纤维：键命中其 inject 且 realm 一致 → refresh，返回受影响集合供调用者等待。有个微妙而关键的语义：绑定只有在安装它的纤维 ACTIVE 时才算可用——所以提供者一进 UNLOADING，依赖者提前一步看到"未满足"，在绑定还完好时就开始自己的拆除。

9.3组件生命周期：惯性状态机

ctx.use(component, config)（算法 4）把组件实例化为纤维：回调 = O-Insert（启动子生命周期），其返回闭包 = O-Retire（target←⊥ 并 unload）。实例化是父组件的一个普通被跟踪效应——父卸载级联子卸载。刷新/装载/卸载（算法 5）实现惯性状态机，三行代码承载定理 63 的三个保证：

另一个工程细节：fiber.target 按提供者 uid比较而非值——uid 永不复用，所以提供者被替换（哪怕提供相等的值）也能被识别并触发重载。reload 完成后若 target 已变，链入 unload；unload 完成后若 target 复活，链回 reload——惯性（§4.3.3）的实现。

9.4ctx[key]：代理访问 = 能力式安全

除了反射式 ctx.get/set，Cordis 用 Proxy 让 ctx[key] 像原生属性一样访问依赖（§5.1.4，算法 6）：沿纤维链向上走——

1. 某个祖先的 committed 视图绑定了 key → 授权，返回该绑定；
2. 走到一个声明了 key 但没提交的纤维 → 组件未加载 → 抛 INACTIVE_ACCESS；
3. 走到 root 仍无声明 → 抛 UNDECLARED_ACCESS。

9.5组件加载器：声明式配置与调和

核心库给的是命令式原语（ctx.effect/use/set）；编排者需要的是声明式接口（§5.2）。加载器把"期望的组装"写成持久化配置，再把配置的变更翻译成纤维操作。每个条目（entry）记录：id / url / isolate / intercept / config / disabled——恰好覆盖支撑集（定义 67）需要的四个字段（τ, π, d, p），所以条目就是纤维的忠实规格。嵌套加载由普通组件实现（@cordisjs/group、@cordisjs/include），仍然落在演算之内。

增量调和（reconciliation）——配置变了一点就只动一点，不是整个拆了重建。它的正确性直接引用元理论：

每字段的最小扰动策略：id/url 变 → 重建；isolate 变 → realm 重指派（算法 7，用"分隔符" δ_k 判定绑定是否属于该条目，移动时一并搬走）；intercept 变 → 原地更新（读取时才查，无需重载）；config 变 → 交给组件自己 diff；disabled 变 → 卸载/重载。组（group）的调和 = 按子条目 id 做键控 diff，递归下行。

9.6热模块替换（HMR）：模块级的可逆效应

论文的主张：因为纤维已经框住了组件的全部效应与协效应，HMR 不需要开发者标注"接受边界"（对比 webpack/Vite 的 module.hot.accept）——换模块 = 处置旧纤维（回收一切）+ 用新模块实例化新纤维。三阶段（算法 8/9/10）：

1. 分类：从改动文件出发做不动点，标记 accepted / declined（依赖环默认 declined → 触发整进程重启）；
2. 陈旧检测：条目依赖树碰到 accepted 模块即为陈旧（declined 作为边界挡在外面）；
3. 事务性重载：先备份并清缓存 → 逐个 dispose + 重新 use → 任何一个模块 import 失败（如语法错误）→ 恢复缓存、用备份组件全部回滚。系统永不进入"半重载"状态。

10.Koishi 案例与工程讨论入门

理论之外：这个范式在真实生态里撑住了吗？以及一系列务实的设计取舍。

10.1案例研究：Koishi（4000+ 插件）

Koishi 是建在 Cordis 之上的开源聊天机器人框架，四年积累了 4000+ 社区插件，从 IM 适配器、数据库驱动到管理控制台。三个看点：

• 表达性与通用性：Koishi 的每个功能都是"上下文原语之上的插件"，Koishi 本身只贡献聊天领域词汇。同一套模型在完全不同的运行时重现：它的网页控制台是第二个独立 Cordis 应用，插件组合的是浏览器/UI 原语。元框架不预设领域、也不预设运行时。
• 无认知负担的时间可组合性：§1 里 VSCode 做不到的"活卸载"，Koishi 天天做——控制台禁用插件，效应当场撤回；开发时 HMR 保存即重载、缓存和活跃连接保持不动。关键是新手作者不需要写卸载路径：经上下文做的效应自动被跟踪、逆自动复合。§1.2.1 说的"关注点局部性缺失"被抽象一次性解决。
• 开放生态的空间可组合性：与 VSCode 里"插件间几乎无依赖"形成对照，Koishi 有真实的依赖拓扑：IM 适配器供给各平台接入、数据库驱动供给持久化、功能插件声明并消费它们。运行时切换存储后端 → 只有解析发生变化的依赖者被重新激活，其余无感。插件与依赖通常由不同作者独立编写、只靠连接它们的协效应协调——跨作者、跨仓库的组装依然一致。

10.2讨论一：系统边界——哪些效应真的可逆？

一个效应能否被逆，取决于系统边界（§6.1）：能独占修改且能恢复的位置在边界内；两者缺一就在边界外——外部的操作记为 id_Γ，既不跟踪也不恢复。边界按位置划，不按介质划：一块内存若只被本系统写就在内，别的进程也写它就在外；私有路径的临时文件在内，别的程序读写的路径在外。协效应会移动边界：把外部位置物化（reify）成 key，所有访问被限制在它提供的、带逆的运算集内，原本的 id_Γ 操作变成可跟踪。

每个跨边界的操作分两段：获取（acquisition）——open 装描述符、malloc 留块、fork 起子进程，记录落在边界内，可逆；发射（emission）——write 的字节、send 的数据报，数据去了别人能读写的地方，不可逆。对不可逆的发射只有两条路：扣留（withhold，等状态确定持久再发——回滚恢复的输出提交问题）或补偿（compensation，删掉已建的文件、退款已收的款——按应用提供的一个更粗的等价关系恢复，且补偿按 LIFO 复合，但元理论要在更粗等价上重新证明）。

10.3讨论二：服务复用、安全、循环、版本（速览）

10.4运维视角：回退、降级与故障半径

把这套理论翻译成运维语言，它的价值就一目了然了。先给一张总对照表：

例一：一次线上故障回滚（连接池）

场景：组件 A 提供连接池（key db），B、C 声明依赖 {db}。A 刚上线的新版本出现故障，需要回滚。

1. 你的动作只有一个：卸载 A（或把配置里的 A 条目换回旧版本——加载器会自动调和）。
2. 框架自动执行：A 进入 UNLOADING、立即停止供给 → B、C 发现目标视图变化，开始自己的停用（拆除期间仍能读旧连接池，连接优雅归还）→ B、C 到达 INACTIVE → 守卫释放 → A 的累积器按 LIFO 跑逆（恢复旧池、撤销监听）→ A 到 INACTIVE。
3. 保证：整个过程 B、C 之外的组件无感（推论 62）；顺序正确性由定理 63 背书，不用人肉编排。

对比传统做法：回退方案里要写清"先停 B、C → 还连接 → 切池"的顺序，还要在回退那一刻重新判断 B、C 是否在跑、影响面多大——这里全部由声明推导。负担从"每次回退时系统地想一遍 B 和 C"，变成"设计时写一行 inject 声明"。（§7 的模拟器 3 就是这个场景的动画版。）

例二：不停服的滚动升级（§6.2）

1. 新版提供者作为额外的普通组件加载，向服务代理（broker）注册；
2. 等它 ACTIVE 之后，逐步把流量从旧提供者切过来（调整选择权重）；
3. 旧提供者排空在途请求后卸载（论文指出这遵循的就是 DSU 领域的 quiescence/tranquility 时间纪律）。

例三：故障半径——坏组件不拖垮宿主

（可以直接玩 §7 的模拟器 4。）一个组件激活到一半失败（端口被占、依赖起不来），框架的行为是：回滚它已装的一半效应 → 把错误记在它自己头上 → 兄弟组件照常运行 → 不自动重试。用运维的话说：故障隔离与干净回滚是框架的责任，"永不出故障"从来不是。论文明确把失败排除在汇流定理之外（§4.4.5）：不同调度可能让不同组件失败——故障是发散的、不可完全预演，能保证的是故障半径（推论 62：失败组件对状态的贡献为零）。

运维速查卡

11.相关工作地图进阶

"这不是第一个想解决这件事的人"——论文如何把自己摆进四片研究版图。

12.总结：与 DeepSeek Harness 的关系入门

绕了一大圈，回到我们出发的地方。

12.1论文做了什么（三段式回顾）

1. 识别问题：动态组合有两个正交维度——时间（撤销副作用）与空间（响应式依赖），经典效应/协效应系统是静态的，不适用于运行期装卸。
2. 建立理论：把效应物化为"变换+逆"（可逆效应 → 局部时间可组合性），把协效应物化为"规格+通知"（响应式协效应 → 局部空间可组合性），统一进一个自相似的上下文类型 Γ∞，用观测等价补上独立性；再用一个带生命周期语义的演算把保证从单组件推广到整个系统（保持性、恢复精确性、有序性、解析一致性、进展、汇流）。
3. 落地工程：Cordis 元框架（ctx.effect / ctx.set / ctx.use / 代理访问 / 声明式加载器 / HMR），Koishi 生态（4000+ 插件）作为存在性验证。

12.2关系链：论文 → Cordis → DeepSeek Harness

《A Programming Paradigm for Spatiotemporal Composability》（本文）
        │  设计蓝图（Cordis 的设计论文）
        ▼
Cordis —— 时空可组合性元框架（cordiverse/cordis）
        │  底层引擎（"powered by Cordis"）
        ▼
DeepSeek Harness（dsh）—— "Everything is a Plugin."
        │  你正在用的本页面（Web GUI）就是它
        ▼
自进化 Agent Harness（论文 §1.2.2 与 §8 结论指向的未来）

论文的结论章把"自我进化的 Agent Harness"列为最有说服力的未来验证方向：AI 在几乎无人监督的情况下持续生成并替换自己的 harness 组件——需要"快速组件替换下的完整恢复"（时间保证）与"频繁拓扑变化下的依赖协调"（空间保证）。这正是 DeepSeek Harness 所站的位置：你眼前这个由插件组装、插件还能改装自己的系统，就是这篇论文想要支撑的那类系统。

13.术语表入门

14.自测小测验入门

读到这里，检验一下自己真的理解了吗？点击选项即时判分。

15.论文信息与引用入门