Algebraic Data Type
An algebraic data type (ADT) is a composite data type formed by combining simpler types according to algebraic operations: sum types (disjoint unions, written `A + B` or `A | B`) and product types (tuples and records, written `A × B` or `(A, B)`). The term "algebraic" is literal: the number of values in a sum type is the sum of the values in its components, and the number of values in a product type is the product. A type `boolean + int` has 2 + 2^32 values; a type `(boolean, int)` has 2 × 2^32 values. This arithmetic is not a coincidence; it is the foundation of a deep connection between data structures and algebra that underlies modern type theory.
Sum Types and Product Types
A sum type, also called a tagged union or variant type, represents a value that is exactly one of several alternatives. In OCaml, the type `type shape = Circle of float | Rectangle of float * float` declares that a `shape` is either a `Circle` with one `float` (the radius) or a `Rectangle` with two `float`s (width and height). The tag — `Circle` or `Rectangle` — is carried at runtime, and pattern matching is used to branch on which alternative is present. The compiler verifies that every alternative is handled, eliminating a class of runtime errors that plague union types in untyped or weakly-typed languages.
A product type represents a value that contains values of several types simultaneously. A record `{name: string; age: int}` is a product type: every value of this type contains both a `name` and an `age`. A tuple `(string, int)` is the same structure without named fields. Product types are the mathematical dual of sum types: where sums say "either A or B," products say "both A and B." Together, sums and products are the building blocks of all data modeling in statically typed functional languages.
Pattern Matching and Exhaustiveness
The power of algebraic data types is not merely in their construction but in their destruction through pattern matching. When a function processes a sum type, it must provide a case for every constructor. The compiler checks this exhaustively: a match that omits a case is a compile-time error, not a runtime crash. This transforms what would be a runtime `switch` statement with a forgotten `default` case into a statically verified total function.
This property is not a linting rule; it is a theorem. In languages with algebraic data types and pattern matching, the type system and the pattern matcher are coupled: the set of patterns must cover the set of constructors, and the compiler proves this coverage. This is why OCaml, Haskell, and Rust can eliminate null pointer exceptions, missing case errors, and invalid state transitions at compile time: the type system encodes the valid states, and pattern matching enforces that every state is handled.
Recursive Types and Inductive Structure
Algebraic data types can be recursive, defining data structures that contain values of the same type. The type `type tree = Leaf | Node of int * tree * tree` defines a binary tree as either a `Leaf` or a `Node` containing an integer and two subtrees. This recursive definition is an inductive type: the set of values is defined by induction on the structure, with `Leaf` as the base case and `Node` as the inductive step.
Inductive types are the computational expression of mathematical induction. Every function on an inductive type is defined by recursion on its structure, and the type system guarantees that well-founded recursion terminates (or, in lazy languages, that productive recursion yields well-defined values). The connection to category theory is explicit: inductive types are initial algebras, and the recursion principle is the universal property of the initial algebra. This is not abstract nonsense; it is the reason why folding a list, traversing a tree, and evaluating an expression are all instances of the same pattern.
The algebraic data type is the most important idea in programming language design that mainstream industry has not yet understood. Object-oriented inheritance, with its open hierarchies and virtual dispatch, is a pale imitation of sum types that sacrifices exhaustiveness checking for extensibility. Every `if (x == null)` check in a Java program is an admission that the language failed to encode the possibility of absence in the type system. Every `switch` statement without a `default` is a bet that the programmer remembered all the cases. Algebraic data types eliminate both bets by making the type system responsible for correctness. The languages that dominate industry — Java, C#, Python, JavaScript — are not missing a feature; they are missing a foundation.