Algebraic data type

An algebraic data type is a type built from sums, where a value is one of several alternatives, and products, where a value has several components at once, possibly recursively. The name comes from counting: the number of values of a sum type is the sum of the numbers for its alternatives, and of a product the product, so types obey the laws of algebra. Values are taken apart by pattern matching, which the compiler checks for missing and unreachable cases.

A product type holds several values at once: a pair int * string or a record { name : string; age : int }. A sum type holds one of several alternatives, each with its own data: Circle of float | Rect of float * float is a circle with a radius or a rectangle with two sides, never both. Combining the two, recursively, gives lists, trees, syntax trees, protocol messages and most of the data a program works with. In OCaml sums are called variants, and the alternatives constructors.

(* A recursive sum of products: arithmetic expressions. *)
type expr =
  | Num of int
  | Var of string
  | Add of expr * expr
  | Mul of expr * expr
  | Neg of expr
 
let rec eval env = function
  | Num n -> n
  | Var x -> List.assoc x env
  | Add (a, b) -> eval env a + eval env b
  | Mul (a, b) -> eval env a * eval env b
  | Neg a -> - eval env a
 
(* Nested patterns match on the shape of a whole subtree at once. *)
let rec simplify e =
  match e with
  | Add (a, b) -> (
      match (simplify a, simplify b) with
      | Num 0, x | x, Num 0 -> x
      | Num x, Num y -> Num (x + y)
      | a, b -> Add (a, b))
  | Mul (a, b) -> (
      match (simplify a, simplify b) with
      | Num 0, _ | _, Num 0 -> Num 0
      | Num 1, x | x, Num 1 -> x
      | Num x, Num y -> Num (x * y)
      | a, b -> Mul (a, b))
  | Neg a -> (match simplify a with Neg b -> b | Num n -> Num (-n) | b -> Neg b)
  | Num _ | Var _ -> e
 
let rec show = function
  | Num n -> string_of_int n
  | Var x -> x
  | Add (a, b) -> "(" ^ show a ^ " + " ^ show b ^ ")"
  | Mul (a, b) -> show a ^ " * " ^ show b
  | Neg a -> "-" ^ show a

e                       =  (1 * x + (2 + 3) * --y)
simplify e              =  (x + 5 * y)
eval [x=4; y=10] e      =  54

Each function is a match with one case per constructor, and simplify matches on the shape of two subtrees at once. The same definition in an object-oriented language would be a class hierarchy with one subclass per constructor and one method per operation.

Writing $|T|$ for the number of values of a type:

where $1$ is the unit type, with one value, and $0$ the empty type, with none. bool is $1+1$, 'a option is $1+a$, and result is a sum of the success and error types. The counts can be checked by listing every value:

(* Enumerate every value of a few small types and count them. *)
let bools = [ false; true ]
let units = [ () ]
let options xs = None :: List.map Option.some xs
let pairs xs ys = List.concat_map (fun x -> List.map (fun y -> (x, y)) ys) xs
let eithers xs ys = List.map Either.left xs @ List.map Either.right ys
 
(* A function from a finite type is its table of outputs, one per input. *)
let rec functions dom cod =
  match dom with
  | [] -> [ [] ]
  | _ :: rest -> List.concat_map (fun y -> List.map (fun t -> y :: t) (functions rest cod)) cod

unit                         1   1
bool                         2   1 + 1 = 2
bool option                  3   1 + 2 = 3
bool * bool                  4   2 * 2 = 4
(bool, unit) Either.t        3   2 + 1 = 3
bool option * bool           6   3 * 2 = 6
bool -> bool option          9   3 ^ 2 = 9
bool option -> bool          8   2 ^ 3 = 8

Function types are the exponentials: a function from a type with three values to one with two is a table of three entries, each with two choices.

The laws of arithmetic hold for types up to isomorphism, where each law is witnessed by a pair of functions inverse to each other:

(* The laws of arithmetic hold for types up to isomorphism: each law is a
   pair of functions that are inverse to each other. *)
 
(* a * (b + c) = a * b + a * c *)
let distribute (a, e) = match e with Either.Left b -> Either.Left (a, b) | Either.Right c -> Either.Right (a, c)
let factor = function Either.Left (a, b) -> (a, Either.Left b) | Either.Right (a, c) -> (a, Either.Right c)
 
(* 1 + 1 = 2 *)
let to_bool = function Either.Left () -> false | Either.Right () -> true
let of_bool b = if b then Either.Right () else Either.Left ()
 
(* a^(b + c) = a^b * a^c: a function out of a sum is a pair of functions. *)
let split f = ((fun b -> f (Either.Left b)), fun c -> f (Either.Right c))
let join (g, h) = function Either.Left b -> g b | Either.Right c -> h c

factor (distribute v) = v          ->  true
to_bool (of_bool b) = b            ->  true
join (split f) agrees with f       ->  true

The exponential laws say that a function out of a sum is a pair of functions, one per alternative, which is what a pattern match is, and that a function of a pair is a function returning a function, which is currying.

Recursive types

A recursive type is a fixed point of an equation. Lists satisfy $L=1+a\times L$, and unfolding the equation gives

a list of length 0, 1, 2 and so on. Binary trees satisfy $T=1+a\times T^2$, and the coefficient of $a^n$ in the solution is the $n$th Catalan number, the number of tree shapes with $n$ nodes. Formal manipulations of these power series are meaningful: the derivative $\partial L/\partial a=L^2$ is the type of lists with one element removed, and in general the derivative of a type is its type of one-hole contexts^[7], which is the zipper.

A pattern match takes a value apart by its constructor and binds the components. Because the constructors of a sum are known, the compiler can check that a match handles all of them, and that no case is unreachable^[4]:

type connection =
  | Disconnected
  | Connecting of { attempt : int }
  | Connected of { address : string }
 
let is_up = function
  | Connected _ -> true
  | Disconnected -> false
 
let label = function
  | Disconnected -> "down"
  | Connecting _ -> "retrying"
  | Connected _ -> "up"
  | Connecting { attempt = 1 } -> "first try"

File "d4_warn.ml", lines 6-8, characters 12-25:
6 | ............function
7 |   | Connected _ -> true
8 |   | Disconnected -> false
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Connecting _
File "d4_warn.ml", line 14, characters 4-30:
14 |   | Connecting { attempt = 1 } -> "first try"
         ^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 11 [redundant-case]: this match case is unused.

The first warning is the practical benefit of sum types. When a constructor is added to a type, every match that does not handle it is reported, so the compiler lists the code that needs updating. Matches are compiled into decision trees or backtracking automata that test each part of the value once^[5].

Illegal states

A record of optional fields, such as an address that is present only when connected, can represent combinations that should never happen: an address while disconnected, or a retry count while connected. A sum type with one constructor per state, each carrying only the data that exists in that state, cannot. "Make illegal states unrepresentable" is the usual summary^[8].

A sum type is a tagged union: a value records which alternative it is and holds that alternative's data. In OCaml, constructors without arguments are stored as immediate integers numbered in order, and constructors with arguments as heap blocks whose header tag is the constructor's index among the non-constant ones:

(* How OCaml stores a variant: constructors without arguments are
   immediate integers, numbered in order; constructors with arguments are
   heap blocks whose tag is their index among the non-constant ones. *)
type shape = Point | Circle of float | Rect of float * float | Empty
 
let describe v =
  let r = Obj.repr v in
  if Obj.is_int r then Printf.sprintf "immediate %d" (Obj.obj r : int)
  else Printf.sprintf "block, tag %d, %d field(s)" (Obj.tag r) (Obj.size r)

Point           immediate 0
Empty           immediate 1
Circle 1.       block, tag 0, 1 field(s)
Rect (2., 3.)   block, tag 1, 2 field(s)

A match therefore tests whether the value is an immediate or a block, and then its integer or tag, often through a jump table. In C the same structure is written by hand, as a struct with an enum field and a union, and nothing checks that the right member is read. Rust's enums are tagged unions checked by the compiler, and use unused bit patterns of the payload as the tag where possible, so Option<&T> is the size of a pointer.

GADTs let each constructor refine the type parameter, so a type can carry invariants about the value. Polymorphic variants are sums whose constructors exist independently of any declaration. Church and Scott encodings represent algebraic data as functions: the Church encoding of a value is its fold, and the Scott encoding its pattern match.

Algebraic data types and class hierarchies split the same table in opposite directions. With a sum type, adding an operation is one new function and adding a case means editing every existing match; with a class hierarchy, adding a case is one new class and adding an operation means editing every class. Wadler called the problem of doing both without editing existing code the expression problem^[6].

Sum and product types with pattern matching are central in ML, OCaml, Haskell, F#, Rust (enums), Swift (enums with associated values) and Scala (sealed traits with case classes). Kotlin has sealed classes, TypeScript discriminated unions of object types with a common tag field, and Java sealed interfaces with records and pattern matching in switch.

Burstall introduced data types defined by constructors with pattern matching on them in the language NPL in 1977^[2], and the language HOPE of 1980 gave them the form used since^[1]. They were adopted by Standard ML, Miranda and Haskell, and, much later, by mainstream languages. The type-theoretic account, with sums, products and recursive types as fixed points, is in Pierce's textbook^[3].

• Polymorphic variantA polymorphic variant is a variant whose constructors, called tags and written with a backquote in OCaml, exist independently of any type declaration. Their types are sets of tags with bounds: [> `A] means at least `A, [< `A | `B] means at most those two, and unification works out unions and intersections of those sets using row variables. They let functions share constructors across types, be extended with new cases without editing old code, and encode subtyping, at the cost of longer types and error messages and of typos in open types going unnoticed.
• GADTA generalized algebraic data type (GADT) is an algebraic data type whose constructors may each give a more specific result type than the declared one, instead of all sharing one polymorphic return type. Matching on a constructor then tells the type checker what the type parameter was, so a single well-typed eval can return an int for an Add node and a bool for an Eq node, checked at compile time rather than by a run-time tag test. GADTs express typed syntax trees, type representations and equality proofs, typed format strings and length-indexed data. The price is that type inference needs annotations.
• ZipperA zipper represents a data structure together with a focus, a position inside it: the substructure at the focus, and the path from the focus back to the root together with everything to either side of that path. Moving the focus one step and editing at the focus take constant time, and the structure is persistent, so edits share everything off the path. The type of paths is the derivative of the structure's type, in the sense of calculus.
• Church encodingChurch encoding represents data in the pure lambda calculus, which has only functions, by functions: a natural number n is the function that applies its argument n times, a boolean is a function choosing between two alternatives, and a pair is a function waiting for a selector. In general a value is represented by its own fold. Arithmetic, logic and data structures all become lambda terms, which is how the lambda calculus was shown to express every computable function; in typed form the encoding needs polymorphism, as in System F.
• Scott encodingRepresenting data by its case analysis rather than its fold: a Scott numeral takes what to do for zero and what to do with the predecessor. Pattern matching and the predecessor take one step; iteration needs recursion from outside, such as a fixed-point combinator.
• CurryingCurrying turns a function of several arguments into a chain of functions of one argument each: f : A * B -> C becomes curry f : A -> (B -> C). The two forms are in one-to-one correspondence, which in mathematics is the exponential law C^(A*B) = (C^B)^A. In OCaml and Haskell every function is curried, so partial application, supplying only some of the arguments, is ordinary.
• BoxingBoxing is storing a value in a separately allocated heap block and handling it through a pointer to that block. Polymorphic languages box values so that every value fits in one machine word and generic code can copy and pass any value the same way; OCaml boxes floats, tuples and other structured values but keeps small integers and constant constructors unboxed as tagged words. The cost is an allocation and an indirection per value, which compilers avoid where they can by unboxing values whose type is known.
• CatamorphismA catamorphism is the generalization of fold from lists to any recursive data type: it replaces each constructor of a value with a function and combines the results bottom up. Formally it is the unique homomorphism from the initial algebra of a functor to any other algebra of that functor. Writing a recursive data type as the fixed point of a base functor lets a single cata function fold every such type, with the recursion written once and each computation reduced to an algebra that handles one layer.
• Red-black treeA red-black tree is a binary search tree whose nodes are coloured red or black so that no red node has a red child and every path from the root to a leaf passes through the same number of black nodes. The two rules keep the height at most 2 log2(n + 1), so search, insertion and deletion take O(log n) time. Red-black trees are an encoding of 2-3-4 trees as binary trees, and Okasaki's functional version reduces insertion to one rebalancing rule with four cases.
• SemigroupA semigroup is a set with an associative binary operation, with no requirement of an identity element. Maximum and minimum, union of bounding boxes, concatenation of non-empty lists and "keep the first" are semigroups that are not monoids. Associativity alone allows a non-empty sequence to be combined in any bracketing, and n copies of an element to be combined in O(log n) operations by repeated squaring. Adjoining an identity turns any semigroup into a monoid.

1. [1]R. M. Burstall, D. B. MacQueen, D. T. Sannella, “HOPE: an experimental applicative language”, LISP Conference (1980).
2. [2]R. M. Burstall, “Design considerations for a functional programming language”, Infotech State of the Art Conference (1977).
3. [3]B. C. Pierce, Types and Programming Languages, ch. 11 and 20, MIT Press (2002).
4. [4]L. Maranget, “Warnings for pattern matching”, Journal of Functional Programming 17 (2007).
5. [5]L. Augustsson, “Compiling pattern matching”, FPCA (1985).
6. [6]P. Wadler, “The expression problem”, message to the java-genericity mailing list (1998).
7. [7]C. McBride, “The derivative of a regular type is its type of one-hole contexts” (2001).
8. [8]Y. Minsky, “Effective ML”, lecture at Harvard (2010); the maxim “make illegal states unrepresentable”.

last updated 27 September 2026