[Haskell-cafe] Hand calculation of Bird's definition of zip using foldr

[Ryan Ingram]

2009/3/12 R J <rj248842 at hotmail.com>:
> Part of my problem is that "e" is defined as a function that takes
> one argument, I don't see how that fits in with the usual scheme for foldr,
> which, as I understand it, is:
>
> foldr f e [x1, x2, ...] = f x1 (f x2 (f x3 ...(f xn e)))...

It's pretty easy, actually.  Lets rewrite the type signatures a bit:

> foldr :: (a -> b -> b) -> b -> ([a] -> b)
> zip :: [x] -> [y] -> [(x,y)]
> zip = foldr f e where
>   e _ = []
>   f _ _ [] = []
>   f x g (y:ys) = (x,y) : g ys

So, from the signature for foldr, we can derive:

> f :: (a -> b -> b)
> e :: b
> zip :: [a] -> b

And from the two type signatures for zip, we derive:

> b ~ [y] -> [(x,y)]
> a ~ x

(~ is type equality)

This gives

> e :: [y] -> [(x,y)]
> f :: x -> ([y] -> [(x,y)]) -> ([y] -> [(x,y)])

or, removing the extra parenthesis

> f :: x -> ([y] -> [(x,y)]) -> [y] -> [(x,y)]

that is, f takes *three* arguments, the second of which is a function
of type [y] ->[(x,y)]

What happens is that the *partially applied* f is getting chained
through the fold; so you get

zip [1,2,3] ['a','b','c']
= foldr f e [1,2,3] ['a','b','c']
= f 1 (f 2 (f 3 e)) ['a', 'b', 'c']

Then, in the first application of f, "g" is (f 2 (f 3 e)):

= (1, 'a') : (f 2 (f 3 e)) ['b','c']

Now, there are two termination conditions; if the first list ends, we
reach "e", which eats the remainder of the second list, returning [].
In fact, e is the only total function of its type (forall x y. [y] ->
[(x,y)]).

If the second list ends, then f sees that and doesn't call g; that is,
the rest of the foldr is unevaluated and unused!

foldr f e [1,2,3] []
=> f 1 (foldr f e [2,3]) []
=> []

  -- ryan