Practicing derivations

Derivations.md

Derivations are the bread and butter of functional programming. It is easy to fall into the trap of thinking it is a pointless academic exercise, which is the reason why a lot of people struggle with FP. Functional programs are not so much written, they're calculated. It is here that the true power of equational reasoning (i.e. being able to swap the left and right parts of an equation everywhere in the code) help us.

So, getting comfortable reading and doing derivations is a must for any FP practitioner.

Below are the ones we did in the previous sessions, plus a couple of exercises.

Fold fusion

The fold fusion law states that g . foldr f a = foldr h b, but it has provisos. Here we discover what they are by induction on the input:

Base case: undefined

The left hand side:

g (foldr f a undefined)
= {- definition of fold -}
g undefined

And the right hand side:

foldr h b undefined
= {- definition of fold -}
undefined

Our first proviso, g undefined = undefined. We say that g is strict. In Haskell, it is trivial to have a non-strict function:

foo x = 1

A common mistake people make is to say that Haskell is lazy when in fact it is non-strict.

Base case: []

g (foldr f a [])
= {- definition of foldr -}
g a

foldr h b []
= {- definition of foldr -}
b

Second proviso: g a = b

Inductive case: (x:xs)

g (foldr f a (x:xs))
= {- definition of foldr -}
g (f x (foldr f a xs))
= {- let y = foldr f a xs -}
g (f x y)

foldr h b (x:xs)
= {- definition of foldr -}
h x (foldr h b xs)
= {- inductive assumption -}
h x (g (foldr f a xs))
= {- let y = foldr f a xs -}
h x (g y)

Third proviso: g (f x y) = h x (g y)

We will see an example of the fold fusion in action which will help us take an program from O(n^3) to O(n).

Note that similar laws exist for foldl and all generalisations of folds. If you are into that, search for Jeremy Gibbons's papers on the topic.

fold-map fusion

The law is foldr f a . map g = foldr (f . g) a. In other words, we can get rid of the intermediate structure created between the fold and the map.

Base case: []

foldr f a (map g [])
= {- definition of map -}
foldr f a []
= {- definition of foldr -}
a

and

foldr (f . g) a []
= {- definition of foldr for [] -}
a

The case for undefined is similar.

Inductive case: (x:xs)

foldr f a (map g (x:xs))
= {- definition of map -}
foldr f a (g x : map g xs)
= {- definition of foldr -}
f (g x) (foldr f a (map g xs))
= {- inductive assumption -}
f (g x) (foldr (f . g) a xs)
= {- definition of foldr -}
foldr (f . g) a (x:xs)

👆 The last line shows a derivation when the right-hand side of an equation (the definition of foldr) is swapped with its left-hand side. Equations go in both directions!

foldr (f . g) a (x:xs)
= {- definition of foldr -}
f (g x) (foldr (f . g) a xs)
= {- inductive assumption -}
f (g x) (foldr f a (map g xs))
= {- definition of foldr -}
foldr f a (g x : map g xs)
= {- definition of map -}
foldr f a (map g (x:xs))

Scan lemma

Law: map (foldr f a) . tails = scanr f a. This law turns an expression of complexity O(n^2) on the left to a linear one on the right. The same law in the opposite direction is map (foldl f a) . inits = scanl f a, which is more common.

First, some definitions:

scanr :: (a -> b -> b) -> b -> [a] -> [b]
scanr f a [] = [a]
scanr f a (x:xs) = let ys = scanr f a xs in f x (head ys) : ys

tails :: [a] -> [[a]]
tails [] = [[]]
tails xs = xs : tails (tail xs)

Base case: []

map (foldr f a) (tails [])
= {- definition of tails -}
map (foldr f a) [[]]
= {- definition of map -}
[foldr f a []]
= {- definition of foldr -}
[a]

and

scanr f a []
= {- definition of scanr -}
[a]

Inductive case: (x:xs)

map (foldr f a) (tails (x:xs))
= {- definition of tails -}
map (foldr f a) ((x:xs) : tails xs)
= {- definition of map -}
foldr f a (x:xs) : map (foldr f a) tails xs
= {- inductive assumption -}
foldr f a (x:xs) : scanr f a xs

and

scanr f a (x:xs)
= {- definition of scanr -}
f x (head (scanr f a xs)) : scanr f a xs
= {- inductive assumption -}
f x (head (map (foldr f a) (tails xs)) : scanr f a xs
= {- head . map f = f . head -}
f x (foldr f a) (head (tails xs)) : scanr f a xs
= {- head . tails = id -}
f x (foldr f a) xs : scanr f a xs
= {- definition of foldr -}
foldr f a (x:xs) : scanr f a xs

👆 This derivation shows that sometimes all you need to do is move forward with a derivation from both sides until you end up with the same result.

map-filter interaction

Law: filter p . map f = map f . filter (p . f). Some laws are only ever helpful in other derivations, this is one example.

In this case it is not necessary to prove the law by induction on the input. All we need is to perform a few program substitutions:

filter p . map f 
= {- definition of filter -}
concat . map (test p) . map f
= {- functor law -}
concat . map (test p . f)
= {- test p . f = map f . test (p . f) -}
concat . map (map f . test (p . f))
= {- functor law -}
concat . map (map f) . map (test (p . f))
= {- concat . map (map f) = map f . concat -}
map f . concat . map (test (p . f))
= {- definition of filter -}
map f . filter (p . f)

Fork laws

It is sometimes necessary to perform two actions on a single input. In fact, this pattern is abstracted in many places: bifunctors, categories, profunctors, etc. Here we focus our attention to the (->) bifunctor, aka the belove function.

Some definitions:

fork :: (a -> b, a -> c) -> a -> (b, c)
fork (f,g) x = (f x, g x)

cross :: (a -> c, b -> d) -> (a, b) -> (c, d)
cross (f,g) = fork (f . fst, g . snd)

unzip :: [(a, b)] -> ([a], [b])
unzip = fork (map fst, map snd)

fork and cross come with a list of laws of their own, which I leave as an exercise:

cross (id, id) = id
fst . cross (f, g) = f . fst
snd . cross (f, g) = g . snd
cross (f, g) . fork (h, i) = cross (f . h, g . i)
fork (f . h, g . h) = fork (f, g) . h

Law: cross (map f, map g) . unzip = unzip . map (cross (f, g))

cross (map f, map g) . unzip
= {- definition of unzip -}
cross (map f, map g) . fork (map fst, map snd)
= {- cross (f,g) . fork (h,i) = cross (f . h, g . i) -}
fork (map f . map fst, map g . map snd)
= {- functor law -}
fork (map (f . fst), map (g . snd))
= {- fst . cross (f, g) = f . fst, snd . cross (f, g) = g . snd -}
fork (map (fst . cross (f, g)), map (snd . cross (f, g)))
= {- functor law -}
fork (map fst . map (cross (f, g))), map snd . map (cross (f, g))))
= {- fork (f . h, g . h) = fork (f, g) . h -}
fork (map fst, map snd) . map (cross (f, g))
= {- definition of unzip -}
unzip . map (cross (f, g))

The most difficult part (at least afaic) is which law to choose when. It requires creativity and insight ... both things that come with practice ✌️