This is an exercise found in the very good book of Richard Bird, Thinking Functionally with Haskell. It is a good example of how a certain method of thinking can help us to reason about programs in functional programming. The method is called equational reasoning: it lets you transform consistently (based on mathematical functional equations) some functions into another ones (sometimes with a large gain in efficiency).

A first example of a law is the map fusion: given any two functions f,g that are composable, map(f . g) = map f . map g (by the “.” sign we mean functional composition). You can find more about the map function in my earlier post: A little bit of recursion – the map function.

The proof of this law is left as an exercise. You can prove it element by element, applying map(f.g) on the fixed general list [a1,…,an], where a1,..,an are elements from a fixed type a.

Remark. We observe that the fusion law for the map function says that you can loop through a list once and apply f.g on every element on the list — or you can loop on the whole list and apply g, then loop again on the output list and apply f. It’s obvious that this law applied only once per list gives a lot of gain in efficiency (think about a list with several millions of elements, or even more).

That being said, we are asked to prove the following equation: cross(map f,map g) . unzip = unzip . map (cross(f,g)).

We are given the definitions:

  1. cross function definition: cross(f,g) = fork(f . fst,g . snd)
  2. unzip function definition: unzip = fork(map fst, map snd)
  3. fork function definition: fork :: (a->b , a->c) -> a -> (b,c); fork (f,g) x = (f x, g x)
  4. fst function definition: fst :: (a,b) -> a; fst(x,y) = x
  5. snd function definition: snd :: (a,b) -> b; snd(x,y) = y

We are given the following equational laws:

  1. Law 1 (cross and fork composition by “components”): cross(f,g) . fork(h,k) = fork(f . h, g . k)
  2. Law 2 (fork fusion law): fork(f,g) . h = fork(f . h, g . h)
  3. Law 3: fst . cross(f,g) = f.fst
  4. Law 4: snd . cross(f,g) = g.snd

We restate what we have to prove:

Lemma.  cross(map f,map g) . unzip = unzip . map (cross(f,g))

Proof. 

cross(map f, map g) . unzip

= {using unzip function definition} cross(map f, map g).fork(map fst, map snd)

= {using Law 1 of cross and fork composition} fork(map f . map fst, map g . map snd)

= {using the map fusion law} fork(map(f . fst), map(g . snd))

= {using Law 3 and Law 4} fork( map(fst . cross(f,g)) , map(snd . cross(f,g)) )

= {using the map fusion law} fork( map fst . map (cross (f,g)) , map snd . map (cross (f,g)) )

= {using Law 2 – fork fusion law} fork(map fst, map snd) . map (cross (f,g))

={unzip definition}

unzip . map (cross (f,g))

End of Proof.

As you can see, the equational reasoning is a very powerful method to prove equational laws. And sometimes, as in the map fusion law, it can lead to optimizations that in other languages are almost impossible to see or prove.

P.S. You can take a look on my page on Patreon (click this text).

Constantin Liculescu

Facebook 

Share Button