Specifying error behavior

The stack chapter left a loose thread: what is top(empty)? Algae has no partial functions — top is total, so top(empty) is some element, we just never said which. That’s a real gap. A caller who pops one element too many deserves a defined answer, not a shrug.

Algae’s motto is failure is modeled with sum types. So we give pop and top a second possible outcome — an Error — and specify the empty case outright:

sort Error : Sort;

op err : → Error;
op pop : Stack(A) → Stack(A) | Error;
op top : Stack(A) → A | Error;

axiom pop_empty(A : Sort)  ⊢ pop(empty) = err;
axiom top_empty(A : Sort)  ⊢ top(empty) = err;

The return types are now sum types: pop yields “a stack or an error,” written Stack(A) | Error. Two things make this fit together:

  • pop(empty) = err type-checks because a value of a summand injects into the sum: err : Error sits happily where a Stack(A) | Error is wanted.

  • The old success laws survive untouched, for the same reason. pop(push(x, s)) = s still holds — s : Stack(A) injects into Stack(A) | Error — it just now reads as “on success, you get s back.” Nothing we proved before breaks.

Here’s the whole thing, error-aware, still verifying:

import core(rewrite_r);

sort Stack : Sort → Sort;
sort Error : Sort;

op empty : → Stack(A);
op push  : A * Stack(A) → Stack(A);
op err   : → Error;
op pop   : Stack(A) → Stack(A) | Error;
op top   : Stack(A) → A | Error;

axiom top_push(A : Sort, x : A, s : Stack(A))  ⊢ top(push(x, s)) = x;
axiom pop_push(A : Sort, x : A, s : Stack(A))  ⊢ pop(push(x, s)) = s;
axiom pop_empty(A : Sort)  ⊢ pop(empty) = err;
axiom top_empty(A : Sort)  ⊢ top(empty) = err;

# empty is now fully specified: peeking it is an error, not a mystery.
lemma peek_empty(A : Sort)  ⊢ top(empty) = err;
proof
  by top_empty(A);
qed;

# the success laws still hold — an A injects into A | Error.
lemma top_of_push(A : Sort, x : A, s : Stack(A))  ⊢ top(push(x, s)) = x;
proof
  by top_push(A, x, s);
qed;

# push one, pop it, then peek: the error surfaces through the composition.
lemma push_pop_peek(A : Sort, a : A)  ⊢ top(pop(push(a, empty))) = err;
proof
  by rewrite_r(Stack(A), pop(push(a, empty)), empty,
               pop_push(A, a, empty), top(_) = err)
  then ⊢ top(empty) = err;
  by top_empty(A);
qed;

  • ``peek_empty`` is the point of the whole exercise: top(empty) now has an answer, err, provable in one step. The gap is closed.

  • ``top_of_push`` confirms nothing regressed — the success law is exactly as before.

  • ``push_pop_peek`` chains operations: push a, pop it back to empty, then peek — and the error propagates out. We rewrite pop(push(a, empty)) to empty and finish with top_empty.

The tradeoff

Specifying errors this way buys you totality and honesty: there are no undefined corners left, pop(empty) genuinely equals err, and any caller can tell success from failure by looking at which side of the sum they got.

But you pay for it. Once pop returns Stack(A) | Error, that error rides along through every composition. push_pop_peek only went through because the inner pop demonstrably succeeded (it produced empty, a real stack) — so the injection carried us past it. Feed a genuinely-might-be-error result into the next operation and a rigorous spec has to case-split: if it errored, propagate; otherwise carry on. The tidy equations start sprouting side conditions, and pop(pop(s)) stops being something you can write without first asking “did the first pop fail?”

That’s the perennial bargain. Leave failure unspecified and the algebra stays clean but the spec lies by omission. Track it in the types and the spec tells the whole truth, but the plumbing multiplies. For a stack — where popping too far is an everyday mistake — paying for honesty is usually worth it. For an operation you can prove never fails, the sum type is just noise you’ll spend proofs peeling back off. Choosing where to draw that line is a real part of writing a specification.