*(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`

.