Algebraic data type

A type built from sums (a value is one of several cases) and products (a value has several fields at once), possibly recursively. The name comes from counting: the number of values of a sum is the sum of the counts, and of a product the product, so types obey the laws of algebra.

Write $∣ T ∣$ for the number of values of a type. Then

∣ A + B ∣ = ∣ A ∣ + ∣ B ∣ ∣ A \times B ∣ = ∣ A ∣ \cdot ∣ B ∣ ∣ A \to B ∣ = ∣ B ∣^{∣ A ∣} ∣ 1 ∣ = 1 ∣ 0 ∣ = 0

with unit as $1$ and an empty variant as $0$ . bool is $1 + 1$ , 'a option is $1 + a$ , and there are $2^{2} = 4$ functions bool -> bool. The laws of arithmetic hold as isomorphisms, and each is a pair of inverse functions:

A \times (B + C) ≅ A \times B + A \times C A^{B + C} ≅ A^{B} \times A^{C} (A^{B})^{C} ≅ A^{B \times C}

The last is currying. Recursive types are fixed points: a list is $L = 1 + a \times L$ , which unfolds to $1 + a + a^{2} + a^{3} + \dots$ , a list of length 0, 1, 2, and so on.

A sum of products, a variant whose cases carry only the data that exists in that state, and the distributive law as code.

(* Sum: one of several cases. Product: several fields at once. *)
type shape = Circle of float | Rect of float * float
 
let area = function Circle r -> Float.pi *. r *. r | Rect (w, h) -> w *. h
 
(* Making illegal states unrepresentable: an address exists only when
   connected, a retry count only while retrying. *)
type connection =
  | Disconnected
  | Connecting of { attempt : int }
  | Connected of { address : string }
 
let describe = function
  | Disconnected -> "disconnected"
  | Connecting { attempt } -> Printf.sprintf "connecting (attempt %d)" attempt
  | Connected { address } -> "connected to " ^ address
 
(* A x (B + C) = A x B + A x C, as a pair of inverse functions. *)
let distribute : 'a * ('b, 'c) Either.t -> ('a * 'b, 'a * 'c) Either.t = function
  | a, Left b -> Left (a, b)
  | a, Right c -> Right (a, c)
 
let factor : ('a * 'b, 'a * 'c) Either.t -> 'a * ('b, 'c) Either.t = function
  | Left (a, b) -> (a, Left b)
  | Right (a, c) -> (a, Right c)

Running it.

area (Rect (2., 3.))                 ->  6
describe                             ->  disconnected
describe                             ->  connecting (attempt 2)
describe                             ->  connected to 10.0.0.1
factor (distribute v) = v for all v  ->  true

Pattern matching takes a sum apart, and the compiler checks that every case is handled. Leaving one out is a warning, with an example of the value that is missed:

A match on connection that forgets Connecting.

File "adt_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 _

That check is what makes a variant like connection useful: when a case is added later, every match that does not handle it is reported. A record of optional fields could represent the same states, plus combinations that should not exist, such as an address while disconnected; the sum type rules them out by construction.