Equational Reasoning: Proving, Not Just Testing

QuickCheck checks a property on a hundred random cases and calls that good evidence. This chapter goes one step further, the way Hutton's own textbook insists on: proving a property holds for every possible list, using nothing but substitution and one genuinely simple pattern — structural induction — borrowed directly from Immutability's own promise that a binding is an equation, true forever.

From testing to proving

Chapter 5 opened with a promise this book has leaned on ever since without quite cashing in: a Haskell binding is an equation, true forever, not an instruction that runs once and is forgotten. QuickCheck (Chapter 21) already took that promise seriously enough to generate a hundred random test cases and check a property holds on all of them — genuinely useful, but still fundamentally a sample, not a guarantee. This chapter takes the promise the rest of the way: since Haskell definitions are real equations, they can be manipulated with exactly the substitution-and-algebra habits from school mathematics, to prove a property holds for every possible input, not just the ones QuickCheck happened to try.

A warmup with no induction at all

Some equalities need nothing more than substituting definitions in and simplifying — ordinary algebra, no special machinery:

double :: Int -> Int
double x = x + x

double' :: Int -> Int
double' x = 2 * x

To show double x = double' x for every x, substitute both definitions and simplify:

$\text{double}\ x = x + x = 2 \times x = \text{double}'\ x$

x + x = 2 * x is just distributivity, true for every x by ordinary arithmetic — no case analysis, no recursion, nothing beyond “substitute the definition, then simplify.” Most equational proofs about recursive structures need one more tool, though, because a list’s definition refers to itself.

Structural induction: the pattern

A list is built exactly one of two ways: it’s [], or it’s x : xs for some element x and a smaller list xs. Structural induction proves a property P holds for every list by matching that exact shape:

Base case — prove P([]) holds.
Inductive step — assume P(xs) holds (the induction hypothesis), and use that assumption to prove P(x:xs) holds.

A recursive function's two cases mirrored against an inductive proof's base case and inductive step — **Figure:** The base case matches the base constructor, the inductive step matches the recursive constructor — a proof by structural induction has exactly the shape of the recursive function it’s proving something about.

That’s not a coincidence worth glossing over: a recursive function defined by pattern-matching on [] and (x:xs) and a proof by induction on the exact same two cases are, structurally, the identical shape. If you can write foldr-style recursion, you already know how to organize an inductive proof — the two skills are the same skill, aimed in different directions.

Proof: associativity of `++`

(xs ++ ys) ++ zs = xs ++ (ys ++ zs) has been used silently, constantly, throughout this book — worth actually proving once, using nothing but ++’s own two-case definition:

(++) :: [a] -> [a] -> [a]
[]     ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)

Base case (xs = []):

$([\,] ++ ys) ++ zs = ys ++ zs = [\,] ++ (ys ++ zs)$

Both sides reduce to ys ++ zs directly from ++’s first equation — nothing left to prove.

Inductive step (xs = x:xs', assuming (xs' ++ ys) ++ zs = xs' ++ (ys ++ zs) as the induction hypothesis):

\begin{aligned} ((x{:}xs') ++ ys) ++ zs &= (x : (xs' ++ ys)) ++ zs && \text{[def of ++]}\\ &= x : ((xs' ++ ys) ++ zs) && \text{[def of ++]}\\ &= x : (xs' ++ (ys ++ zs)) && \text{[induction hypothesis]}\\ &= (x{:}xs') ++ (ys ++ zs) && \text{[def of ++, backward]} \end{aligned}

Every step is either applying ++’s own definition or invoking the induction hypothesis exactly once — no cleverness beyond substitution, applied patiently.

Proof: the Functor laws for lists, finally proven

Chapter 9 stated the Functor laws — fmap id = id and fmap (f . g) = fmap f . fmap g — as properties an instance is expected to satisfy, checked with QuickCheck in Chapter 21, but never actually proven. For lists, fmap is map, and both laws fall to the identical induction pattern:

map id xs = xs:

Base case: map id [] = [] , matching [] directly.

Inductive step (assuming map id xs' = xs'):

\text{map id } (x{:}xs') = \text{id } x : \text{map id } xs' = x : xs' = (x{:}xs')

map (f . g) xs = (map f . map g) xs:

Base case: both sides reduce to [] directly.

Inductive step (assuming map (f.g) xs' = (map f . map g) xs'):

\begin{aligned} \text{map } (f.g)\ (x{:}xs') &= f(g\ x) : \text{map } (f.g)\ xs' && \text{[def of map, def of (.)]}\\ &= f(g\ x) : (\text{map } f \cdot \text{map } g)\ xs' && \text{[induction hypothesis]}\\ &= (\text{map } f \cdot \text{map } g)\ (x{:}xs') && \text{[def of map, unwound]} \end{aligned}

Both laws this book asked you to trust since Chapter 9 are now genuinely established — not just consistent with a hundred random QuickCheck cases, but true for every possible list, proven the same way ++’s associativity was.

★Cool Fact

GHC’s own optimizer exploits exactly these proven equalities directly: the RULES pragma lets library authors tell the compiler "map/map" forall f g xs. map f (map g xs) = map (f . g) xs, and GHC will rewrite matching code at compile time, fusing two list traversals into one. This isn’t a hypothetical use for the proof above — it’s the literal equation, encoded as a real compiler optimization, precisely because someone already proved it’s always true.

⚠Common Pitfall

Structural induction proves a property for every finite list — Laziness’s infinite lists (primes, fibs) sit outside what this technique directly covers, since there’s no base case to start an infinite structure’s induction from. Reasoning rigorously about infinite structures needs a related but distinct tool (coinduction), genuinely outside this chapter’s scope — the proofs here are airtight for the ordinary, finite lists most Haskell code actually works with, not a claim about every value Chapter 6 discussed.

In the Wild

Equational reasoning isn’t confined to textbooks — Haskell’s own standard libraries document Functor, Applicative, and Monad laws explicitly in their source comments, and library authors are expected to either prove their instances satisfy them or have a very good reason to explain why not. Tools like liquidhaskell push this further still, letting a type signature itself encode a property (like “this list is always sorted”) that the compiler checks automatically — proof, not merely testing, built directly into the type system.

λA Category-Theoretic View

This entire technique is itself a small, concrete instance of Curry–Howard (Chapter 4): a property like map id xs = xs is a proposition, and the induction above — base case plus inductive step — is literally a proof term establishing it, built the same way a well-typed program is a proof of the type it inhabits. Proving a Haskell equation and writing a well-typed Haskell program are, underneath, the same kind of act.

QuickCheck and equational reasoning aren’t competitors — they answer different questions at different costs. QuickCheck is fast, automatic, and good at catching a wrong conjecture before you waste an afternoon trying to prove something false. Equational reasoning is slower and requires actually understanding why a property holds, but it’s the only one of the two that ends in certainty. Immutability’s opening promise — an equation, true forever — was never just a nice way to talk about Haskell. It’s the literal reason proofs like these are even possible.