Equational Reasoning

Equational reasoning is a powerful technique for analyzing and proving properties of functional programs. In pure functional languages like Haskell, it’s particularly effective due to referential transparency. For more on purity and referential transparency, see Expressions and Reduction and Functions and Equations.

The Foundations: Referential Transparency

A program is referentially transparent if any expression can be replaced with its value without changing the program’s behavior. This property is what makes equational reasoning possible and is central to Haskell’s design (Expressions and Reduction).

Basic Principles of Equational Reasoning

Equational reasoning allows us to:

Substitute equals for equals
Transform programs step by step
Prove properties about our code
Optimize implementations

For more on substitution and transformation, see Lambda Calculus and Pattern Matching and Recursion.

Example of Simple Substitution

let x = 5 + 3 in x * 2
= let x = 8 in x * 2
= 8 * 2
= 16

Each step replaces an expression with its equivalent value.

Proof Techniques

Direct Substitution

Directly substitute definitions and simplify:

-- Define a function
double x = x + x
 
-- Prove: double (a + b) = double a + double b
double (a + b)
= (a + b) + (a + b)    -- By definition of double
= a + b + a + b        -- Associativity of (+)
= a + a + b + b        -- Commutativity and associativity of (+)
= double a + double b  -- By definition of double

Induction

For recursive functions and data structures, induction is a powerful technique. For more on recursion and induction, see Pattern Matching and Recursion and Algebraic Data Types.

Example: Proving Length of Append

-- Prove: length (xs ++ ys) = length xs + length ys
 
-- Base case: xs = []
length ([] ++ ys)
= length ys                  -- By definition of (++)
= 0 + length ys             -- By definition of (+)
= length [] + length ys     -- By definition of length
 
-- Inductive case: xs = (x:xs')
-- Assume: length (xs' ++ ys) = length xs' + length ys
 
length ((x:xs') ++ ys)
= length (x:(xs' ++ ys))    -- By definition of (++)
= 1 + length (xs' ++ ys)    -- By definition of length
= 1 + (length xs' + length ys)  -- By induction hypothesis
= (1 + length xs') + length ys  -- By associativity of (+)
= length (x:xs') + length ys    -- By definition of length

Structural Induction

For recursive data types, we use structural induction (Algebraic Data Types).

Example: Tree Depth

data Tree a = Leaf | Node a (Tree a) (Tree a)
 
depth :: Tree a -> Int
depth Leaf = 0
depth (Node _ l r) = 1 + max (depth l) (depth r)
 
-- Prove: depth (mirror t) = depth t
-- where mirror is:
mirror :: Tree a -> Tree a
mirror Leaf = Leaf
mirror (Node x l r) = Node x (mirror r) (mirror l)
 
-- Base case: t = Leaf
depth (mirror Leaf)
= depth Leaf       -- By definition of mirror
= 0                -- By definition of depth
 
-- Inductive case: t = Node x l r
-- Assume: depth (mirror l) = depth l and depth (mirror r) = depth r
 
depth (mirror (Node x l r))
= depth (Node x (mirror r) (mirror l))  -- By definition of mirror
= 1 + max (depth (mirror r)) (depth (mirror l))  -- By definition of depth
= 1 + max (depth r) (depth l)  -- By induction hypothesis
= 1 + max (depth l) (depth r)  -- By commutativity of max
= depth (Node x l r)  -- By definition of depth

Working with Higher-Order Functions

Equational reasoning extends to higher-order functions, which is particularly useful for understanding and optimizing functional code (Higher-Order Functions, Functions and Equations).

Example: Map Fusion

-- Prove: map f (map g xs) = map (f . g) xs
 
-- Base case: xs = []
map f (map g [])
= map f []         -- By definition of map
= []               -- By definition of map
= map (f . g) []   -- By definition of map
 
-- Inductive case: xs = (x:xs')
-- Assume: map f (map g xs') = map (f . g) xs'
 
map f (map g (x:xs'))
= map f (g x : map g xs')    -- By definition of map
= f (g x) : map f (map g xs')  -- By definition of map
= (f . g) x : map f (map g xs')  -- By definition of (.)
= (f . g) x : map (f . g) xs'    -- By induction hypothesis
= map (f . g) (x:xs')  -- By definition of map

Case Studies

Proving Properties of Recursive Functions

For more on recursion and proofs, see Pattern Matching and Recursion.

-- Prove: reverse (reverse xs) = xs
 
-- Base case: xs = []
reverse (reverse [])
= reverse []       -- By definition of reverse
= []               -- By definition of reverse
 
-- Inductive case: xs = (x:xs')
-- Assume: reverse (reverse xs') = xs'
 
reverse (reverse (x:xs'))
= reverse (reverse xs' ++ [x])  -- By definition of reverse
= reverse [x] ++ reverse (reverse xs')  -- reverse distributes over (++)
= [x] ++ xs'        -- By definition of reverse and induction hypothesis
= x:xs'             -- By definition of (:) and (++)

Optimizing with Equational Reasoning

For optimization techniques and laws, see also Evaluation Strategies and Monad Laws.

-- Original function
sum (filter p xs)
 
-- Optimization
sum (filter p (xs ++ ys))
= sum (filter p xs ++ filter p ys)  -- filter distributes over (++)
= sum (filter p xs) + sum (filter p ys)  -- sum distributes over (++)

This optimization allows for parallel computation of the sums.

Common Laws for Standard Functions

Knowing these laws helps in equational reasoning. For more on standard functions and their properties, see Lists and List Comprehensions, Higher-Order Functions, and Property-Based Testing.

List Functions

-- Map laws
map id = id
map f . map g = map (f . g)
 
-- Filter laws
filter p . filter q = filter (\x -> p x && q x)
filter p . map f = map f . filter (p . f)
 
-- Fold laws
foldr f z [] = z
foldr f z (x:xs) = f x (foldr f z xs)
foldr f z (map g xs) = foldr (\x acc -> f (g x) acc) z xs

Functor Laws

-- Identity
fmap id = id
 
-- Composition
fmap f . fmap g = fmap (f . g)

Applicative Laws

-- Identity
pure id <*> v = v
 
-- Composition
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
 
-- Homomorphism
pure f <*> pure x = pure (f x)
 
-- Interchange
u <*> pure y = pure ($ y) <*> u

Monad Laws

-- Left identity
return a >>= f = f a
 
-- Right identity
m >>= return = m
 
-- Associativity
(m >>= f) >>= g = m >>= (\x -> f x >>= g)

Free Theorems

Parametricity in Haskell leads to “free theorems” - properties that must hold based solely on a function’s type signature.

For example, any function of type [a] -> [a] (that doesn’t use undefined or similar) must satisfy:

map f . g = g . map f

for any function f. This is because g can’t inspect, create, or modify the elements - it can only rearrange, drop, or duplicate them.

Tooling Support

Haskell’s ecosystem provides tools to aid equational reasoning:

QuickCheck: Property-based testing to verify equations
LiquidHaskell: Refinement types that can express and verify properties
Coq/Agda integration: For formal verification of Haskell code

Quartz 4

Explorer