Undo and Redo

Undo here is a new committed entry, not a rewind, and everything surprising about it follows from that. This chapter is the declaration every change makes about how it comes back, the two arguments that make undo per-person and per-focus, what happens when an undo conflicts with someone else's edit, and why no inverse is ever stored anywhere.

Undo Is a New Entry, Not a Rewind

In most applications, undo is a pointer walking backwards over a stack of past operations. Harmos cannot work that way. The journal is append-only: entries are never deleted, never edited, and positions never renumber. Nothing in the system can move backwards through history, because history is the thing everything else is rebuilt from.

So undo does the only thing it can. It commits a new transaction that puts the state back, and that new transaction is an ordinary entry — checked, applied, sealed, published, and replayed like every other. Pressing Ctrl+Z makes history longer, not shorter.

This looks like a constraint and turns out to be the feature. An undo that rewinds a shared cursor is unsafe the moment two people edit at once. An undo that appends is just another edit, so it composes with everybody else's edits under exactly the rules you already know.

Making a Transaction Undoable

Every change answers the undo question where it is defined, and silence does not compile. There are three answers and no default:

#[harmos::transaction(id = "symbol.move", version = 1, inverse = Self)]
pub struct MoveSymbol { /* … */ }        // its own inverse

#[harmos::transaction(id = "ledger.deposit", version = 1, inverse = Withdraw)]
pub struct Deposit { /* … */ }           // another change takes it back

#[harmos::transaction(id = "symbol.place", version = 1, irreversible)]
pub struct PlaceSymbol { /* … */ }       // it cannot be taken back

One declaration, and — for the first two — one body beside it. The inverse type is not repeated in the body: it is what the attribute already declared.

impl Invert<Schematic> for MoveSymbol {
    /// The inverse carries the handful of bytes it restores — the old place —
    /// and nothing else. It never clones the schematic, and it is read at the
    /// one instant the old place still exists: after `check` passed, before
    /// `apply` runs.
    fn invert(&self, before: &Schematic) -> Self {
        Self {
            symbol: self.symbol,
            to: before.symbol(self.symbol).position,
        }
    }
}

Nothing else registers it. Closing the catalog with #[harmos::transactions] (chapter 3) walks its variants, collects what each one declared, and bakes the resulting table into the value register hands boot. There is no marker on the variant and no second assembly line, because the change already answered.

Three rules hold that table honest, and all three are compile errors:

1. Every change answers. A transaction with neither inverse = … nor irreversible does not compile — the refusal lands on the attribute and says what the three answers are.
2. Pairs are mutual. If Deposit declares inverse = Withdraw, then Withdraw declares inverse = Deposit. inverse = Self is its own pair. The check runs where each change is declared, so a half-declared pair is caught at the definition rather than at a call site.
3. A named inverse is a catalog member. The macro never invents a variant: if Withdraw is not in the catalog that would commit it, closing the catalog says so and tells you to add it.

A change declared irreversible carries no invert body — writing one is the fourth compile error, because there is nothing for it to be the body of.

Three things in that small block are worth naming.

before is the state as it stands before your change. It is the only place in the system where the old position of R1 is still visible, and inverse is called at the only moment it exists — after check has succeeded, before apply runs. Because check already passed, inverse may make the same assumptions apply makes: no defensive lookups, no if let hedging.

The inverse carries what it restores. It does not clone the state, take a snapshot, or keep a reference to anything. It copies the handful of bytes needed to undo this one change into its own payload. A two-field struct is a complete undo for a 200-sheet schematic.

inverse = Self is a convenience, not the rule. It fits when an operation is naturally symmetric — a move back to where it was, a rename back to the name it had. When it is not, the inverse is a different transaction, and the two name each other. An application that decided a connection could be taken back would write it like this:

// Not what the schematic example does — see the next section for the choice
// it made instead.
#[harmos::transaction(id = "net.connect", version = 1, inverse = DisconnectPins)]
pub struct ConnectPins { /* … */ }

impl Invert<Schematic> for ConnectPins {
    fn invert(&self, _before: &Schematic) -> DisconnectPins {
        DisconnectPins { net: self.net, pins: self.pins.clone() }
    }
}

DisconnectPins would be nothing special, and not a kind of thing the undo machinery owns. It would be an ordinary transaction joining the catalog alongside ConnectPins — one more variant in the enum from Chapter 3 — with its own check and apply and the same application error, declaring inverse = ConnectPins in turn, testable with cargo test and no runtime running. That matters for the next section: when undo runs, it is running your code under your rules.

Transactions That Cannot Be Taken Back

Not everything has an inverse, and the deciding sentence is short: an inverse that restores nothing is not an inverse.

Because the inverse must carry what it restores in its own payload, the question is always "what would this have to haul?" For a move, two fields. For a rename, one name. For ReplaceSheet, the entire previous sheet — at which point an application may reasonably decide the operation is a place where history stops rather than pay that on every commit. An application may also decide, for its own reasons, that a step simply is not undoable. Both decisions are spelled the same way, and spelled out loud: irreversible, in the change's own attribute.

The schematic example makes that decision twice, and both times because the inverse would have to answer a question the editor declines to answer. PlaceSymbol is irreversible, because taking a placement back means deciding what happens to every net that has since connected to its pins — and an inverse that restores only half of that is not an inverse. ConnectPins is irreversible for the same reason one level along: the inverse would have to know whether this connection created the net, and whether taking the pins off should take the net with them.

The consequence is precise. An entry whose transaction is irreversible is a barrier. Within its focus, undo does not cross it — it will not reach behind that entry to find an older one it likes better.

A Barrier Halts Undo Within Its Focus

The walk visits the requesting principal's own entries newest-first, skips the ones the focus you passed does not admit, and stops at the first admitted entry carrying no inverse — the answer there is Error::NothingToUndo. A barrier the focus excludes blocks nothing: your irreversible entry in one document never freezes undo in another, which is the point of passing a focus at all.

Guarding against cross-focus interference is not the barrier's job. Every inverse runs its ordinary check against current state, and an undo whose ground has shifted — whatever focus shifted it — is refused with your typed conflict rather than applied. Commit order still matters within a focus: place an irreversible entry above the one you want undoable in the same focus, and undo stops at it. Somebody else's barrier is never in your way, because the walk never visits their entries at all.

Do Not Fake an Inverse

The tempting fix when Ctrl+Z starts erroring is a no-op invert that returns something harmless. Do not. It appends a real, durable entry announcing that a change was undone while the state still contains it, and the undo fold below will then treat the original as inactive — so the next Ctrl+Z skips a change the user can still see on screen. An honest refusal is a better application than a lie in the history.

Undoing

let receipt = handle.undo(alice(), Focus::all()).await?;

Two arguments, and both are load-bearing.

The Principal: Undo Is Per Person

Undo selects the requesting principal's latest still-active entry. Alice's Ctrl+Z never touches Bob's rename, even when Bob's rename is the most recent thing in the entire journal. Nothing was configured to make that true; it is what the selection rule says.

On a single-user desktop this is invisible. The moment two people share a runtime — or one person and a guest, or a user and a background service — it is the difference between undo and sabotage.

The Focus: Undo Is Per Whatever You Say

pub struct Focus<A: Application> {
    predicate: Option<Arc<dyn Fn(&A::Transaction) -> bool + Send + Sync>>,
}

impl<A: Application> Focus<A> {
    /// Considers every one of the requesting principal's entries.
    pub fn all() -> Self;

    /// Considers only the entries whose transaction the predicate accepts.
    pub fn matching(predicate: impl Fn(&A::Transaction) -> bool + Send + Sync + 'static) -> Self;
}

The field is private and there is nothing else in the struct: a focus is one optional predicate, shared behind an Arc so it can be cloned into the writer along with the request. Focus::all() considers every one of your entries. Focus::matching narrows by that predicate — and look carefully at what the predicate receives. It is &A::Transaction: the catalog enum from Chapter 3, holding the payload your application declared. It is never the metadata the runtime witnessed.

So the predicate is a method you write on your own catalog, dispatching across its variants. The schematic example narrows undo to one symbol's own edits:

impl Transaction {
    /// Which symbol an edit is about, when it is about one.
    pub fn symbol(&self) -> Option<SymbolId> {
        match self {
            Self::PlaceSymbol(change) => Some(change.symbol),
            Self::MoveSymbol(change) => Some(change.symbol),
            Self::ConnectPins(_) | Self::RenameNet(_) => None,
        }
    }
}

/// Undo and redo only what alice did to one symbol.
fn only(symbol: SymbolId) -> Focus<SchematicEditor> {
    Focus::matching(move |change: &Transaction| change.symbol() == Some(symbol))
}

let receipt = handle.undo(alice(), only(R1)).await?;

In the transcript that call walks past a rename of a net — outside the focus, so not a candidate — and takes the move of R1 underneath it. The rename stands untouched.

Note where the grouping key had to live for this to work: in the payload, on every transaction that belongs to the group. Metadata carries no application vocabulary, so a symbol id could never have gone there. Witness and declare, from Chapter 4, is what makes scoping possible at all.

The same shape scales one level up. An editor keeping several sheets open in one runtime carries a document id in every transaction's payload and focuses on that instead, which gives each open sheet its own undo history from one runtime and one journal. It is a modelling decision made up front, when the transactions were designed, rather than retrofitted the day somebody asks for per-sheet undo.

One more property, easy to miss and worth stating flatly: one call undoes one entry. Focus narrows the candidates; it does not batch them. Five commits take five undo calls. If a user gesture should be one undo, make it one transaction — Chapter 2's atomicity rule pays for itself here.

Redo is the mirror image: journal.redo(principal, focus) re-applies the forward transaction of the thing you most recently undid within that focus.

And redo has a lifespan: your next ordinary commit ends it. The moment you commit a new forward change, your undone entries stop being redoable — the present has diverged from the future they would restore, and redoing onto it would be a lie. This is the behavior every editor has taught your hands already: type after an undo and Ctrl+Y goes quiet. The truncation is personal, like everything else here — someone else's commit never empties your redo, because their divergence is guarded the usual way: your redo re-checks against current state and refuses honestly if the world moved on.

Asking Without Pressing

A toolbar has to know whether its two buttons are live, and finding out by provoking a refusal would be a commit nobody asked for. reversals is the read beside the two verbs: it walks the very fold undo and redo select through, appends nothing, and answers both halves at once, so a drawn button and the verb behind it cannot disagree about what exists. It obeys the same two rules they do — per principal, per focus — including the barrier, so a principal whose latest in-focus change declared itself irreversible reads back undoable: false. The answer is At-stamped like every other read, which is how a view that has fallen behind tells a stale enabled button from a fresh one. What true does not promise is that the press will succeed: the inverse still runs its own check against current state, so the flag says the history is there and the next section says whether it still fits.

let At { value, position } = handle.reversals(alice(), Focus::all()).await?;

let Reversals { undoable, redoable } = value;

Conflicts: Undo Is Allowed to Refuse

The inverse is a transaction, so it goes through the ordinary pipeline — which means it runs its ordinary check, against the current state, not against the state it was derived from. There are exactly two outcomes:

• The check passes. The inverse is applied and appended as a new entry carrying link = Some(Link::UndoOf(original)), and you get a Receipt like any other commit.
• The check refuses. Nothing is appended and nothing is mutated, and undo returns Error::UndoConflict(e) carrying your own typed error.

Worked through: Alice renames net 1 from N$1 to VCC. Bob then renames net 2 to N$1 — the name Alice's net just gave up. Alice presses Ctrl+Z. The inverse is "rename net 1 back to N$1"; its check asks whether that name is free; it is not, because Bob is using it; Alice gets Error::UndoConflict(SchematicError::NameTaken("N$1")) and the journal is exactly as it was a moment before.

That refusal is the whole design working. The alternative — forcing the inverse — would leave two nets answering to one name, in a document where the editor's own rules say that cannot happen. Independent edits compose; conflicting edits fail safely, atomically, and with an error your own domain wrote.

Correlation Does Not Select What Is Undoable

A five-step wizard may share one CorrelationId across its commits. That is what correlation is for, and it is not what undo uses. A correlation links a causal workflow that may span transactions, records, jobs, and services — and records and jobs have no inverses, because they change no state. "Undo the correlation" is not an operation the journal can define.

Reversing an arbitrary causal family is compensation: it is best-effort, it is your application's business, and it is never called undo.

Under the Hood: Capture in the Pipeline, and the Fold

Chapter 4's pipeline had a stage we passed over:

… → check → optional inverse capture → apply → seal → publish → reply

Capture sits exactly there because that is the only instant with both properties it needs: check has succeeded, so the inverse may assume a valid world, and apply has not run, so the pre-state still exists.

Now the part that surprises everyone.

Inverses Are Never Stored

Envelope<P> — the shape entries take at the storage boundary — has no inverse field, and Kind has no inverse variant. Nothing in any file harmos writes holds an inverse. Anywhere.

They do not need to be stored, because replay regenerates them for free. Replay applies entries in order, so when it reaches entry 300 the state is precisely what it was when entry 300 was first committed. Calling invert(self, before) there is the same function on the same two inputs, so it returns the same result. This is why invert carries the same purity rule as apply: no clock, no randomness, no I/O, a deterministic function of (self, before) and nothing else. Determinism is what buys the storage saving.

And there is a stronger reason than saving bytes. A stored inverse would be a second copy of undo truth, sitting beside the entries it was derived from and free to disagree with them — after a bug fix, after an evolution, after a partial write. Harmos's razor is that anything rebuildable by folding the entry order is a cache and never truth.

The Undo Stack Is a Fold

Which is exactly what the undo stack is. There is no undo stack structure anywhere in the runtime. What exists is the entry order plus one optional field on each entry's metadata:

pub enum Link {
    /// This entry reverses the entry at the linked position.
    UndoOf(Position),
    /// This entry re-applies the entry at the linked position.
    RedoOf(Position),
}

Fold the order over those links and the stack appears. An ordinary entry makes its own position a candidate for its principal. An entry linked UndoOf(p) marks p inactive. An entry linked RedoOf(p) marks p active again. "The requesting principal's latest still-active entry within the focus" is a question asked of that fold, and there is nothing else to consult.

Five entries, two people:

300  Alice  MoveSymbol   R1 → (10, 45)   link: —
301  Bob    RenameNet    net 1 → VCC     link: —
302  Alice  RenameNet    net 2 → GND     link: —
303  Alice  RenameNet    net 2 → N$2     link: UndoOf(302)   ← Alice pressed Ctrl+Z
304  Alice  RenameNet    net 2 → GND     link: RedoOf(302)   ← Alice pressed Ctrl+Y

After 303, Alice's still-active entries are {300} — 302 is marked undone, and 301 was never hers to begin with. Bob's {301} is untouched; his rename is not in Alice's undo path and never was. After 304, 302 is active again.

Note what 303 and 304 are: ordinary renames, carrying ordinary payloads. The only thing that makes them an undo and a redo is the link the writer witnessed on them, and the link names the entry they answer — 302 both times, never each other.

Every one of those five is a real, durable, replayable entry. Nothing was deleted, nothing was rewritten, and position 302 still says today exactly what it said when it was sealed. Nothing in the system is allowed to treat the derived stack as authoritative, so a crash costs nothing: recovery replays the same links and folds the same stack back into existence.

Why This Matters

Per-user, per-focus undo is a primitive here, not a feature you build. The selection is a fold over links harmos already replays, and the inverse is an ordinary transaction that your own check already validates. Two people editing one document each get their own undo history; a conflict comes back as a typed domain error instead of a corrupted document; and none of it needs a byte of extra storage, because the inverses are re-derived rather than saved.

Test Your Knowledge

1. A colleague proposes storing each inverse in its entry: “then undo after a restart doesn't have to recompute anything, and it's faster.” Find the objection that survives even if the performance claim were true.

The performance claim is mostly false, but that is the weaker argument. Recovery already walks every pre-state — that is what replay is — so re-deriving an inverse costs one pure function call at a point the runtime is already standing. There is no seek, no extra pass, and no state to reconstruct specially.

The objection that survives is the fold test. Anything rebuildable by folding the entry order is a cache and is never truth. A stored inverse would be a second, independent copy of undo truth sitting beside the entry it was derived from — and two copies of a truth can disagree. They disagree after a bug is fixed in inverse, after a partial write, after an evolution that changes what the payload means. At that moment the system has to choose which one is real, and there is no principled answer. Re-derivation cannot disagree with the entries, because it is the entries.

This is why Envelope<P> has no inverse field and Kind has no inverse variant: the absence is the design, and it is testable.

2. A teammate reasons: “Chapter 2 says check never runs during replay, because history is settled. Undo replays an old entry backwards. So undo must not run check either — otherwise a rule we tightened in v2 could veto the undo of a v1 entry.” Untangle it.

The premise is misapplied, and the conclusion would destroy the safety property undo depends on.

"History is settled" means an already accepted entry is never re-validated when history is rebuilt. Replay calls only apply, on entries that were checked at the moment they were committed, under the rules of that moment.

An undo is not a replay. It is a new commit, entering the writer pipeline at the head, in the present. Its transaction — the inverse — has never been checked by anyone, because it did not exist until now. So it is checked exactly once, at commit time, like every other transaction. The rule was never "checks stop running"; it was "checks govern the future only". The undo is the future.

And that check is not an inconvenience to route around — it is where conflict detection lives. It runs against the current state, not the state the original was committed against, which is precisely how harmos notices that the world moved on. Skip it and undo becomes a blind overwrite: resurrected symbols, dangling net references, other people's work silently reverted.

On the v2 worry specifically: yes, a tightened v2 rule can refuse an undo that v1 would have allowed, and that is correct. The undo produces a new state, right now, which must satisfy today's invariants. What v2 can never do is invalidate the entry at position 300 — that one is settled and still replays.

3. Alice renames net 1 from N$1 to VCC at 300, Bob renames net 2 to N$1 at 301, Alice moves R1 at 302. Alice presses Ctrl+Z twice. Describe both results exactly — and say what happens on a third press.

First press. Undo selects Alice's latest still-active entry: 302. Bob's 301 is not a candidate and never was — selection is per principal. The inverse of the move is the move back; its check asks whether R1 is placed, it is, so the inverse is applied and appended at 303 with link = UndoOf(302). Alice gets a Receipt for 303. Notice that the undo lands at the head of history, above Bob's edit, rather than being woven in beside 302.

Second press. The fold now shows 302 inactive, so Alice's latest still-active entry is 300. Its inverse is "rename net 1 back to N$1". That inverse's check asks whether N$1 is free — and Bob took it at 301. The check refuses with the editor's own typed error, so undo appends nothing, mutates nothing, and returns Error::UndoConflict(SchematicError::NameTaken("N$1")). The state still has her move-back from 303. Nothing is half-done.

Third press. The same conflict, again. A conflict is a fact about the current state, not a strike counter — it is stable until the world changes. If Bob renames net 2 to something else, the same undo would then succeed. The right response in the UI is to tell Alice why ("another net is already called N$1"), which you can do precisely, because the error came from your own domain rather than from the framework.

One thing this walk depends on: every one of Alice's entries between the head and 300 carries an inverse. Had she connected some pins at 301 instead of Bob renaming a net, that connection — declared irreversible — would be a barrier of her own, the walk would stop there, and both presses would answer NothingToUndo.

4. Product wants a “cancel setup” button: the five commits of a placement wizard already share one CorrelationId, so the request is “just undo that correlation”. What do you tell them, and what do you build?

Correlation never selects what is undoable. It links a wider causal workflow, and that workflow may include records, jobs, and services — none of which have inverses, because none of them change state. "Undo the correlation" is not an operation the journal can define.

Undo is also one entry per call. Even with a focus that matched exactly those five transactions, undo selects the principal's latest still-active entry in the focus and appends one inverse. Five entries would mean five calls, each of which can independently conflict — which is honest, but it is not the single atomic "cancel" the button promises.

Two real options, and choosing between them is a modelling decision, not a workaround:

• Make it one transaction. If cancelling must be one undoable unit, then placing must have been one unit too. One transaction carrying the whole placement in its payload gives you one entry, one inverse, one Ctrl+Z. This is Chapter 2's atomicity rule arriving with a bill.
• Write compensation. Commit new transactions that undo the effect at the domain level, with your own rules about what happens when the world has moved on. That is a legitimate application feature — it is just not undo, and calling it undo in the code will mislead the next reader.