BotOf Tech — 技术与植物养护笔记

译文系列（2/4）：① 问题、预备知识与上下文范式 · ② 动态组合演算 · ③ Cordis 实现与 Koishi · ④ 系统边界、相关工作与结论

本篇承接统一 context，把局部 effect/coeffect 机制提升为多组件交错运行时的动态组合演算。

4. 动态组合演算

本章把前述局部机制提升为一个可运行系统：多个组件交错加载、卸载、替换时，怎样仍然保持时间与空间上的可组合性。核心对象是 fiber。组件是静态声明，fiber 则是组件在某个上下文中的一次具体实例。

4.1 组件、fiber 与 registry

定义 43（组件）。 在同时携带 effects 与 coeffects 的上下文 Γ 上，一个组件为三元组：

ℭ_Γ := 𝔇_Γ × 𝔓_Γ × 𝔈*_Γ
component = (d, p, e)

d 是需求规格，声明组件要读取哪些 key；p 是提供规格，声明它将提供哪些 key；e 是组件加载时执行的带见证可逆 effect。这里的 p 是承诺，而不是当前状态：只有 fiber 真正处于 Active 时，这些 key 才算已提供。

定义 44（fiber）。 固定 fiber 名称集合 𝔑。组件 (d,p,e) 的实例是：

⟨d, p, e, π, σ, τ, θ⟩

π：父 fiber 的名称，确定上下文树中的所有权；
σ：fiber 在运行期间登记的子 fiber 表；
τ∈{⊥,⊤}：是否已退休；
θ：生命周期状态。

基础演算中，状态是 Inactive(ξ) 或 Active(g,ω)：ξ 是失败信息或空值，g 是卸载时使用的累加逆，ω 是激活瞬间提交的依赖视图。后续异步演算还会加入 Reloading 与 Unloading。所谓 committed view 很重要：provider 开始退出后，consumer 的卸载逻辑仍可使用它激活时看到的同一份依赖，而不会读到半新半旧的 registry。

定义 45（registry）。 每个状态携带有限偏映射 F_γ : 𝔑 ⇀ 𝔉_Γ。所有 fiber 的局部子表之并恰好等于 registry；每个名字只出现一次；每个 key 至多有一个活动 provider。最后一条让依赖解析成为函数，而非不确定选择。

4.2 基础规则

定义 46（目标视图）。 target(γ,n) 把 fiber n 声明的每个 key 映射到当前活动 provider；只要有一个需求未满足，它就是 ⊥。quiet(γ) 表示每个 fiber 的当前生命周期状态已与目标视图一致，即系统没有待执行的激活或卸载。

基础演算有五种动作：

O-Insert：父 fiber 执行 effect，登记一个新的子 fiber；
O-Retire：执行登记动作返回的逆，把子 fiber 标为退休；
O-Remove：已退休、Inactive 且无子项的 fiber 从 registry 删除；
L-Reload：Inactive 且依赖已满足时，提交当前依赖视图并执行组件 effect，进入 Active；
L-Unload：Active 且目标已变化时，执行累加逆并回到 Inactive。

定义 47（登记也是 effect）。 组件实例化必须发生在另一个 effect 内；O-Insert 的逆就是 O-Retire。于是父组件卸载会恢复其登记动作，退休所有子组件，形成递归的生命周期所有权。

定义 48（受限变换）。 组件 effect 只能写自己的生命周期状态与局部登记表；它可以读取全局 registry 与 committed view，但不能直接改写别的 fiber。这个 confinement 条件是后续交换性证明的边界：若组件绕过 context 修改共享全局量，定理不再适用。

4.3 进行中的转换

现实中的加载和卸载会异步等待，也可能在途中发生依赖变化或失败，因此一步完成的基础规则还不够。

定义 49（惯性状态机）。 生命周期扩展为：

Inactive(ξ) | Reloading(g,ω,i) | Active(g,ω) | Unloading(g,ω)

其中 i 是尚未消费完的 effect iterator。已安装指 Reloading、Active 或 Unloading；失败 fiber 是 Inactive(ξ) 且 ξ≠⊥。

4.3.1 provider 撤回

定义 50。 若某个已安装 consumer 的 committed view 把 key 解析到 provider n，则 n 正被依赖。provider 的退出拆成两步：L-Leave 先将其标为 Unloading，使其立刻停止对新解析“提供服务”；然后等待原有 consumer 全部卸载，才执行 L-Unload 撤回真实 binding。顺序因此是：

provider 停止对外提供
  → consumer 看到依赖失效并完成清理
  → provider 才撤回资源

这避免 consumer 在清理期间拿到悬空引用。

4.3.2 可中断的迭代加载

定义 51（effect iterator）。 effect 可写成逐步产生逆操作的 iterator：

𝔈^iter_Γ := Γ → Maybe(𝔈_Γ × 𝔈^iter_Γ)

每完成一个原子步骤就交出其 inverse。若依赖在异步间隙变化，系统不再推进 iterator，而只恢复已经完成的前缀。

定义 52（追踪 iterator）。 effect^iter 把 iterator 提升到递归 effect 上下文；每得到一个 inverse，就前插到累加器，因此最终按 LIFO 执行。普通 effect 是只 yield 一次的退化 iterator。

迭代规则分为 L-Begin、L-Iter、L-Finish 与 L-Divert。前三者启动、推进和提交加载；L-Divert 在目标视图已变化时终止旧迭代并转入卸载。系统由此既不会强行取消正在执行的原子步骤，也不会让过期配置继续跨过下一个安全边界。

4.3.3 异步惯性

异步 transition 一旦开始便运行到完成；期间到来的目标变化只更新目标，不抢占当前 transition。Reloading 完成后若目标已过期，就串接 Unloading；Unloading 完成后若目标又恢复，就串接 Reloading。这个“惯性”语义把任意密集的外部变更压缩成一串完整状态转换，避免两个 cleanup 同时操作同一资源。

4.3.4 失败

加载 iterator 抛错时应用 L-Raise：已积累的 inverse 全部执行，fiber 进入带错误值的 Inactive，committed view 清空。失败不会留下本次尝试的可观察副作用；后续目标再次变化时仍可重试。卸载 inverse 若自身失败，则超出“inverse 确实恢复对应 effect”这一见证义务，运行时不能凭空修复它。

4.4 元理论：系统整体保证什么

定义 53（episode）。 给每步编号 t。fiber 从开始 Reloading 到最终完成对应 Unloading 的区间称为一次 episode；它把一段可能交错的全局执行圈定为一个组件的完整生命周期。

引理 54（写入清单）。 逐条检查规则可得：一个生命周期动作只写当前 fiber 的状态/累加器/committed view；登记动作只写父 fiber 的局部表和新 fiber；删除只删除满足严格条件的遗留项。

引理 55（≃ 不变性）。 若两个初始上下文观测等价，则相同规则在两边同时可用，执行结果仍观测等价。

引理 56（名称等变性）。 对 fiber 名做任意双射重命名，不改变规则是否可用或执行含义。名字只是身份，不承载业务语义。

引理 57（遗留项）。 已退休、Inactive、无子项且不再提供任何 key 的 vestigial fiber 可删除，不影响任何后续可观察行为。

4.4.1 保持性

定义 58（良构 registry）。 registry 满足父子登记一致、名称唯一、父项存在、活动 provider 唯一、状态与局部表结构匹配等不变量。

定理 59（Preservation）。 若第 t 步前 registry 良构，那么无论应用哪条规则，第 t+1 步后仍良构。证明按规则分类，利用写入清单排除对不相关 fiber 的破坏。

4.4.2 时间可组合性

定义 60（全局两两独立）。 一个 episode 中所有触及共享状态的原子 effect 与系统交错步骤两两独立；iterator 可达的后续阶段也必须满足这一点。

定理 61（精确恢复）。 在两两独立、effect confinement 与 inverse 见证成立时，某 fiber episode 结束后，删除该 episode 自己的登记动作，最终状态与 episode 开始前观测等价。证明把 interleaving 中属于该 fiber 的步骤通过交换律移到一起；它们的 inverse 以反序相消，其余组件的步骤保持原序。

推论 62（终态恢复）。 已退休 fiber 最终被删除时，它对上下文的可观察贡献为零。这是“卸载干净”的系统级版本，不只是单个 effect 的局部性质。

4.4.3 空间可组合性

定理 63（顺序）。 fiber 只有在依赖都由 Active provider 提供时才开始加载；provider 在所有依赖它的 consumer 完成卸载前不会撤回自己的 effect。因此 consumer 的整个 episode——包括 teardown——都位于 provider 的可用区间内。

定理 64（解析一致性）。 一个 episode 在开始时提交的依赖视图 ω 在整个 episode 内不变。依赖变化可以触发下一次转换，却不会让正在进行的 transition 同时跨越两套 provider 解析。

4.4.4 进展

定义 65（先行关系）。 m≺n 表示 n 的运行或卸载必须等待 m，来源包括父子所有权与 provider/consumer 依赖。

定理 66（Progress）。 若 ≺ 无环、每个 effect iterator 有有限长度、可生成的名称有限，并且调度器持续选择生命周期规则，那么系统经过有限步必达 quiet 状态。证明以依赖 DAG 的秩、剩余 iterator 长度及未完成 transition 数构造递减度量。

4.4.5 汇合

定义 67（supported）。 未退休、父 fiber 也 supported、依赖声明能由 supported provider 满足的 fiber 属于支持集。

引理 68。 在无环先行关系下，支持递归有良基，不会无限回溯。

定义 69（提供完备）。 组件成功激活时，确实安装其 p 声明的全部 key。

引理 70。 在 quiet、无失败、提供完备的状态中，Active fiber 恰好等于支持集。

引理 71（换位）。 两个独立步骤若相邻，可交换次序而得到观测等价状态。

引理 72（删除）。 可从执行历史中删去一个最终不受支持 episode 的登记、生命周期与移除步骤，而不改变剩余终态。

定理 73（Confluence）。 在两两独立、无环、提供完备且最终 quiet、无失败的条件下，终态由最终仍受支持的组件集合唯一决定，与加载/卸载请求的交错顺序无关；任何两条到达静止点的执行都得到观测等价的规范形。

这一定理不是“并发程序自动正确”的万能结论。它明确要求原子 effect 独立、inverse 正确、依赖无环、声明兑现；Cordis 的价值是把这些义务集中在少量原语边界，而不是让每个业务调用点都手工维护。