Exceptions and Handlers

Most control flow is polite: a function is called, it computes, it returns, and control resumes right where it left off. Exceptions are the impolite kind. A raise deep inside a call abandons the current computation entirely, tears down the stack frame by frame, and lands at the nearest enclosing handle — possibly many calls up. This non-local jump is exactly what you want when something has gone wrong ten layers deep and there is nothing sensible for the intervening layers to do but get out of the way.

To model it rigorously we need an operational semantics in which an exception propagates: a rule that says "if a subterm raises, so does the whole term," unwinding until a handler stops it. We also need a typing discipline, and here lies a genuinely surprising design decision — raise e can be given any type at all, because it never returns a value of that type. That single choice is what lets exceptions slot into an otherwise ordinary type system, and it is also why the type system, on its own, tells you nothing about which exceptions a function might throw.

Unwinding the stack

Picture the runtime as a stack of frames, innermost on top. A raise at the top does not return to its caller; instead each frame is discarded in turn — its pending work thrown away — until a frame that installed a handle is reached. That frame catches the exception, binds its payload, and runs the handler body in place of everything that was unwound. Watch the stack collapse:

The crucial word is discarded. When frame g is unwound, any half-finished computation it held — the multiplication it was about to do, the file it was about to close — simply vanishes. (This is why languages add finally / ensure blocks: a hook that runs during unwinding, so cleanup is not skipped.) Control never comes back to a discarded frame; exceptions are one-shot escapes, not resumable jumps — an important contrast with the continuations of the next lesson.

Operational semantics: propagate, then catch

The cleanest formulation uses evaluation contexts E — a term with a single hole marking where evaluation is currently focused. Two families of rules do everything. First, propagation: a raised exception blows away whatever context surrounds it (unless that context is a handler):

E[\,\mathsf{raise}\ v\,] \longrightarrow \mathsf{raise}\ v \qquad (E \neq \mathsf{handle}\ [\,\cdot\,]\ \mathsf{with}\ h)

This single schema is the stack unwinding: each step peels one layer of context off, propagating the \mathsf{raise}\ v outward. Second, the handler rules — one for when the protected term finished normally, one for when it raised:

\mathsf{handle}\ v\ \mathsf{with}\ h \longrightarrow v \qquad\qquad \mathsf{handle}\ (\mathsf{raise}\ v)\ \mathsf{with}\ h \longrightarrow h\ v

If the body produced a value v, the handler is discarded and v passes through. If the body raised, the handler h (a function from the exception type to the result type) is applied to the payload v. Notice the handler catches only the first layer: a raise inside the handler itself propagates further out, to the next enclosing handle.

Typing: why raise e has any type

Fix a type T_{\mathit{exn}} of exception values (in ML, the extensible exn type). The typing rule for raise is the one that surprises everyone:

\dfrac{\Gamma \vdash e : T_{\mathit{exn}}}{\Gamma \vdash \mathsf{raise}\ e : T}

The result type T in the conclusion is completely unconstrained — it appears nowhere in the premise. Why is that sound? Because raise e never returns a value: it always diverts control. Progress-and-preservation is happy to hand it whatever type the surrounding context demands, since no value of type T is ever actually produced. This is the same move that types a non-terminating loop or an explicit abort at any type — the "bottom" trick. It lets raise NotFound sit in a branch of an if whose other branch has type int, and the whole if still types as int.

The handler pins the type back down. handle demands that the protected body and the handler's output agree, giving the whole expression that common type:

\dfrac{\Gamma \vdash e : T \qquad \Gamma \vdash h : T_{\mathit{exn}} \to T} {\Gamma \vdash \mathsf{handle}\ e\ \mathsf{with}\ h : T}

Exceptions are a sum type, made control-flow

You can implement exceptions with nothing but the algebraic data types from the previous lesson. Model "a computation that either succeeds with a T or raises an exception x" as the sum T + T_{\mathit{exn}} — a Result. Propagation becomes short-circuiting: once you hit a Raised, you stop and pass it up untouched; handle is a case that turns a Raised back into a normal value. Run this store-free evaluator, which raises on division by zero and shows a handler catching it:

// "Raise as a value": a computation yields Ok(v) or Raised(exn). T + Exn. type Exn = { kind: "DivByZero" } | { kind: "NotFound"; key: string }; type Result = | { tag: "ok"; value: number } | { tag: "raised"; exn: Exn }; const ok = (n: number): Result => ({ tag: "ok", value: n }); const raise = (e: Exn): Result => ({ tag: "raised", exn: e }); // A tiny expression language, with a division that can raise. type Expr = | { tag: "num"; n: number } | { tag: "div"; l: Expr; r: Expr } | { tag: "raise"; exn: Exn } | { tag: "handle"; body: Expr; onExn: (e: Exn) => Expr }; function evalExpr(e: Expr): Result { switch (e.tag) { case "num": return ok(e.n); case "raise": return raise(e.exn); case "div": { const l = evalExpr(e.l); if (l.tag === "raised") return l; // propagate: short-circuit const r = evalExpr(e.r); if (r.tag === "raised") return r; // propagate if (r.value === 0) return raise({ kind: "DivByZero" }); return ok(Math.trunc(l.value / r.value)); } case "handle": { const res = evalExpr(e.body); if (res.tag === "ok") return res; // handle v with h => v return evalExpr(e.onExn(res.exn)); // handle (raise v) with h => h v } } } const num = (n: number): Expr => ({ tag: "num", n }); const div = (l: Expr, r: Expr): Expr => ({ tag: "div", l, r }); // 10 / 0 raises, unwinding straight past the pending work... console.log("unhandled:", JSON.stringify(evalExpr(div(num(10), num(0))))); // ...but wrapped in a handler that returns -1 on DivByZero, it is caught. const guarded: Expr = { tag: "handle", body: div(num(10), num(0)), onExn: (ex) => num(ex.kind === "DivByZero" ? -1 : 0), }; console.log("handled: ", JSON.stringify(evalExpr(guarded))); // { tag: "ok", value: -1 }

The three if (…tag === "raised") return … lines are the propagation rule in disguise, and the handle case is precisely the two handler rules. Exceptions add no new data to the language — only a new control discipline over a plain sum type. (Chaining those short-circuits by hand is tedious, which is exactly why languages bake the discipline in — and why the pattern is captured abstractly by the exception monad.)

No — and one language family thinks they made the wrong default. In Common Lisp's condition system, signalling a condition does not immediately unwind the stack. Handlers run while the signalling frame is still alive, and they can choose to resume the computation via a restart — patching the problem and continuing from where the error was raised, rather than abandoning everything below the handler. It is strictly more expressive than the raise/catch of ML, C++, Java and Python (all of which unwind first, ask questions never). The modern research direction — algebraic effects and handlers — generalises exactly this idea: an "exception" whose handler receives the continuation and may invoke it zero, one, or many times, unifying exceptions, generators, async, and more under one construct. Exceptions, it turns out, are just the special case where the handler ignores the continuation.

The typing rule \Gamma \vdash \mathsf{raise}\ e : T gives a raise any type — which means the type system will not warn you about exceptions you forgot to handle. A function typed int → int can throw NotFound, and nothing in that arrow reveals it. Standard ML, OCaml, C++ and (mostly) Python all take this route: exceptions are an unchecked effect. Java famously tried the opposite with checked exceptions in the throws clause — putting the raised-exception set into the type — and the ergonomics were controversial enough that almost no later language copied it. The takeaway: reading a function's type tells you what it returns, never what it might throw. To know that, read the code, the docs, or reach for an effect system.

A second, sharper trap: exceptions silently break equational reasoning. In a pure language let x = e in x + x equals e + e. With exceptions (and effects) it does not — if e raises, the first form raises once at the let, and substituting e twice changes where and how often the effect happens. Refactorings that are obviously safe in pure code can move, duplicate, or delete a raise.