Derivations and partiality

foldr.md

We saw that every data type is inhabited by a value ⊥ pronounced "bottom". It is very important in a non-strict language such as Haskell to represent how much knowledge you have about a value. You can either know exactly what the value is, know only a part of it, or know nothing at all. Bottom represents the latter, but you could as well only know that a list starts with 1, i.e. 1 : ⊥.

In fact, all data types in Haskell respect an approximation function ⊑, where x ⊑ y means "x is an approximation of y". For example with booleans, x ⊑ y iff ⇔ x ≡ ⊥ or x ≡ y in other words either you don't know anything about a particular boolean, or you know exactly what it is. This approximation ordering is important when reasoning about recursive algorithms, which is why it is important to understand the notion of "nothingness" in Haskell.

In the next session we'll see talk about cyclic data structures and fixed points, where it plays a big role.

Exercise for next session

The fusion law of map is well known and is commonly used to reduce the runtime complexity of an algorithm:

map f . map g = map (f . g)

Folds and unfolds have similar laws. The foldr fusion law states that

g . foldr f a = foldr h b

provided three properties are satisfied.

Can you find out what these properties are? To do that, prove that the equality holds for all lists.

Example of a derivation

Just wanted to provide an example of how to do it. Given the following definition of reverse:

reverse [] = []
reverse (x:xs) = reverse xs ++ [x]

We want to prove the following law holds:

reverse (reverse xs) == xs

Case undefined

reverse (reverse undefined)
= {- no match in the definition of reverse -}
reverse undefined
= {- again -}
undefined

Case []

reverse (reverse [])
= {- definition of reverse -}
reverse []
= {- again -}
[]

Case (x:xs)

reverse (reverse (x:xs))
= {- def of reverse -}
reverse (reverse xs ++ [x])
= {- we claim reverse (xs ++ [x]) = x : reverse xs -}
reverse (x:reverse xs)
= {- definition of reverse -}
reverse (reverse xs) ++ [x]
= {- claim -}
x:reverse (reverse xs)
= {- induction hyposethis -}
x:xs

The claim above can be proved similarly.

A couple more

If you blasted through the foldr derivation, here are a few others that should be a piece of cake (in fact, you might need some of them to do the foldr derivation 😬).

foldr f a . map g            = foldr (f . g) a
map (foldr f a) . tails      = scanr f a
map f . concat               = concat . map (map f)
map f . tail                 = tail . map f
f . head                     = head . map f
filter p . map f             = map f . filter (p . f)
cross (map f, map g) . unzip = unzip . map (cross (f, g))

Some definitions for reference:

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)

filter :: (a -> Bool) -> [a] -> [a]
filter p = concat . map (test p)
  where test p x = if p x then [x] else []

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)