I found this beautiful little example while reading John Hughes’ “Why Functional Programming Matters” [PDF]. All the cool stuff in this post is stolen shamelessly from section 3 of that paper, while any mistakes and not-so-cool stuff is mine.

## List recursion

Here are a few list processing functions written using recursion:

They all have the same recursive structure; a base case for the empty list [], and a case that breaks the list into head and tail a:as. The second case performs some function on the list head and on the result of a recursive call on the rest of the list.

The functions differ in the value they return for the empty list case, and the function they use to combine the head of the list and the result of the recursive call on the tail.

## Expressing sum without explicit recursion

Let’s take a closer look at the sum function with this in mind.

It returns 0 for the empty list case, and uses (+) as its combining function. If we imagine we have some function foo which takes care of all the recursion stuff for us, then our sum function becomes a function of foo, (+), and 0.

## Solving for foo

We now have two definitions for sum, a recursive one and one in terms of foo. We can solve these two equations by substituting the second sum definition into the original. Everywhere we had sum, we’ll put foo (+) 0. We’ve said they are equivalent, so we know this is ok.

Let’s generalise this a little. foo is a function which takes another function ((+) in this case) and a value (0 here). We can write this as foo f x, where f = (+) and x = 0.

All we’ve done is substitute for different values, so we can be happy we haven’t changed anything thanks to the equivalences we’ve declared between expressions.

Finally, we can remove redundant parentheses and move f to its more common prefix position:

And while we’re at it let’s call foo by its more common name:

So while I’ve previously struggled to derive a right fold implementation, we’ve derived a correct one by performing straightforward substitution into an existing recursive function.

## Beautiful

To me this is a wonderful illustration of how programming with expressions (functional programming) lets us use fundamental mathematical truths to reason about and reliably transform our code. We managed to get a very valuable function for free – no giant leaps of insight required. We declared an equality that represented the recursive part of our call and solved it to get foldr, just as we would solve a standard algebraic equation.

I find this wonderfully elegant and beautiful.

## Full circle

To bring this full circle, we can now rewrite the recursive list processing functions from the beginning of this post. Using our derived fold function means we can avoid having to specify the mechanics of the recursion.

Aside: we’d typically use a left fold for some of these cases where it would help them be executed more efficiently, but for these particular cases they are mathematically equivalent.