How do foldr and zipWith (:) work together?

Question

I'm new to Haskell, and I've come across the following code that baffles me:

foldr (zipWith (:)) (repeat []) [[1,2,3],[4,5,6],[7,8,9,10]]

It produces the following result, which after playing around with it, I'm not entirely sure why:

[[1,4,7],[2,5,8],[3,6,9]]

I'm under the impression that (:) prepends items to a list, and that (repeat []) produces an endless amount of empty lists [], and that foldr takes a function, an item, and a list, and condenses the list by consecutively applying the function to each item in the list along with the results.

That is to say, I intuitively understand how the following code produces a result of 10:

foldr (+) 1 [2,3,4]

But, I'm not at all sure why foldr (zipWith (:)) (repeat []) takes a list of lists and produces another list of lists with items grouped by their original inner indices.

Any explanation would be enlightening.

Answer 1

This is very simple. foldr is defined so that

foldr f z [] = z
foldr f z (x:xs) = f x (foldr f z xs)

thus,

foldr f z [a,b,c,...,n] = f a (f b (f c (...(f n z)...)))

Or, here,

foldr (zipWith (:)) (repeat []) [[1,2,3],[4,5,6],[7,8,9,10]]
=
zipWith (:) [1,2,3] 
  ( foldr (zipWith (:)) (repeat []) [[4,5,6],[7,8,9,10]] )
=
...
=
zipWith (:) [1,2,3] 
  ( zipWith (:) [4,5,6]
      ( zipWith (:) [7,8,9,10] 
          ( foldr (zipWith (:)) (repeat []) [] )))
=
zipWith (:) [1,2,3] 
  ( zipWith (:) [4,5,6]
      ( zipWith (:) [7,8,9,10] 
          ( repeat [] )))
=
zipWith (:) [1,2,3] 
  ( zipWith (:) [4,5,6]
      ( zipWith (:) [ 7, 8, 9,10] 
                    [[],[],[],[],[],[],....] ))
=
zipWith (:) [1,2,3] 
  ( zipWith (:) [ 4,  5,  6 ]
                [[7],[8],[9],[10]] )
=
zipWith (:) [ 1   , 2   , 3   ] 
            [[4,7],[5,8],[6,9]] 

And that's that.

_{(Next on the menu, traverse ZipList [[1,2,3],[4,5,6],[7,8,9,10]]... :) or maybe later.)}

---

As for the other example, it is

foldr (+) 1 [2,3,4] 
= 2 + foldr (+) 1 [3,4] 
= 2 + (3 + foldr (+) 1 [4]) 
= 2 + (3 + (4 + foldr (+) 1 [])) 
= 2 + (3 + (4 + 1))
= 2 + (3 + 5)
= 2 + 8
= 10

because + is strict in both of its arguments.

zipWith is not strict in both arguments, nor is the (:), so the first sequence should be taken as an illustration only. The actual forcing will occur in the top-down order, not bottom-up. For instance,

> map (take 1) . take 1 $ zipWith (:) (1 : undefined) (repeat undefined)
[[1]]

fully in accordance with

map (take 1) . take 1 $ zipWith (:) (1 : undefined) (repeat undefined)
=
map (take 1) . take 1 $ zipWith (:) (1 : undefined) (undefined : repeat undefined)
=
map (take 1) . take 1 $ (1 : undefined) : zipWith (:) undefined (repeat undefined)
=
map (take 1) $ (1 : undefined) : take 0 (zipWith (:) undefined (repeat undefined))
=
map (take 1) $ (1 : undefined) : []
=
map (take 1) [(1 : undefined)]
=
[take 1 (1 : undefined)]
=
[1 : take 0 undefined]
=
[1 : []]
=
[[1]]