Prereqs: ๐ Ch. 5 (Products and Coproducts). 8 min.
Types form a semiring. Product types are multiplication, sum types are addition, Void is 0, Unit is 1. The same algebraic identities you learned in grade school โ a ร 1 = a, a + 0 = a, distributivity โ hold for types up to isomorphism. A type definition is an equation you can solve.
Product types are multiplication
A pair (a, b) is the product of two types. It contains a value of type aand a value of type b. The number of inhabitants of a pair is the product of the inhabitants of each component. Pairs are commutative and associative up to isomorphism, just like multiplication.
Scheme
; Product type: a pair holds one value from each type.; Inhabitants of (Bool, Bool) = 2 * 2 = 4
(define (enumerate-pairs as bs)
(apply append
(map (lambda (a)
(map (lambda (b) (list a b)) bs))
as)))
(define bools '(#t#f))
(display "Bool ร Bool: ")
(display (enumerate-pairs bools bools)) (newline)
; 4 inhabitants; Pairs are commutative: (a, b) โ (b, a)
(define (swap p) (list (cadr p) (car p)))
(display "swap (1, #t): ")
(display (swap '(1#t))) (newline)
; Pairs are associative: ((a, b), c) โ (a, (b, c))
(define (assoc p)
(list (car (car p)) (cadr (car p)) (cadr p)))
(display "flatten ((1, 2), 3): ")
(display (assoc '((12) 3)))
A record (or struct) is a product type with named fields. Instead of remembering that the first element is the name and the second is the atomic number, you give each field a label. The algebra is the same: it's still multiplication.
Scheme
; Records = named products.; Haskell: data Element = Element { name :: String, symbol :: String, atomicNumber :: Int }
(define (make-element name symbol number)
(list 'element name symbol number))
(define (element-name e) (list-ref e 1))
(define (element-symbol e) (list-ref e 2))
(define (element-number e) (list-ref e 3))
(define hydrogen (make-element "Hydrogen""H"1))
(define helium (make-element "Helium""He"2))
(display (element-name hydrogen)) (display " (")
(display (element-symbol hydrogen)) (display "), Z=")
(display (element-number hydrogen)) (newline)
(display (element-name helium)) (display " (")
(display (element-symbol helium)) (display "), Z=")
(display (element-number helium))
Sum types are addition
A sum type Either a b holds a value of type aor a value of type b, tagged so you can tell which. The number of inhabitants is the sum. Bool is 1 + 1: two tags, no payload.
Scheme
; Sum type: Either a b = Left a | Right b; Inhabitants of Either Bool Unit = 2 + 1 = 3
(define (left x) (list 'left x))
(define (right x) (list 'right x))
(define (left? e) (eq? (car e) 'left))
(define (either on-left on-right e)
(if (left? e) (on-left (cadr e)) (on-right (cadr e))))
; Bool = 1 + 1 (two tags, no data)
(define true-val (left '()))
(define false-val (right '()))
(display "true tag: ") (display true-val) (newline)
(display "false tag: ") (display false-val) (newline)
; Either Bool () has 3 inhabitants
(define inhabitants
(list (left #t) (left #f) (right '())))
(display "Either Bool () inhabitants: ")
(display (length inhabitants)) (display " -> ")
(display inhabitants)
Python
# Sum types via tagged tuplesdef Left(x): return ("left", x)
def Right(x): return ("right", x)
def either(on_left, on_right, e):
tag, val = e
return on_left(val) if tag == "left"else on_right(val)
# Bool = 1 + 1
true_val = Left(())
false_val = Right(())
print(f"true: {true_val}")
print(f"false: {false_val}")
# Either Bool () = 2 + 1 = 3 inhabitants
inhabitants = [Left(True), Left(False), Right(())]
print(f"Either Bool () has {len(inhabitants)} inhabitants")
The algebra: Void is 0, Unit is 1
Void (no inhabitants) is the additive identity: a + 0 โ a. Unit (one inhabitant) is the multiplicative identity: a ร 1 โ a. Multiplying by Void annihilates: a ร 0 โ 0. These are the axioms of a semiring.
Scheme
; The type algebra:; Void = 0 (no inhabitants); Unit = 1 (one inhabitant: '()); Bool = 2 (= 1 + 1); a + 0 โ a (Either a Void โ a); a ร 1 โ a ((a, ()) โ a); a ร 0 โ 0 ((a, Void) โ Void); a ร 1 โ a: pairing with unit adds no information
(define (pair-with-unit x) (list x '()))
(define (drop-unit p) (car p))
(display "pair: ") (display (pair-with-unit 42)) (newline)
(display "drop: ") (display (drop-unit (pair-with-unit 42))) (newline)
; round-trip: 42 -> (42 ()) -> 42; a + 0 โ a: Either a Void โ the Right case can never happen; So every value must be Left a, which is just a with a tag.
(define (inject x) (list 'left x))
(define (project e) (cadr e))
(display "inject 7: ") (display (inject 7)) (newline)
(display "project: ") (display (project (inject 7))) (newline)
; Bool = 1 + 1 = 2
(display "Bool has ") (display (+ 11)) (display " inhabitants")
Maybe a = 1 + a
Maybe a is Nothing | Just a, which is 1 + a. It adds one extra value (Nothing) to any type. Maybe Bool has 1 + 2 = 3 inhabitants: Nothing, Just True, Just False. This is Either () a.
Scheme
; Maybe a = Nothing | Just a = 1 + a
(define nothing 'nothing)
(define (just x) (list 'just x))
(define (nothing? x) (eq? x 'nothing))
(define (maybe default f m)
(if (nothing? m) default (f (cadr m))))
; Maybe Bool = 1 + 2 = 3 inhabitants
(define maybe-bools (list nothing (just #t) (just #f)))
(display "Maybe Bool: ") (display maybe-bools) (newline)
(display "count: ") (display (length maybe-bools)) (newline)
; Maybe is isomorphic to Either () a
(define (maybe->either m)
(if (nothing? m)
(list 'left '())
(list 'right (cadr m))))
(display "Nothing -> ") (display (maybe->either nothing)) (newline)
(display "Just 42 -> ") (display (maybe->either (just 42))) (newline)
; Safe division returns Maybe
(define (safe-div a b)
(if (= b 0) nothing (just (/ a b))))
(display "10/3: ") (display (safe-div 103)) (newline)
(display "10/0: ") (display (safe-div 100))
Python
# Maybe a = 1 + a โ Python uses None as Nothingdef safe_div(a, b):
returnNoneif b == 0else a / b
print(f"10/3 = {safe_div(10, 3)}")
print(f"10/0 = {safe_div(10, 0)}")
# Maybe Bool = {None, True, False} = 3 inhabitants
maybe_bools = [None, True, False]
print(f"Maybe Bool: {maybe_bools} ({len(maybe_bools)} values)")
Distributivity: a ร (b + c) = a ร b + a ร c
Products distribute over sums, just like multiplication distributes over addition. A pair of (a, Either b c) is isomorphic to Either (a, b) (a, c). This is a real isomorphism: two functions that are inverses of each other.
Scheme
; Distributivity: a ร (b + c) โ (a ร b) + (a ร c); (a, Either b c) โ Either (a, b) (a, c)
(define (prod->sum p)
(let ((a (car p)) (e (cadr p)))
(if (eq? (car e) 'left)
(list 'left (list a (cadr e)))
(list 'right (list a (cadr e))))))
(define (sum->prod s)
(let ((pair (cadr s)))
(if (eq? (car s) 'left)
(list (car pair) (list 'left (cadr pair)))
(list (car pair) (list 'right (cadr pair))))))
; Round-trip test
(define test-val (list "x" (list 'left 42)))
(display "original: ") (display test-val) (newline)
(display "prod->sum: ") (display (prod->sum test-val)) (newline)
(display "round-trip: ") (display (sum->prod (prod->sum test-val))) (newline)
(display "match? ") (display (equal? test-val (sum->prod (prod->sum test-val))))
Lists: solving an equation with types
A list is either empty or a head element followed by a tail list: List a = Nil | Cons a (List a). As an equation: x = 1 + a ร x. Expand it: x = 1 + a + aยฒ + aยณ + .... A list is either empty (1), one element (a), two elements (aยฒ), three (aยณ), and so on. The algebra predicts the structure.
Scheme
; List a = 1 + a ร List a; Nil = 1 (empty list), Cons a (List a) = a ร List a; Equation: x = 1 + a*x; Solution: x = 1 + a + a^2 + a^3 + ...; Scheme lists already are this:; '() = Nil (the 1); (cons head tail) = Cons head tail (the a ร x); Count inhabitants of List Bool up to length 3:; length 0: 1 way (empty list); length 1: 2 ways (T) (F); length 2: 4 ways (TT) (TF) (FT) (FF); length 3: 8 ways; Total = 1 + 2 + 4 + 8 = 15 (= 2^0 + 2^1 + 2^2 + 2^3)
(define (lists-of-length items n)
(if (= n 0) '(())
(apply append
(map (lambda (rest)
(map (lambda (item) (cons item rest))
items))
(lists-of-length items (- n 1))))))
(display "length 0: ") (display (length (lists-of-length '(#t#f) 0))) (newline)
(display "length 1: ") (display (length (lists-of-length '(#t#f) 1))) (newline)
(display "length 2: ") (display (length (lists-of-length '(#t#f) 2))) (newline)
(display "length 3: ") (display (length (lists-of-length '(#t#f) 3))) (newline)
(display "total up to 3: ") (display (+ 1248))
; 1 + a + a^2 + a^3 with a=2
Python
# List a = 1 + a * List a# x = 1 + a*x => x = 1 + a + a^2 + a^3 + ...fromitertoolsimport product
def lists_of_length(items, n):
returnlist(product(items, repeat=n))
bools = [True, False]
for n inrange(4):
count = len(lists_of_length(bools, n))
print(f"length {n}: {count} lists")
total = sum(len(lists_of_length(bools, n)) for n inrange(4))
print(f"total up to length 3: {total}")
# 1 + 2 + 4 + 8 = 15
The semiring of types
Putting it all together. Types and their operations satisfy the same laws as natural numbers with addition and multiplication. This is not a metaphor. It's a semiring isomorphism.
Type
Algebra
Identity
Example
Product (A × B)
Multiplication
Unit (1)
(Int, Bool)
Sum (A + B)
Addition
Void (0)
Either Int Bool
Function (A -> B)
Exponentiation
--
Int -> Bool
Scheme
; The semiring of types:;; Numbers Types Law; ------- ----- ---; 0 Void additive identity; 1 () multiplicative identity; a + b Either a b sum type; a ร b (a, b) product type; a + 0 = a Either a Void โ a additive identity; a ร 1 = a (a, ()) โ a multiplicative identity; a ร 0 = 0 (a, Void) โ Void annihilation; a(b+c) = ab+ac distributivity; 2 = 1+1 Bool two constructors; 1 + a Maybe a optional value;; Verify: Bool ร Bool ร Bool = 2 ร 2 ร 2 = 8
(define (all-triples items)
(apply append
(map (lambda (a)
(apply append
(map (lambda (b)
(map (lambda (c) (list a b c)) items))
items)))
items)))
(define triples (all-triples '(#t#f)))
(display "Bool^3 = ") (display (length triples)) (display " inhabitants")
(newline)
; Maybe (Maybe Bool) = 1 + (1 + 2) = 4
(define mmb (list 'nothing
(list 'just 'nothing)
(list 'just (list 'just #t))
(list 'just (list 'just #f))))
(display "Maybe (Maybe Bool) = ") (display (length mmb))
The blog post uses Haskell algebraic data types and C++ structs/unions. This page uses Scheme tagged lists for sum types and plain lists for product types. The key insight translates directly: counting inhabitants of a type follows the same arithmetic as the type's algebraic expression. Haskell enforces these types at compile time; Scheme relies on tagging conventions. The algebra is the same either way.
Ready for the real thing? Read the blog post. The semiring table is in the middle. The list equation at the end is worth staring at.
Algebraic data type