◄ WORLD V · SONNY 5DART 246 · a helldive at the net

THE ALGEBRAIC DATA TYPE types you add and multiply — and match to take apart

An algebraic data type is built from two operations: sum (a choice — this OR that, a tagged union) and product (a pair — this AND that, a record). Maybe a = None | Some a is a sum; (a, b) is a product. The payoff is pattern matching: because the type enumerates its shapes, the compiler knows every case and can force you to handle all of them — the dreaded “forgot a case” bug becomes a compile error. Sums and products are the whole grammar; every data structure is some algebra of them.

THE TECHNIQUE sum (tagged choice) + product (pair); match on the tag

A list of Maybe values, each tagged None(0) or Some(1). The demo matches on the tag and sums only the Some payloads: live demo

HISTORY & CREDIT HOPE 1980 · SML mid-80s

“A union is just a struct with a tag you check by hand.” — when the type is the enumeration of shapes, the checking is the compiler's job, not yours, and a missed case is caught before the program runs. The algebra is what makes the match exhaustive. cited

1965 · Tony Hoare — records; Landin, structured values.
1980 · Burstall, MacQueen & Sannella (HOPE) — datatypes with named constructors and clausal pattern matching: the modern algebraic data type. (Original ML, ~1973, gave Hindley-Milner inference + first-class functions, not constructors; ADTs reached the ML family via Standard ML, mid-1980s.)
now · Haskell data, Rust enum, Swift, TypeScript unions — exhaustive matching everywhere.

Sum + product is a closed algebra: |A+B| = |A|+|B|, |A×B| = |A|·|B|. The type literally counts its own inhabitants, and the match must cover them all. ML/Hope

RECOMMEND FOR I-13 sum of the Some payloads, computed

On the canonical compiler, a Maybe list [Some 10, None, Some 20, Some 30] matched by tag sums to 60 — the None contributes nothing:

$ i13 run t_adt.i13 # match tag==Some, sum payloads total = 60 -- Some 10 + Some 20 + Some 30 ; None skipped

Recommend: i13 encodes algebraic data but does not type it — a sum is a [tag, payload] pair in an array, matched with an if on the tag (exactly the demo). What it forgoes is the compiler's exhaustiveness check: nothing forces you to handle None. That is the recurring trade of the whole batch — i13's ledger says types: NOT COVERED, so the shapes are all there at runtime but the “did you miss a case” guarantee is on you, not the validator.