Hand calculation of Bird's definition of zip using foldr
Can someone provide a complete hand calculation of zip [1,2,3] [4,5,6] using the following definition of zip, based on foldr: zip :: [a] -> [b] -> [(a, b)] zip = foldr f e where e ys = [] f x g [ ] = [] f x g (y : ys) = (x , y) : g ys foldr :: (a -> b -> b) -> b -> ([a] -> b) foldr _ e [] = e foldr f e (x : xs) = f x (foldr f e xs) This implementation of zip produces the expected result [(1, 4), (2, 5), (3, 6)], but I'm unable to do the hand calculation and don't understand why it works. 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)))... Thanks, as always, to all in this great community. _________________________________________________________________ Windows Live™: Life without walls. http://windowslive.com/explore?ocid=TXT_TAGLM_WL_allup_1a_explore_032009
zip [1,2,3] [4,5,6] = zip (1:2:3:[]) (4:5:6:[]) = foldr f e (1:2:3:[]) (4:5:6:[]) = f 1 (foldr f e (2:3:[])) (4:5:6:[]) = (1, 4) : foldr f e (2:3:[]) (5:6:[]) = (1, 4) : f 2 (foldr f e (3:[])) (5:6:[]) = (1, 4) : (2, 5) : foldr f e (3:[]) (6:[]) = (1, 4) : (2, 5) : f 3 (foldr f e []) (6:[]) = (1, 4) : (2, 5) : (3, 6) : foldr f e [] [] = (1, 4) : (2, 5) : (3, 6) : e [] = (1, 4) : (2, 5) : (3, 6) : [] = [(1, 4), (2, 5), (3, 6)] On 12 Mar 2009, at 20:01, R J wrote:
Can someone provide a complete hand calculation of zip [1,2,3] [4,5,6] using the following definition of zip, based on foldr:
zip :: [a] -> [b] -> [(a, b)] zip = foldr f e where e ys = [] f x g [ ] = [] f x g (y : ys) = (x , y) : g ys
foldr :: (a -> b -> b) -> b -> ([a] -> b) foldr _ e [] = e foldr f e (x : xs) = f x (foldr f e xs)
This implementation of zip produces the expected result [(1, 4), (2, 5), (3, 6)], but I'm unable to do the hand calculation and don't understand why it works. 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)))...
Thanks, as always, to all in this great community.
Windows Live™: Keep your life in sync. Check it out._______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
2009/3/12 R J
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
participants (3)
-
Miguel Mitrofanov -
R J -
Ryan Ingram