Folding

Consider the functions sumNumbers :: [Int] -> Int, myMaximum :: [Int] -> Int, and countNothings :: [Maybe a] -> Int again.

sumNumbers :: [Int] -> Int
sumNumbers [] = 0
sumNumbers (x:xs) = x + sumNumbers xs

myMaximum :: [Int] -> Int
myMaximum [] = 0
myMaximum (x:xs) = go x xs
    where go biggest [] = biggest
        go biggest (x:xs) = go (max biggest x) xs

countNothings :: [Maybe a] -> Int
countNothings [] = 0
countNothings (Nothing : xs) = 1 + countNothings xs
countNothings (Just _  : xs) = countNothings xs

They have one common characteristic. They take a list and produce a value that depends on the values of the elements in the given list. They “crunch” or fold a list of many values into a single value.

Prelude has a function called foldr, which performs a right associative fold over a Foldable data type. We’ll learn more about Foldable soon. At this point, it suffices to think of lists, so we define

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f y []     = y
foldr f y (x:xs) = f x (foldr f y xs)

What this definition says, is that for an empty list [] :: [a], foldr returns the default value y :: b. For any other list x : xs, foldr applies f to x and the result of foldr f y xs (i.e. folding over the rest of the list). It’s a simple definition by recursion.

In other words, foldr calls its argument function f repeatedly with two arguments.

• The first argument is the current element from the list.
• The second argument is what f returned for the rest of the list.

Consider the list [1,2,3]:

The expression foldr (+) 0 [1,2,3] evaluates as follows:

foldr (+) 0 [1,2,3] ==> foldr (+) 0 (1:2:3:[])
                    ==> 1 + (foldr (+) 0 (2:3:[]))
                    ==> 1 + (2 + (foldr (+) 0 (3:[])))
                    ==> 1 + (2 + (3 + (foldr (+) 0 [])))
                    ==> 1 + (2 + (3 + 0))

The result can be thought of as a tree:

One way to think about foldr f y xs is that it replaces the (:) operation with f and [] with y. In this case, f was (+) and y was 0. If you write out how sumNumbers [1,2,3] behaves, you’ll notice that it performs the same computation as foldr (+) 0 [1,2,3] does! More generally:

sumNumbers xs == foldr (+) 0 xs

Those more experienced with math may notice that we can prove this claim by induction: Firstly, sumNumbers [] ==> 0 and foldr (+) 0 [] ==> 0, so in the base case sumNumbers [] == foldr (+) 0 []. Next, we may assume as our induction hypothesis that sumNumbers xs == foldr (+) 0 xs for any list xs. Then, for the list x:xs, we have sumNumbers (x:xs) ==> x + sumNumbers xs. Hence, foldr (+) 0 (x:xs) ==> x + foldr (+) 0 xs ==> x + sumNumbers xs by induction hypothesis. Therefore, by induction, the equation holds.

You don’t need to read, write, or understand induction proofs in this course, but perhaps it is reassuring to know that properties and equalities of functions in Haskell can be (in principle) analysed mathematically, because Haskell is such a nice language. (Equalities and properties can be analysed in any programming language, but for Haskell, this analysis is especially convenient because Haskell is pure.)

Another folding example is the map function:

map g xs = foldr helper [] xs
    where helper y ys = g y : ys

To see why this works, consider what foldr helper [] [x1,x2,..,xn] does:

Now, since helper x xs ==> g x : xs for every x and xs, we get that:

The resulting list, [ g x1, g x2, g x3, ..., g xn ], is then exactly what we would have gotten with map g xs. (This could have been also proved by induction as we did for sumNumbers.) The lesson to take away is that folding is a particular, yet quite general, way to apply some transformation recursively into some structure (e.g. a list).

Exercises

All exercises can be found in Set4a and Set4b. Please pay attention in the title of the exercise in which file the exercises of this section can be found.

Exercises from 4a:

None for now :)

Exercises from 4b:

You can check your current points from the blue blob in the bottom-right corner of the page.