Algebraic Data Types and Pattern Matching

Ask a working functional programmer what makes their language feel tight — why a whole class of bugs simply cannot happen — and the answer is almost always the same two features working as one: algebraic data types and pattern matching. An ADT lets you say "a shape is a circle or a rectangle or a triangle, and here is exactly what data each one carries." Pattern matching then forces you to say what to do in every case — and the compiler complains if you forget one. Together they turn "did I handle all the cases?" from a nagging worry into a mechanically checked fact.

The name "algebraic" is not decoration. These types are built by exactly two operations — a sum (a choice between alternatives) and a product (a bundle of fields) — and those operations obey the ordinary laws of high-school algebra. This lesson develops the calculus of sums-of-products, the typing rules for constructors and case, and the beautiful compilation problem hiding underneath a humble match: how a nested pattern becomes an efficient decision tree, and how a compiler proves a match is exhaustive and free of dead branches.

Sums of products: the algebra of data

Start from records and variants. A product type T_1 \times T_2 holds a T_1 and a T_2 at once — a record, a tuple, a struct. A sum type T_1 + T_2 holds a T_1 or a T_2, tagged so you always know which — a variant, a tagged union, an enum. An algebraic data type is nothing more exotic than a sum of products: a choice among several constructors, each of which bundles zero or more fields.

\texttt{Shape} \;=\; \underbrace{\texttt{Circle}(\mathbb{R})}_{\text{product}} \;+\; \underbrace{\texttt{Rect}(\mathbb{R}\times\mathbb{R})}_{\text{product}} \;+\; \underbrace{\texttt{Tri}(\mathbb{R}\times\mathbb{R}\times\mathbb{R})}_{\text{product}}

Why "algebraic"? Because if you read + and \times as counting the inhabitants of a type, the laws of arithmetic fall straight out. Write |T| for the number of values of type T. Then a sum adds and a product multiplies:

|T_1 + T_2| = |T_1| + |T_2| \qquad\quad |T_1 \times T_2| = |T_1| \cdot |T_2|

The unit type \mathbf{1} (one value) is the multiplicative identity — a field of type \mathbf{1} carries no information, and indeed T \times \mathbf{1} \cong T. The empty type \mathbf{0} (no values) is the additive identity: T + \mathbf{0} \cong T, and a function \mathbf{0}\to T exists uniquely for any T (there is nothing to map). \mathtt{Option}\,T = \mathbf{1} + T — "nothing, or a T" — is the humblest sum-of-products there is, and it has exactly 1 + |T| values, as the algebra predicts.

Constructors and case: the typing rules

A constructor is an injection into a sum: it tags a value so the runtime — and the type system — knows which alternative it came from. Case analysis is the only way back out. Here are the rules for a binary sum T_1 + T_2, with left/right injections \mathsf{inl} and \mathsf{inr}:

\dfrac{\Gamma \vdash e : T_1}{\Gamma \vdash \mathsf{inl}\,e : T_1 + T_2} \qquad\qquad \dfrac{\Gamma \vdash e : T_2}{\Gamma \vdash \mathsf{inr}\,e : T_1 + T_2}

Notice that a single injection cannot, on its own, know the whole sum type — the T_2 in the left rule is unconstrained. This is why constructors in ML/Haskell belong to a declared datatype: the declaration supplies the missing half. Elimination is case, which must handle both tags and produce the same result type T in each branch, binding the payload to a fresh variable:

\dfrac{\Gamma \vdash e : T_1 + T_2 \qquad \Gamma, x_1 : T_1 \vdash e_1 : T \qquad \Gamma, x_2 : T_2 \vdash e_2 : T} {\Gamma \vdash \big(\mathsf{case}\;e\;\mathsf{of}\;\mathsf{inl}\,x_1 \Rightarrow e_1 \mid \mathsf{inr}\,x_2 \Rightarrow e_2\big) : T}

Two demands make this the workhorse of type-safe programming. First, every constructor of the sum must appear as an arm — miss one and the term does not type. Second, all arms must agree on the answer type T, so the whole case has a single, predictable type no matter which tag arrives at runtime. Exhaustiveness is not a lint suggestion; it is baked into the elimination rule.

Nested patterns compile to a decision tree

Real pattern matching goes deeper than one tag. You write a column of patterns, each possibly nested — Some(None), Cons(0, rest), (true, _) — and the language picks the first that fits. The compiler's job is to turn that declarative table into a decision tree: a sequence of primitive tag-tests, each branch narrowing the possibilities, with no field inspected twice and no redundant test. Consider matching a value of type \mathtt{Option}(\mathtt{Option}\;\mathbb{N}) against three patterns:

match x with | None => "empty" | Some(None) => "hole" | Some(Some n)=> "value"

The naive reading tries each row top-to-bottom, re-testing the outer tag every time. The compiled decision tree tests the outer tag once, then — only on the \mathsf{Some} branch — tests the inner tag. Reveal it step by step:

Each internal node is a single switch on a constructor tag; each leaf is an action (a right-hand side). This is exactly what maranget's algorithm — the one used in OCaml — produces: it repeatedly picks a column, splits the pattern matrix by the constructors appearing there, and recurses, yielding a tree whose every path corresponds to a distinct runtime shape. A good compiler even balances the choice of which column to test first to keep the tree small.

Exhaustiveness and redundancy, mechanically

The same matrix machinery answers the two questions a programmer most wants answered at compile time. Exhaustiveness: is there any value the patterns all miss? Redundancy: is any row unreachable because earlier rows already cover everything it could match? Both reduce to a single primitive — a usefulness check: given the rows so far, is there a value matched by a candidate row and by none above it?

Usefulness is decided by the same recursive constructor-splitting used to build the decision tree, which is why a single algorithm gives you the compiled match, the "non-exhaustive: Some(None) not matched" warning, and the "unreachable branch" warning all at once. When the checker reports a missing case it can even reconstruct a witness — the smallest value that slips through — which is why OCaml and Rust can print "you forgot Some(None)" rather than a vague complaint.

A pattern-matching evaluator, end to end

Here is the whole story in miniature: an ADT for a tiny expression language, encoded in TypeScript as a tagged union (a sum of products), and an evaluator whose switch is a total, exhaustive case. Because TypeScript narrows the union in each arm, forgetting a constructor is a type error — the assertNever trick makes the exhaustiveness check explicit. Press Run:

// An algebraic data type: a SUM of four PRODUCTS (constructors). type Expr = | { tag: "Lit"; value: number } // Lit(number) | { tag: "Neg"; arg: Expr } // Neg(Expr) | { tag: "Add"; left: Expr; right: Expr } // Add(Expr, Expr) | { tag: "IfPos"; cond: Expr; then: Expr; else: Expr }; // Exhaustiveness enforced by the compiler: an unmatched tag makes `e` non-never here. function assertNever(e: never): never { throw new Error("non-exhaustive match: " + JSON.stringify(e)); } // The evaluator IS a case-analysis over the sum. One arm per constructor. function evalExpr(e: Expr): number { switch (e.tag) { case "Lit": return e.value; case "Neg": return -evalExpr(e.arg); case "Add": return evalExpr(e.left) + evalExpr(e.right); case "IfPos": return evalExpr(e.cond) > 0 ? evalExpr(e.then) : evalExpr(e.else); default: return assertNever(e); // compile-time proof all cases are covered } } // Nested pattern matching in action: simplify Neg(Neg x) => x, Add(Lit 0, e) => e. function simplify(e: Expr): Expr { switch (e.tag) { case "Neg": if (e.arg.tag === "Neg") return simplify(e.arg.arg); // Neg(Neg x) => x return { tag: "Neg", arg: simplify(e.arg) }; case "Add": { const l = simplify(e.left), r = simplify(e.right); if (l.tag === "Lit" && l.value === 0) return r; // Add(0, e) => e if (r.tag === "Lit" && r.value === 0) return l; // Add(e, 0) => e return { tag: "Add", left: l, right: r }; } case "IfPos": return { tag: "IfPos", cond: simplify(e.cond), then: simplify(e.then), else: simplify(e.else) }; case "Lit": return e; default: return assertNever(e); } } const lit = (n: number): Expr => ({ tag: "Lit", value: n }); const neg = (a: Expr): Expr => ({ tag: "Neg", arg: a }); const add = (l: Expr, r: Expr): Expr => ({ tag: "Add", left: l, right: r }); // Add(0, Neg(Neg 5)) == 5 const prog: Expr = add(lit(0), neg(neg(lit(5)))); console.log("eval =", evalExpr(prog)); // 5 console.log("simplify=", JSON.stringify(simplify(prog))); // { tag: "Lit", value: 5 }

Delete the case "Lit" from evalExpr and the compiler rejects the program at assertNever(e): e is no longer never, so the "impossible" branch is reachable. That is exhaustiveness checking, running in your editor as you type.

Take the algebra seriously and something wonderful happens. If a type is a polynomial in its variable — a binary tree is T(a) = 1 + a \times T(a)^2 — then the derivative \frac{dT}{da}, computed by the ordinary rules of calculus, turns out to be the type of one-hole contexts: a tree with a single element removed, remembering exactly where the hole is. Conor McBride's "The Derivative of a Regular Type is its Type of One-Hole Contexts" makes this precise, and it is the theory behind the zipper — the data structure every functional text editor uses to point into a tree and move around efficiently. Data types don't just look like algebra; you can do calculus on them and the answers mean something.

The most dangerous pattern you can write is a catch-all where you meant to be exhaustive. A final | _ => default arm silences the compiler forever: add a new constructor to your datatype six months later and every match with a wildcard keeps compiling, silently routing the new case to the wrong default. The exhaustiveness checker — your most valuable tool — has been switched off precisely where you needed it. Prefer to enumerate the cases; let the compiler's non-exhaustiveness error be your to-do list when the type grows.

A subtler trap: pattern order matters, and a too-general row above a specific one makes the specific one redundant. | x => ... before | 0 => ... means the 0 case can never fire. Good compilers warn ("this match case is unused"), but the warning is easy to ignore — and a redundant branch is often a real logic bug wearing a disguise.