## 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.

### 2 Responses to Equational Reasoning Shopping List

1. Nathan Stien says:

I discovered your blog from HWN and it looks to be pretty dang useful.

But I have a request: Would it be possible for you to disable automatic smileys in your blog template? WordPress has inconsiderately obscured some of your code with a bitmap smiley (on the line with filter and liftM2).