Revertible Effects:时间维度的副作用撤销
论文用 Revertible Effects 解决 temporal composability——组件被移除时,它对环境做的修改必须被完全且安全地撤销。核心思想:每个 effect 必须携带一个 inverse(逆操作),运行时把所有 inverse 复合到一个累加器里,卸载时按 LIFO 顺序应用。
Effect 的类型
【论文原文结论 §3.1】论文把 effect 建模为类型 Γ → Γ × (Γ → Γ):作用于当前上下文,返回修改后的上下文以及一个 inverse 函数。Effect context 定义为 ∂Γ ≔ Γ × (Γ → Γ),其中第一分量是当前状态,第二分量是 accumulator——即"迄今所有 effect 的 inverse 复合",是把上下文恢复到初始状态的函数。
论文 §3.1.1 Def 3 给出 trackΓ:把 (f, g) 映射为 ∂Γ → ∂Γ,对状态 (γ, φ) 产出 (f(γ), φ ∘ g)——前向应用 f,把 inverse g 复合到累加器。Thm 7 证明 recover(track(f,g)(γ,φ)) = recover(γ,φ),即"跟踪后恢复等价于不跟踪直接恢复"。
【论文原文结论 §3.1.2】论文增强模型,让 inverse 在 effect 应用点由调用者按当前状态给出(𝔈Γ ≔ Γ → Γ × (Γ → Γ)),并要求 witness 条件 g(δ) = γ(Def 8)——即 inverse 应用到 effect 后的状态必须恢复到 effect 前的状态。多个 effect 通过 ⋄ 组合(Def 9),track 是 monoid homomorphism(Thm 5),recovery 在 LIFO 顺序下精确(Thm 15、Thm 16)。
ctx.effect:Cordis 的 API 对应
对应 Cordis §5.1.1 的 ctx.effect,TypeScript 伪代码:
ctx.effect(() => {
const resource = acquire()
return () => {
release(resource)
}
})ctx.effect 接收一个函数,该函数执行前向 effect(获取资源)并返回一个 cleanup 函数(释放资源)。运行时把 cleanup 复合到父 context 的累加器上。
- 多个逆操作的组合:
dispose被 prepend 到父 context 的ctx.dispose,因此子 effect 的 inverse 实际上是父上的一个 effect(对应∂²Γ的递归结构)。开发者只需为每个原子 effect 写 inverse,复合 inverse 由⋄自动派生。 - LIFO 顺序:Algorithm 1 的
inverse ← value ∘ inverse,新 inverse 复合在前面,卸载时按相反顺序应用。后注册的 effect 先撤销,符合"后进先出"的资源生命周期直觉。 - 与 React useEffect cleanup、RAII、事务回滚的异同:【论文原文结论 §7.3】React useEffect 把 effect 与 cleanup 结构化配对,但 hook 不能在条件/循环/嵌套函数里调用,effect body 不接受 async 或迭代器,无法从已有 effect 组合出复合 inverse;RAII/线性类型把 reversal 限定在词法区域;STM 把回滚限定在事务内;Cordis 的 effect 是普通操作,自由组合、可异步、只需为每个原子 effect 写 inverse,复合 inverse 由组合自动派生。
ctx.effect 不验证 inverse 正确性
【论文原文结论 §3.1.3】ctx.effect 只负责跟踪 inverse,不会自动证明 inverse 一定正确。Witness 条件 g(δ) = γ 是开发者义务而非运行时验证。如果 inverse 写错(比如释放了错误的资源、或 inverse 的副作用与 effect 不对称),恢复会失败或污染状态,运行时不负责。
独立性(Def 19)要求两个 effect 的变换 monoid 彼此交换,且互不扰动对方的 inverse——这是把单组件的 LIFO 推广到多组件交错序列的前提(Cor 21)。非交换的 effect(比如有序操作链)需要通过 coeffect 排序来保证可恢复性。
这一节的核心
| 理论概念 | Cordis 实现 |
|---|---|
| Unified Context Γ∞ | ctx,一等上下文 |
| Revertible Effect | ctx.effect(callback) |
| Inverse Accumulator | fiber.dispose |
见证条件 g(δ)=γ | 开发者义务,运行时不验证 |
LIFO 组合 ⋄ | track 是 monoid homomorphism(Thm 5) |
Revertible Effects 解决了"撤销"——但组件还要能"响应依赖变化"。后者由 Reactive Coeffects 解决。