← back

Map from fold

1 February 2017

(This is the standard derivation from Hutton's tutorial on fold, with a minor addition.)


QUESTION

I've been trying to implement map by passing in f as an argument to fold_left, but that doesn't seem to be working because when I implemented fold_left, I assumed the folding function took in 2 arguments as its parameters so I just called f(arg1, arg2).

In map, however, its mapping function only takes in 1 argument so fold_left can't call the folding function in that case. Is there a way to work around that? Or am I just going about fold_left incorrectly?


ANSWER

You need to construct a function g to pass to the fold function, where g uses f.


Using mathematics:

Let's calculate a definition of map in terms of fold. We're going to fuse the definition of map into fold.

map f [] = []
map f (x:xs) = f x : map f xs

We want to solve this equation

map f xs = fold g b xs

=> {eta reduction}

map f = fold g b

THEOREM: universal property of the natural fold on cons lists

f  [] = v
f (x:xs) = g x (f xs)          <=>          f = fold g v

Proof: by induction on the list and the definition of foldr. QED.

=> {apply theorem}

map f      <=>

map f [] = b
map f (x:xs) = g x (map f xs)


=> {first equation, by defn map}

b = []


=> {second equation, by defn map}
f x : map f xs = g x (map f xs)

=> { let ys = map f xs }
f x : ys = g x ys

=> {treat this as a function defn}
g = \x ys -> f x : ys

=> {apply theorem, using g above and b from base case equation}

map f = fold (\x ys -> f x : ys) []

QED.

Now this is for foldr, on lists where elements are prepended and removed from the left, by symmetry

map f = fold (\ys x -> ys ; f x) []   (; is snoc)

holds for lists where elements are appended and removed from the right under foldl.