Definiton of length using foldr

Question

I'm trying to understand a part in the lecture notes of a class I'm taking. It defines the length function as:

length = foldr (\_ n -> 1 + n) 0

Can someone explain me how this works? I can't wrap my mind around it.

Answer 1

First, type of foldr: (a -> b -> b) -> b -> [a] -> b

Taking the usage into context, foldr takes in 3 arguments: a function (that takes in a. an element of a list and b. an accumulator, and returns the accumulator), the starting value of accumulator, and a list. foldr returns the final result of the accumulator after applying the function through the list.

As for this piece of code:

length = foldr (\_ n -> 1 + n) 0

As you can see, it is missing the list - so the return value of the right hand side is a function that will take in a list and produce an Int (same type as 0). Type: [a] -> Int.

As for what the right hand side means: (\_ n -> 1 + n) 0

\ means declare an unnamed function

_ means ignore the element from the list (correspond to a in the type of foldr). As you know, foldr will go through the list and apply the function to each element. This is the element passed into the function. We don't have any use of it in a length function, so we denote that it should be ignored.

n is the parameter for the Int passed in as accumulator.

-> means return

1 + n will increment the accumulator. You can imagine that the return value is passed back to foldr and foldr saves the value to pass into the next call to the function (\_ n -> 1 + n).

The 0 outside the bracket is the starting value of the counter.

Answer 2

The function foldr is to fold the list with a right associative operator, you can easily understand what the function does if you use the operator(+), (The function has the same behavior as sum):

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

For your length function, it is equivalent to:

foldr (\_ n -> 1 + n) 0 [1,2,3,4,5] = 1+(1+(1+(1+(1+0))))

That is what the foldr for

Answer 3

There's several equivalent ways to understand it. First one: foldr f z [1, 2, 3, 4, ..., n] computes the following value:

f 1 (f 2 (f 3 (f 4 (f ... (f n z)))))

So in your case:

length [1,2,3,4] = foldr (\_ n -> 1 + n) 0 [1,2,3,4]  
                 = (\_ n -> 1 + n) 1 ((\_ n -> 1 + n) 2 ((\_ n -> 1 + n) 3 ((\_ n -> 1 + n) 4 0)))
                 = (\_ n -> 1 + n) 1 ((\_ n -> 1 + n) 2 ((\_ n -> 1 + n) 3 (1 + 0)))
                 = (\_ n -> 1 + n) 1 ((\_ n -> 1 + n) 2 (1 + (1 + 0)))
                 = (\_ n -> 1 + n) 1 (1 + (1 + (1 + 0)))
                 = 1 + (1 + (1 + (1 + 0)))
                 = 1 + (1 + (1 + 1))
                 = 1 + (1 + 2)
                 = 1 + 3
                 = 4

Another one is to start from this function, which copies a list:

listCopy :: [a] -> [a]
listCopy [] = []
listCopy (x:xs) = x : listCopy xs

That may look like a trivial function, but foldr is basically just that, but except of hardcoding the empty list [] and the pair constructor : into the right hand side, we instead use some arbitrary constant and function supplied as arguments. I sometimes like to call these arguments fakeCons and fakeNil (cons and nil are the names of the : operator and [] constant in the Lisp language), because in a sense you're "copying" the list but using fake constructors:

foldr fakeCons fakeNil [] = fakeNil
foldr fakeCons fakeNil (x:xs) = fakeCons x (subfold xs)
    where subfold = foldr fakeCons fakeNil

So under this interpretation, your length function is "copying" a list, except that instead of the empty list it's using 0, and instead of : it's discarding the elements and adding 1 to the running total.

And here's yet a third intepretation of foldr f z xs:

1. z is the solution of your problem when the list is empty.
2. f is a function that takes two arguments: an element of the list , and a partial solution: the solution to your problem for the list of elements that appear to the right of the element that's passed to f. f then produces a solution that's "one element bigger."

So in the case of length:

1. The length of an empty list is 0, so that's why you use 0 as the second argument to foldr.
2. If the length of xs is n, then the length of x:xs is n+1. That's what your first argument to foldr, \_ n -> n + 1, is doing: it's computing the length of a list, given as arguments the first element of the list (which in this case we ignore) and the length of the rest of the list (n).

This way of thinking about foldr is very powerful, and should not be underestimated. Basically, in the function that you pass as the first argument to foldr, you're allowed to assume that the problem you're trying to solve has already been solved for all lists shorter than the one you're dealing with. All your argument function has to do, then, is to compute an answer for a list that's one element longer.