Higher order function specifics with foldr and foldl

Question

I'm having trouble interpreting the function signature for foldl. I understand how it works, but I'm not sure how it relates to the signature.

I have a few questions about its detail

foldr :: (a -> b -> b) -> b -> [a] -> b

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

It seems like the first parameter takes an addition function:

(a -> b -> b)

Within the function argument, what exactly is happening? Does this section apply the right-most integer a to the accumulator b to yield another integer 9 in this case? After this, does it then return a function that takes the accumulator as a parameter?

And following this, what do the last two parameters below mean?

[a] -> b

Many thanks.

Answer 1

When you pass (+) in to the first argument of foldr you implicitly declare that a is the same as b. This gets confusing since we tend to reuse names, but if I write it all together using the same namespace for the type variables

(+)       :: Num i => i -> i -> i
foldr     :: (a -> b -> b) -> b -> [a] -> b
foldr (+) :: Num i => i -> [i] -> i

where the third line implies that i ~ a and i ~ b thus, by transitivity, a ~ b. Also, it might be more clear here to see that the first remaining parameter in foldr (+) is an "initial" value for the fold and the [i] bit is the list that we're compressing, folding, reducing.

It might be even more clear to call foldr (+) 0 by it's more common name, sum :: Num a => [a] -> a. We also have foldr (*) 1 as product :: Num a => a -> [a].

So yes, your description of how the accumulator function is behaving in foldr (+) is exactly correct, but more specific than the function is in general. For instance, we can use foldr to build a Map.

foldr (\(k, v) m -> Map.insert m k v) Map.empty :: Ord k => [(k, v)] -> Map k v

In this case the accumulator function takes our association list and keeps inserting the values into our accumulat*ing* Map, which begins empty. To be utterly thorough here, let me write out the types all together again

(\(k, v) -> m -> Map.insert m k v)       :: Ord k => (k, v) -> Map k v -> Map k v
foldr                                    :: (a -> b -> b) -> b -> [a] -> b
foldr (\(k, v) -> m -> Map.insert m k v) :: Ord k => Map k v -> [(k, v)] -> Map k v

where we've forced a ~ (k, v) and b ~ Map k v.

---

As a final view on the matter, here's the definition of foldr with some suggestive variable names

foldr _    b []     = b
foldr (<>) b (a:as) = a <> foldr f b as

So you can see how (<>) :: a -> b -> b combines a and b types. We can "run" this definition explicitly to see how it builds up the computation.

foldr (+) 0 [1,2,3]
1 + (foldr (+) 0 [2,3])
1 + (2 + (foldr (+) 0 [3]))
1 + (2 + (3 + (foldr (+) 0 [])))
1 + (2 + (3 + 0))
1 + (2 + 3)
1 + 5
6

Which may be even more clear when we use a non-symmetric operation like the Map example above. Below I'm using {{ k -> v, k -> v }} to represent the Map since it isn't printable directly.

-- inserts a single (k,v) pair into a Map
ins :: Ord k => (k, v) -> Map k v -> Map k v
ins (k, v) m = Map.insert m k v

foldr ins Map.empty [('a', 1), ('b', 2)]
ins ('a', 1) (foldr ins Map.empty [('b', 2)])
ins ('a', 1) (ins ('b', 2) (foldr ins Map.empty []))
ins ('a', 1) (ins ('b', 2) Map.empty)
ins ('a', 1) (ins ('b', 2) {{  }})
ins ('a', 1) {{ 'b' -> 2 }}
{{ 'b' -> 2, 'a' -> 1 }}

Answer 2

It depends on how you look at it. The first step yields (+) 1 (foldr (+) 5 [2,3,4]). As you try to use the result of folding, this will force the evaluation of the second argument of (+), and since (+) is strict, this unravels the entire list. The last step yields (+) 1 ((+) 2 ((+) 3 ((+) 4 5))). So, yes, the first two numbers added are 4 and 5, yet this is not the first thing foldr does, and in this case you will have the list replaced with a tree of thunks first, then evaluate it to get the sum of all numbers and 5.

The replacing of list with thunks is good in cases where the function is not strict - this way you can evaluate only as much as necessary, even a possibly infinite list. In cases when the function is strict, it makes sense to consider rewriting with foldl'.