组件生命周期与卸载顺序

论文版本948a07b (main)

Revertible Effects 解决"撤销",Reactive Coeffects 解决"感知依赖变化"。两者要在组件实例上协同,需要一个完整的生命周期状态机。论文 §4.3 给出这套机制,其中 Provider/Consumer 卸载顺序是最重要的工程细节。

完整状态机

【论文原文结论 §4.3 Def 49】组件(fiber)的完整生命周期状态机:

七个 L- 原语:

原语	触发	语义
L-Begin	target ≠ ⊥ 且 fiber 在 Inactive	进入 Reloading,记录 committed view,启动 effect iterator
L-Iter	Reloading 中,target = ω,iterator 产出 Just(i')	应用一次 iteration 的 effect,复合 inverse 到 accumulator
L-Finish	Reloading 中,iterator 产出 Nothing	所有 effect 安装完毕,进入 Active
L-Divert	Reloading 中,target ≠ ω(依赖变化)	中止/着陆当前 iteration,进入 Unloading(要么 abort、要么 land 再 unload)
L-Raise	iteration 抛出错误 ξ	进入 Unloading 携带 ξ,后续 L-Unload 应用现有 accumulator
L-Leave	Active 中,target ≠ ω	标记 Unloading 但不应用 inverse,停止提供 coeffect
L-Unload	Unloading 中,¬ relied_n(γ)	应用 accumulator g,进入 Inactive

Provider 与 Consumer 的卸载顺序

【论文原文结论 §4.3.1】这是论文最重要的工程机制之一。base calculus 的 L-Unload 把"移除 provision"和"运行 inverse"放在一起,没有为 consumer 的 teardown 留出区间。如果 provider 直接应用 inverse 释放资源,而 consumer 还在用这个 provider 的依赖,就会出现"数据库连接池被关闭、但事务还没提交"的崩溃。

论文引入 Unloading 中间态和 guard ¬ relied_n(γ)(没有 fiber 再依赖 n)来保证正确顺序:

1. L-Leave:Provider n 标记 Unloading,停止提供 coeffect(其 σ 离开 σ_γ 的 union),但保留自己的 committed view 和 inverse 未动;
2. Consumer m 检测到依赖即将消失(target view 变为 ⊥ 或指向其他 fiber);
3. Consumer m 使用 committed view 中的旧依赖完成清理——因为 σ_γ 只 union Active fiber,Unloading fiber 的绑定对其他 fiber 不可见,但 consumer 自己的 committed view 仍指向它;
4. L-Unload 在 guard ¬ relied_n(γ) 满足时执行——即所有依赖 n 的 consumer 都已 deactivate;
5. Provider n 才执行自己的 inverse 并释放资源。

这种机制解决了:

• 连接池关闭前等连接归还
• 数据库关闭前等事务提交
• Tool Provider 卸载前等正在使用它的 Agent
• 父组件退出时对子组件级联清理

【论文原文结论 §4.4.4 Thm 66】guard 不会死锁:σ_γ 只 union Active fiber,一旦 L-Leave 标记 n,它的 table 离开 σ_γ,没有 target view 能再指向 n,所有 committed 到 n 的 consumer 都被迫进入自己的 teardown,依赖图沿 ≺ 关系向下传递,acyclicity + finite 保证 guard 释放(详见 Progress 定理)。

Inertia:异步加载中依赖变化怎么办

【论文原文结论 §4.3.3】现代 effect 常是异步的(fetch、文件 IO、子 Agent 调用)。一旦 iteration 在飞行中(async Future),它必须 land,不能被 abort。target view 在飞行期间变化时,L-Divert 只能选择"着陆后再 unload"分支,不能"中止 iteration"——因为 iteration 一旦提交到 Future 就无法取消。

三个相关概念:

• Inertia(惯性):飞行中的 transition 句柄,不可取消,只能等待着陆;
• Iteration boundary:L-Divert 介入的粒度——只在 iteration 边界检查 target 变化;
• Partial rollback:已积累的 inverse 被应用、未完成部分被回滚;
• reload 与 unload 相互链接:reload 完成后若 target 已变则链式进入 unload,unload 完成后若 target 已变则链式进入 reload(Algorithm 5)。

这套机制保证了 async 加载组件时不会出现"半旧半新"——要么完成转入 Active,要么经 L-Divert/L-Raise 进入 Unloading 并完全回滚(对应 Resolution Coherence 定理)。

理论与实现对应表

【论文原文结论 §5.1 Table 2】论文形式化概念到 Cordis 实现的映射:

理论概念	Cordis 实现
Unified Context Γ∞	ctx,一等上下文
Revertible Effect	ctx.effect(callback)
Coeffect 注册与访问	ctx.set(key, value) / ctx.get(key)
Component Instantiation	ctx.use(component, config)
Dependency Specification	fiber.inject(即理论 d)
Inverse Accumulator	fiber.dispose
Committed View	fiber.committed
Target View	fiber.target(由 refresh 重算)
Isolation	ctx.isolate(key, realm)
Interception	ctx.intercept(key, metadata)
Inertia	fiber.inertia(飞行中的 transition 句柄)
Lifecycle State	fiber.state(LOADING=Reloading, FAILED=Inactive(ξ))

Fiber 与 React Fiber 的区别

【基于原文的推断】论文 Def 44 把 fiber 定义为组件的一次实例化,携带 (d, p, e, π, σ, τ, θ)——父 fiber、自己的 coeffect 表、retirement 标记、生命周期状态。它与 React Fiber 只是名称类似,概念不同:React Fiber 是 React 内部的 reconciliation 单元,承载组件树遍历状态;Cordis Fiber 是 dynamic composition calculus 中的组件实例,承载 effect accumulator、committed view 和生命周期状态机。两者都借用"fiber"一词的"轻量执行线索"含义,但理论框架完全不同。

下一步看这套机制在元理论上保证了什么:形式化定理的工程翻译。