Revertible Effects: temporal side-effect rollback

论文版本948a07b (main)

The paper uses Revertible Effects to solve temporal composability — when a component is removed, every modification it made to the environment must be completely and safely reverted. The core idea: every effect must carry an inverse (the reverse operation), the runtime composes all inverses into a single accumulator, and at unload time they are applied in LIFO order.

The type of an Effect

[Paper's original conclusion §3.1] The paper models an effect as the type Γ → Γ × (Γ → Γ): it acts on the current context and returns the modified context along with an inverse function. The effect context is defined as ∂Γ ≔ Γ × (Γ → Γ), where the first component is the current state and the second component is the accumulator — i.e. "the composite of the inverses of all effects so far", a function that restores the context to its initial state.

The paper §3.1.1 Def 3 gives trackΓ: it maps (f, g) to ∂Γ → ∂Γ, producing for state (γ, φ) the value (f(γ), φ ∘ g) — apply f forward and compose inverse g into the accumulator. Thm 7 proves that recover(track(f,g)(γ,φ)) = recover(γ,φ), i.e. "recovering after tracking is equivalent to recovering directly without tracking".

[Paper's original conclusion §3.1.2] The paper strengthens the model so that the inverse is supplied by the caller at the point of effect application, based on the current state (𝔈Γ ≔ Γ → Γ × (Γ → Γ)), and requires the witness condition g(δ) = γ (Def 8) — i.e. applying the inverse to the post-effect state must restore the pre-effect state. Multiple effects compose through ⋄ (Def 9), track is a monoid homomorphism (Thm 5), and recovery is exact under LIFO order (Thm 15, Thm 16).

ctx.effect: the Cordis API correspondence

This corresponds to ctx.effect in Cordis §5.1.1; TypeScript pseudocode:

ctx.effect(() => {
  const resource = acquire()
  return () => {
    release(resource)
  }
})

ctx.effect takes a function that performs the forward effect (acquire a resource) and returns a cleanup function (release the resource). The runtime composes the cleanup onto the parent context's accumulator.

• Composition of multiple inverses: dispose is prepended to the parent context's ctx.dispose, so the child effect's inverse is effectively an effect on the parent (corresponding to the recursive structure of ∂²Γ). Developers only need to write inverses for atomic effects; the composite inverse is derived automatically via ⋄.
• LIFO order: Algorithm 1's inverse ← value ∘ inverse composes the new inverse at the front, and at unload time the inverses are applied in reverse order. Effects registered later are reverted first, matching the "last-in-first-out" intuition about resource lifecycles.
• Comparison with React useEffect cleanup, RAII, and transaction rollback: [Paper's original conclusion §7.3] React useEffect structurally pairs effect with cleanup, but hooks cannot be called inside conditions/loops/nested functions, the effect body does not accept async functions or iterators, and a composite inverse cannot be composed from existing effects; RAII / linear types confine reversal to a lexical region; STM confines rollback to within a transaction; Cordis's effects are ordinary operations, freely composable, may be async, and only require writing inverses for each atomic effect — the composite inverse is derived automatically through composition.

ctx.effect does not verify inverse correctness

[Paper's original conclusion §3.1.3] ctx.effect only tracks inverses; it does not automatically prove that an inverse is correct. The witness condition g(δ) = γ is a developer obligation, not a runtime verification. If an inverse is written incorrectly (e.g. it releases the wrong resource, or the inverse's side effect is asymmetric with the effect), recovery will fail or pollute state, and the runtime is not responsible.

Independence (Def 19) requires that the transformation monoids of two effects commute with each other and that they do not disturb each other's inverse — this is the precondition for generalizing a single component's LIFO to interleaved multi-component sequences (Cor 21). Non-commutative effects (e.g. an ordered operation chain) require coeffect-based ordering to guarantee recoverability.

Core of this section

Theoretical concept	Cordis implementation
Unified Context Γ∞	ctx, first-class context
Revertible Effect	ctx.effect(callback)
Inverse Accumulator	fiber.dispose
Witness condition g(δ)=γ	Developer obligation, not verified by runtime
LIFO composition ⋄	track is a monoid homomorphism (Thm 5)

Revertible Effects solve "reverting" — but components must also "respond to dependency changes". The latter is solved by Reactive Coeffects.