Equational Reasoning Shopping List

Pure functional programming has the advantage that one can reason with it very like one does in mathematics. Specifically, if you know two expressions to be equal, they can be freely swapped. This underlies the use of inlining, sharing and the ability to replace any linear recursion with a fold, unfold, zip, etc. as appropriate.

As a first Haskell example, consider the following very-well-known optimization. Given code like

map f $ map g $ map h list

or in the more common style:

map f . map g . map h $ list

it appears naively that this will traverse the list three times: once to apply h, again to apply g, and finally a third time to apply f.

But because map, f, g and h are all pure functions, they can be replaced with something equivalent without changing the result of the code.

Consider an element of list, say x. After the three maps, it will have been replaced in the final list with f(g(h x))), or equivalently f . g . h $ x. So we should be able to replace the three maps with one that does the same thing:

map (f . g . h) list

And in fact GHC does precisely this.

Equational Rules
Following is a collection (and more are most welcome!) of rules for transforming your programs. I have written their equality with ==, though of course Haskell functions are not in Eq. I have written implication as –> and equivalence/double-implication as <–>.

map f . map g == map (f . g)
filter f . filter g     == filter (\x -> f x && g x)
                        == filter (liftM2 (&&) f g)
f . f == id --> filter (p . f) == map f . filter p . map f
filter (all p) . cartesianProduct == cartesianProduct . map (filter p)
filter p . concat == concat . map (filter p) == concatMap (filter p)

And now some concerning pairs and arrow combinators, Haskell translations of ones from Meijer et al.’s seminal paper:

fst . (f *** g) == f . fst
fst . (f &&& g) == f
-- and the obvious equivalents for snd and g.
fst . h &&& snd . h == id
fst &&& snd == id
(f *** g) . (h &&& j) == (f . h) &&& (g . j)
(f &&& g) . h == (f . h) &&& (g . h)
(f *** g) == (h *** j) <--> f == h && g == j
(f &&& g) == (h &&& j) <--> f == h && g == j

And more, translated from the same paper, for Either and the arrow combinators using it:

(f +++ g) . Left == Left . f
(f ||| g) . Left == f
-- and the obvious equivalents for g and Right
{- h strict -} --> (h . Left) ||| (h . Right) == h
Left ||| Right == id
(f ||| g) . (h +++ j) == (f . h) ||| (g . j)
{- f strict -} --> f . (g ||| h) == (f . g) ||| (f . h)
(f ||| g) == (h ||| j)  f == h && g == j
(f +++ g) == (h +++ j)  f == h && g == j

And finally the “Abides Law” tying the two together:

(f &&& g) ||| (h &&& j) == (f ||| h) &&& (g ||| j)

There are many more such rules, and if you have more to suggest I’d love to add them to the list.