effect-systemrevertibledynamic-compositiontype-theoryeffect-tracking

Revertible Effects (可撤销效应)

在 Spatiotemporal Composability (时空可组合性 范式中，每个 effect 都必须携带一个显式 inverse；runtime 自动追踪这些 inverse 并在组件卸载时LIFO 撤销——把"卸载后环境恢复到加载前状态"做成结构性保证。Shi, Zhang & Cui (2026) Section 3.1 的核心构造。

形式化定义

Effect 上下文

\partial\Gamma \;:=\; \Gamma \times (\Gamma \to \Gamma) 二元组 (\gamma, \varphi)：当前 context state \gamma + 累加器 (accumulator) \varphi，后者是迄今为止执行的所有 effect 的 inverse 的复合——只要对它求值，就能从任意当前 state 恢复初始 state。 ### Track 操作 \mathrm{track}_\Gamma(f, g) : (\gamma, \varphi) \mapsto (f(\gamma),\ \varphi \circ g)

  • f：前向 effect
  • g：candidate inverse（左逆，g \circ f = \mathrm{id}_\Gamma）
  • 累加器从右往左复合 inverse（LIFO 撤销）

Theorem 4 \mathrm{pr}_1 \circ \mathrm{track}_\Gamma(f,g) = f \circ \mathrm{pr}_1——前向 effect 在 state 投影上正确传递。

Theorem 5 \mathrm{track}_\Gamma 是 twisted 复合幺半群 \mathbb{T}_\Gamma 到 \partial\Gamma \to \partial\Gamma 的幺半群同态——inverse 的复合性是结构性质。

Twisted 复合

(f_1, g_1) \circ (f_2, g_2) \;:=\; (f_1 \circ f_2,\ g_2 \circ g_1)

注意 inverse 在右操作数先复合——复合顺序与撤销顺序相反。

与 classical effect 体系的关系

Classical effect system (Lucassen-Gifford, Moggi, Plotkin-Power) Revertible effect
Effect 描述 类型注解 / algebra / handler 值（pair f, g）
推理时机 编译期 运行时
Inverse 无 结构保证——由 track 同态自动派生
作用域 词法 动态（runtime 加载/卸载）
状态恢复 RAII / bracket（词法退出） LIFO 累加器（动态退出）

独立性条件（Definition 19 / Theorem 42）

为让 effect 的累加器 LIFO 撤销不必保持原始执行顺序——即两个 effect 顺序无关——论文要求 effect 函数独立 (independent)：

  • Clause 1：effect f 的 transformations 与 g 的 commutation（即与 \mathbb{M}(f) 的每个生成元 commutation）。
  • Clause 2：f 的 transformations 不扰动 g 的 outcome（反之亦然）。

Theorem 42：若 e_1, e_2 涉及的 key 上操作可交换，则 e_1, e_2 独立。

一个 key 若是"独立添加/移除条目的表"（路由表、事件监听器表）——commutative；若是"有序链"（middleware 链）——不 commutative，中间件 A 插在 B 之前的请求与 A 在 B 之后看到的请求不同。

在 Cordis 中的实现

ctx.effect(async (config) => {
  // 前向 effect
  const conn = await openConnection(config.url)
  ctx.set('db', conn)
  // 返回 inverse
  return async () => {
    await conn.close()
  }
})

卸载时 runtime 自动 LIFO 调 inverse；如果有提供 \mathrm{relied}_n(\gamma) 守卫（Section 4.3.1），会先等所有依赖者完成自己的 deactivation 再执行。

与 quant 系统的潜在接口

策略/执行系统中的 side-effect 通常是有状态的、长时间持有的：

  • 开仓 → 持仓效应；inverse = 平仓。
  • 注册数据订阅 → callback 注册；inverse = 退订。
  • 修改 risk limit → 状态变更；inverse = 还原 limit。

把每条 side-effect 显式建模为 (f, g) pair，runtime 自动追踪与撤销，等价于给策略系统装上"安全卸载"——避免"删除策略模块但持仓未平"的常见事故。详见 Spatiotemporal Composability (时空可组合性 页中标注的迁移接口。

引用本页