Revertible Effects：時間次元の副作用ロールバック
本論文は Revertible Effects で temporal composability を解決する——コンポーネントが除去される際、環境に対して行った変更は完全かつ安全にロールバックされなければならない。中核思想：すべての effect は inverse（逆操作）を携え、ランタイムはすべての inverse を単一の累算器に複合し、アンロード時に LIFO 順で適用する。
Effect の型
[論文原文の結論 §3.1] 本論文は effect を型 Γ → Γ × (Γ → Γ) としてモデル化する：現在のコンテキストに作用し、変更後のコンテキストと inverse 関数を返す。Effect context は ∂Γ ≔ Γ × (Γ → Γ) と定義され、第一成分が現在の状態、第二成分が累算器——すなわち「それまでのすべての 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）、回復は 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 を親コンテキストの累算器に複合する。
- 複数の逆操作の複合：
disposeは親コンテキストのctx.disposeに prepend されるため、子 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 |
Witness 条件 g(δ)=γ | 開発者の義務、ランタイムは検証しない |
LIFO 複合 ⋄ | track は monoid homomorphism（Thm 5） |
Revertible Effects は「ロールバック」を解決する——しかしコンポーネントは「依存変化への応答」もできなければならない。後者は Reactive Coeffects が解決する。