Chapter 4

Revertible effects — undo as a value

The question this chapter answers: when a plugin is removed, how do we undo everything it did — completely, in the right order, and without the plugin author writing an uninstall routine? The paper's answer is that every effect should hand back its own undo, and the runtime should keep those undos. The rest is working out what "keep" has to mean for that to be sound.

4.1 An undo is a stored function

Any impure function f : X ⇝ Y can be read as a pure one if you make the world an explicit argument: f : Γ × X → Γ × Y. Fix the input and look only at what happens to the world: you get a map Γ → Γ. That map is the effect. "Register route /stats" is a function from worlds-without-the-route to worlds-with-it.

To make an effect undoable, pair it with a second function g : Γ → Γ that takes the world back. Undoing is one-sided: we require g ∘ f = id ("do, then undo, lands where you started") and say nothing about f ∘ g ("undo, then redo" need not give the identical world — the redone route may get a fresh internal id).

If you do two effects and want to undo both, you undo the second first. Written as a rule on pairs:

// twisted composition, in code
const seq = ([f1, g1], [f2, g2]) => [x => f1(f2(x)), x => g2(g1(x))]

4.2 The undo stack: state + accumulator

A runtime that tracks effects needs to carry, alongside the world, the composite of every undo so far. The paper packages the two together:

Two operations move this pair:

track(f, g)(γ, φ) = (f(γ), φ ∘ g)        recover(γ, φ) = (φ(γ), id)

In words: track applies the effect to the world and pushes its undo onto the front of the accumulator (front, because φ ∘ g runs g first). recover runs the whole accumulator and resets it.

let world = γ0, undoAll = id
function track(f, g) { world = f(world); const prev = undoAll; undoAll = x => prev(g(x)) }
function recover()   { world = undoAll(world); undoAll = id }

Three short theorems say this bookkeeping is sound. Each is one sentence in the running example:

• Thm 4 (pr₁ ∘ track(f,g) = f ∘ pr₁): tracking changes nothing about what the route registration does; it only records the undo on the side.
• Thm 5 (track respects sequencing): tracking the route, then the timer, then the roster one at a time is the same as tracking the three-step composite once. So we may reason about a plugin's whole load as one effect.
• Thm 7 (if g(f(γ)) = γ then recover(track(f,g)(γ,φ)) = recover(γ,φ)): after tracking an effect whose undo works, "recover" still lands at the same place it would have before. The quantity φ(γ) — "where recover would take us" — never moves. The paper names φ(γ) = γ₀ the soundness invariant; it is the thing every later result protects.

4.3 The undo must be produced when the effect runs

Look at the roster step. To remove stats from the roster you need to know which entry is yours — and the entry's id is only known after you add it. So the undo cannot be written down before the effect runs; it has to be returned by the effect, closing over what the effect learned. Def 3's track(f, g) fixed g in advance and required it to work at every world; the fix reshapes the effect so the undo comes out with the result:

// an effect function: world in, (world, undo) out
const addToRoster = (name) => (γ) => {
  const id = γ.roster.add(name)                  // learned only now
  return [γ, (γ2) => { γ2.roster.remove(id); return γ2 }]
}

Since effect functions return pairs, you cannot compose them with plain ∘; the paper defines the composition that threads the world through and twists the undos:

One more idea, which you can skim on first read. The paper "lifts" an effect function so it acts on the effect context (world + accumulator) instead of the bare world — effect : 𝔈Γ → 𝔈∂Γ, Def 12. The interesting part is what the lifted version returns as its undo: track(g, pr₁∘e). Read that as: undoing is itself an effect, and the way to undo an undo is to redo. Thm 15 checks it: the world is restored exactly; the accumulator is restored exactly only if g ∘ f = id globally; but in every case the soundness invariant holds — and that is all recovery needs.

4.4 A plugin loads by a sequence of effects: iterators are generators

stats did three things, each with its own undo. The natural shape is a generator: run a step, yield its undo, run the next. The paper reifies that shape as a type:

ctx.effect(function* () {
  const route = ctx.http.route('/stats', handler)
  yield () => route.remove()               // undo 1
  const timer = setInterval(tick, 1000)
  yield () => clearInterval(timer)         // undo 2   (runs before undo 1)
  const id = ctx.roster.add('stats')
  yield () => ctx.roster.remove(id)        // undo 3   (runs first of all)
})

Thm 16 is the guarantee for one plugin: apply the steps in order, undo them in reverse order, and every undo meets exactly the world its own step produced, with the soundness invariant holding throughout. A plain effect function is the degenerate iterator that is done after one step.

4.5 What is guaranteed here, and what is not