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 解決。