Algebraic Data Types and Pattern Matching

A product type `A × B` (written `(A, B)` or as a record `{fst: A, snd: B}`) represents a value that simultaneously contains an `A` and a `B`. Its introduction rule is pairing: from `a : A` and `b : B` we build `(a, b) : A × B`. Its elimination rule is projection: from `p : A × B` we extract `fst(p) : A` and `snd(p) : B`. Records and structs generalize this to named fields; tuples are the anonymous case. The name "product" comes directly from counting: if `A` has `m` inhabitants and `B` has `n`, then `A × B` has exactly `m·n` inhabitants — one for each pairing, just as in ordinary multiplication. A sum type `A + B` (also called a tagged union, disjoint union, or variant type) represents a value that is either an `A` or a `B`, tagged so the two cases are distinguishable even when `A` and `B` overlap or coincide. Its introduction rules are the two constructors `inl : A → A + B` and `inr : B → A + B` (traditionally "inject left" / "inject right"; in surface syntax these become named constructors like `Some`/`None` or `Leaf`/`Node`). Its elimination rule is case analysis: to consume a value of type `A + B` you must supply a handler for both possibilities. Counting again: if `A` has `m` inhabitants and `B` has `n`, then `A + B` has `m + n` — one for each tagged copy, matching ordinary addition. This numeric analogy is why the whole family is called algebraic: type formation obeys laws such as `A × (B + C) ≅ A × B + A × C` (distributivity) and `A + 0 ≅ A` (where `0` is the empty/void type, the additive identity), directly paralleling ring axioms. A general algebraic data type declaration introduces a new named type together with a finite list of constructors, each constructor taking a (possibly empty) tuple of argument types — so each constructor is itself a product, and the type as a whole is a sum of those products. For example, ``` data Shape = Circle(radius: Float) | Rectangle(width: Float, height: Float) | Triangle(a: Float, b: Float, c: Float) ``` declares `Shape` as `Circle-args + Rectangle-args + Triangle-args`, where each variant's arguments form a product. Constructors are ordinary typed functions — `Circle : Float → Shape` — except that they are injective and disjoint: no two different constructors ever produce equal values, and each constructor is determined by its arguments. This injectivity/disjointness pair is what lets pattern matching work: given a `Shape` value, we can always ask "which constructor produced this, and what were its arguments?" and get a unique answer. A `match` (or `case`, or `switch` in ADT-aware languages) expression enumerates patterns — one per constructor, optionally with sub-patterns for nested ADTs and variables to bind constructor arguments — and the compiler's exhaustiveness checker verifies that the patterns cover every possible constructor of the scrutinee's type, with no case left unhandled and (for well-designed languages) no unreachable case left dead. Recursive ADTs, where a constructor's arguments mention the type being defined (e.g., `List(a) = Nil | Cons(a, List(a))`), give the type-theoretic foundation for inductively defined data. Pattern matching on such types, combined with structural recursion, is precisely the mechanism used to define functions over lists, trees, and other recursive structures — the topic taken up under Recursion and Higher-Order Functions.

Typing constructors. For a data declaration ``` data T(α₁,...,αₖ) = C₁(τ₁₁,...,τ₁ₙ₁) | C₂(τ₂₁,...,τ₂ₙ₂) | ... | Cₘ(τₘ₁,...,τₘₙₘ) ``` (possibly parametrically polymorphic in type variables `α₁,...,αₖ`, connecting to Parametric Polymorphism), the type checker installs each `Cᵢ` as a function ``` Cᵢ : τᵢ₁ → τᵢ₂ → ... → τᵢₙᵢ → T(α₁,...,αₖ) ``` This is exactly a curried constructor function, typed like any other function in the simply typed lambda calculus, except it is marked as a data constructor so the exhaustiveness checker (below) can enumerate `{C₁,...,Cₘ}` as the complete set of ways to build a `T`.

Typing and checking a match. A match expression ``` match e { p₁ -> e₁ | p₂ -> e₂ | ... | pₖ -> eₖ } ``` is typed by: (1) inferring the type `T` of the scrutinee `e`; (2) checking each pattern `pᵢ` against `T`, extending the local typing context with any variables bound by `pᵢ`; (3) checking each branch body `eᵢ` at some common result type `σ`, under its extended context; (4) running exhaustiveness and (5) redundancy checks over the pattern list. If all pass, the whole match has type `σ`.

Exhaustiveness checking is the algorithmic heart of the mechanism. The standard technique (used in ML-family and Haskell compilers) maintains a set of uncovered pattern spaces, represented compactly as a list of pattern vectors with wildcards, and processes the match's patterns top to bottom, subtracting each pattern's coverage from the uncovered set: ``` function CheckExhaustive(scrutineeType T, patterns [p1, ..., pk]): uncovered := { Wildcard } # initially: "any value of type T" is uncovered for pi in patterns: if uncovered is empty: report "pattern pi is unreachable" # redundancy check newUncovered := {} for u in uncovered: newUncovered += Subtract(u, pi) # part of u not matched by pi uncovered := newUncovered if uncovered is not empty: witness := PickExample(uncovered) report "non-exhaustive match: missing case, e.g. " + witness else: report "exhaustive" function Subtract(spacePattern u, matchPattern p):

# u and p are pattern trees over the same constructor tree;

# returns the part of u's coverage not covered by p, as a set (list) of pattern trees if p is Wildcard or Variable: return {} # p covers everything u covers if p is Constructor(C, subpatterns) and u is Wildcard:

# expand u into one sub-case per constructor of T result := {} for each constructor Cj of T (Cj != C): result += { Constructor(Cj, Wildcard,...,Wildcard) } result += { Constructor(C, Wildcard,...,Wildcard) minus-matched-by(p) via recursive Subtract on arguments } return result if p is Constructor(C, subpatterns) and u is Constructor(C, subU) with same C: return CartesianSubtract(subU, subpatterns) # recurse component-wise if p is Constructor(C, ...) and u is Constructor(C', ...) with C != C': return { u } # p cannot touch this case at all ``` Intuitively, `uncovered` tracks "the region of the value space not yet proven reachable by an earlier pattern," starting as the whole type and shrinking (constructor by constructor, argument by argument) as each pattern is processed. If anything remains uncovered at the end, the compiler has found a concrete counterexample value — a witness — that no pattern matches, and it reports that value as a missing case. If, when processing pattern `pᵢ`, the uncovered set is already empty, then `pᵢ` can never fire and is flagged as dead code — a genuinely useful diagnostic in its own right.

Compiling a match to code. Once type-checked, a match compiles to a decision tree or backend switch: at runtime, each value carries a small integer or pointer tag identifying its constructor (plus, inline or boxed, its constructor arguments). Compilation dispatches on this tag — typically via a jump table for a match with many constructors, giving `O(1)` dispatch — then binds the pattern variables to the corresponding fields and evaluates the matched branch. Nested patterns (e.g., matching on `Cons(Leaf, rest)`) are compiled via well-studied pattern-match compilation algorithms (Wadler's or the Maranget "compiling pattern matching to good decision trees" approach) that share tests between overlapping patterns to avoid re-scrutinizing the same subterm twice. ```

# Runtime representation and dispatch, sketched struct Value { tag: Int # which constructor, e.g. 0=Nil, 1=Cons fields: Array # constructor arguments, empty for nullary constructors } function evalMatch(v: Value, branches: Array<(tag: Int, arity: Int, body: Fn)>): for (t, arity, body) in branches: if v.tag == t: return body(v.fields[0], ..., v.fields[arity-1]) # bind and evaluate error("unreachable: exhaustiveness checker guarantees this never triggers") ``` The final `error` line is the operational payoff of exhaustiveness checking: it is provably dead whenever the static checker accepted the match, so production compilers either omit it or compile it to a trap instruction rather than a real branch.

Type checking cost. Checking a single constructor application `Cᵢ(e₁,...,eₙᵢ)` costs the same as checking any `n`-ary function application: `O(n)` recursive type checks against the declared argument types, so this step contributes no asymptotic overhead beyond ordinary function application in the simply typed lambda calculus.

Exhaustiveness checking cost. Let a match have `k` patterns over a scrutinee type with maximum constructor arity `a` and nesting depth `d` (how deeply patterns nest sub-patterns). The uncovered-set algorithm processes patterns one at a time, and in the worst case the uncovered set can grow to size proportional to the product of constructor counts along each nested position — but in practice, and in all standard formulations (Maranget's algorithm, used in OCaml and Rust), the check runs in time polynomial in the size of the pattern matrix: `O(k · d · a)` for well-structured matches, since each pattern only needs to be compared against the current frontier of uncovered constructor combinations, and each comparison walks the pattern tree once. Pathological cases with many independent nested sum types can exhibit combinatorial blowup in the number of missing-case witnesses reported, but the yes/no exhaustiveness decision itself is decidable and tractable for all patterns arising from realistic ADTs, because constructor sets are finite and fixed by the type declaration — this finiteness is exactly what makes the check terminate, unlike exhaustiveness questions over unbounded domains like integers.

Match compilation and dispatch cost. Compiling `k` patterns into a decision tree costs `O(k · d)` in the size of the generated code (each pattern contributes at most one test per nesting level), and the resulting runtime dispatch is `O(1)` for a top-level tag switch (jump table) plus `O(d)` for extracting nested fields — matching the cost of an ordinary field access or array index, i.e. no asymptotic overhead versus hand-written tagged-union code with manual `if`/`else` tag checks.

Correctness argument. The key safety property is: > Progress-and-preservation for match: if `e : T` is a well-typed value (a constructor application `Cᵢ(v₁,...,vₙᵢ)`) and `match e {p₁->e₁,...,pₖ->eₖ}` passed exhaustiveness checking, then some `pⱼ` matches `e`, and the corresponding branch is well-typed at the match's result type. The proof is a direct consequence of two invariants maintained by the algorithm above: 1. Soundness of `Subtract`: at every step, `uncovered` exactly denotes the set of values of type `T` matched by none of `p₁,...,pᵢ` so far — proved by induction on the pattern list, using the fact that `Subtract(u, p)` is defined by case analysis that exactly mirrors the constructor structure of `T` (each constructor is either fully consumed by `p`, fully excluded, or its own sub-arguments recursively subtracted). 2. Completeness of the constructor set: because `T`'s constructors `C₁,...,Cₘ` are declared exhaustively and are pairwise disjoint and injective (a metatheoretic property enforced by the type system, not by the programmer), every value of type `T` is `Cᵢ(v₁,...,vₙᵢ)` for exactly one `i` — this is the "no junk, no confusion" property standard in the theory of inductive/algebraic datatypes. Combining (1) and (2): if `uncovered = ∅` after processing all patterns, then by (1) no value of type `T` is left unmatched, and by (2) every runtime value genuinely has some constructor form, so the runtime dispatch in `evalMatch` is guaranteed to find a matching branch — hence the `error("unreachable")` line is dead code whenever the static check succeeds. This is a genuine proof by structural induction on the finite constructor set, not merely a claim: it is exactly analogous to proving a `switch` over an `enum` total once every enum tag has a case, except ADTs generalize this to arbitrarily nested, recursive, and parametrically polymorphic shapes.

Tradeoffs. Exhaustiveness checking requires the compiler to know the closed set of constructors for a type ahead of time; this is why "open" extensible unions (as in object-oriented subclassing, or JavaScript's untagged values) cannot get the same static guarantee without extra machinery (sealed traits, visitor patterns, or explicit "open union" library encodings). Deeply nested patterns over many-constructor types can also produce exponentially many warning messages (though not exponential checking time) if a language reports every missing combination individually rather than a minimal counterexample — real compilers mitigate this by reporting only one witness per top-level match, as sketched in the pseudocode above.

Take a small recursive ADT for arithmetic expressions and a function evaluating them, then trace both type checking and exhaustiveness checking concretely. ``` data Expr = Num(Int) | Add(Expr, Expr) | If(Expr, Expr, Expr) # nonzero test: If(cond, then, else) function eval(e: Expr) -> Int: match e { Num(n) -> n Add(l, r) -> eval(l) + eval(r) If(c, t, f) -> if eval(c) != 0 then eval(t) else eval(f) } ``` Consider evaluating `Add(Num(3), If(Num(0), Num(10), Num(20)))`.

Now trace the exhaustiveness checker on the `match` inside `eval`, following the pseudocode: 1. `uncovered = {Wildcard}` (any `Expr` at all). 2. Process `Num(n)`: `Wildcard` expands over `Expr`'s three constructors; the `Num`-shaped part is fully consumed (bound by variable `n`), leaving `uncovered = {Add(Wildcard,Wildcard), If(Wildcard,Wildcard,Wildcard)}`. 3. Process `Add(l, r)`: matches the `Add` case exactly (both sub-patterns are variables, hence wildcards), removing it: `uncovered = {If(Wildcard,Wildcard,Wildcard)}`. 4. Process `If(c, t, f)`: matches the remaining `If` case exactly: `uncovered = {}`. 5. Final `uncovered` is empty → exhaustive, no runtime fallthrough possible, compiled to a 3-way jump table indexed by tag. Now suppose a programmer forgets the `If` case: ``` function badEval(e: Expr) -> Int: match e { Num(n) -> n Add(l, r) -> badEval(l) + badEval(r) } ``` Re-running the check: after step 3 above, `uncovered = {If(Wildcard,Wildcard,Wildcard)}`, and there are no more patterns to process. The checker reports this residual as a concrete witness — e.g. `If(Num(0), Num(0), Num(0))` — and the compiler rejects the function before it ever runs, in contrast to a language with plain `switch`/`instanceof` chains, where the analogous mistake compiles cleanly and only manifests as a crash (or worse, silently wrong behavior from a default branch) when an `If` node is finally evaluated in production.

The theoretical roots of sum and product types trace to intuitionistic logic and the Curry–Howard correspondence, where sum types correspond to logical disjunction and product types to conjunction; pattern matching corresponds to disjunction elimination (case analysis) in natural deduction. The concrete language mechanism — algebraic data types with `data`/`type` declarations and exhaustive pattern matching as a first-class syntactic construct — was crystallized in the ML family of languages in the 1970s and carried forward through Miranda and Haskell, later reappearing with modern syntax in OCaml, F#, Scala, Swift, Rust, and TypeScript.

Compilers themselves are a primary consumer: abstract syntax trees are almost universally represented as recursive ADTs (an `Expr` or `Stmt` sum type per node kind), and every compiler pass — parsing, type checking, optimization, code generation — is written as pattern matches over that tree, making ADTs the backbone of how programming languages implement other programming languages. Rust's `Option` and `Result` are ADTs that replace null pointers and unchecked exceptions with compiler-checked alternatives, directly preventing null-dereference bugs at the type level; Swift's `enum` with associated values plays the identical role in iOS/macOS application code. Functional-first industrial systems — financial modeling in OCaml and F#, blockchain and compiler tooling in Haskell, telecom systems in Erlang's pattern-matching-based clause dispatch — rely on ADTs to make protocol states, message formats, and parser outputs statically checkable. TypeScript's discriminated unions bring the same discipline to large JavaScript codebases, letting editors and compilers flag missing cases in UI state machines before deployment. The pattern also underlies parser combinator libraries, JSON/protobuf schema modeling, and the `Maybe`/`Either` types that motivate the treatment of Monads: An Introduction.

Ask the tutor: How does pattern-match compilation choose the order in which to test nested sub-patterns to minimize the number of runtime checks?