Fold as the Universal List Eliminator

A list is either empty or an element consed onto a shorter list. That two-case shape is the entire structure of the type, so any function that consumes a list must do exactly two things: say what the empty case means, and say what to do with a head given the result for the tail. foldr is the function that packages those two answers and applies them to the whole list. What makes it more than a convenience is that it is the only function of that shape that respects the structure, and that uniqueness is what turns list programs into algebraic equations.

The two equations that define the type

Write the list type with its constructors:

data List a = Nil | Cons a (List a)

A fold takes a replacement for each constructor. For Nil it takes a value z :: b. For Cons it takes a binary function f :: a -> b -> b. It then walks the list, substituting:

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

Three lines define it, and the third line is the whole idea: the result for a cons cell is the function applied to the head and to the result for the tail. For sum, f = (+) and z = 0. For length, f = const (1 +) and z = 0. For map g, f = (:) . g and z = []. For (++), f = (:) and z = ys. Every structural recursion over a list can be written this way, and the compiler’s own derived foldr instance for a recursive type is generated by exactly this rule.

The universal property

The claim that foldr is universal is a statement about arrows, not about code. Let (b, z, f) be any list algebra: a carrier type b, a nullary operation z, and a binary operation f with the right types. A function h :: [a] -> b is a homomorphism from the list algebra to that algebra when

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

The universal property says that for every such algebra there is exactly one homomorphism, and it is foldr f z. Existence is the definition; uniqueness is the useful half. Two functions that both satisfy the two equations are equal, so proving a property of foldr f z never requires induction on the list. The equations are the induction.

This is what lets Bird-style derivations work. To show that map g . map f = map (g . f), unfold both sides by the equations: map g (map f []) = map g [] = [] and map g (map f (x:xs)) = g (f x) : map g (map f xs), which matches map (g . f) (x:xs). The base case and the step case are the two equations, and the induction hypothesis is discharged by the uniqueness clause. The same style proves that foldr (:) [] = id, that reverse = foldl (flip (:)) [], and that a fold composed with a fold is a fold when the inner one produces the outer one’s carrier.

foldl is not the same fold

The left fold threads the accumulator through the list from the left:

foldl :: (b -> a -> b) -> b -> [a] -> b
foldl f z []     = z
foldl f z (x:xs) = foldl f (f z x) xs

The equations look symmetric, but the recursion is in tail position, so the recursive call itself is a jump that does not grow the stack. The accumulator is accumulated eagerly only in the syntactic sense: f z x is computed before the call, but under lazy evaluation the result of f is not forced, so foldl (+) 0 [1..n] builds the expression ((0 + 1) + 2) + ... and only evaluates it when the final result is demanded. That is the space leak described in call-by-need evaluation, and it is the reason foldl' exists: the strict version forces the accumulator at each step.

The two folds are related but not interchangeable. foldl f z xs = foldr (flip f) z (reverse xs) holds for strict f, and the reverse costs an extra traversal. foldr can consume an infinite list when f ignores its second argument, which is what makes take 5 (foldr (:) [] [1..]) terminate; foldl cannot, because it must reach the end before returning anything. The direction of the trade is therefore: foldr is the structural eliminator that can short-circuit and can work on infinite lists; foldl' is the accumulator loop that runs in constant space but must consume the whole input.

Which fold the compiler chooses

GHC’s list fusion rewrites foldr into a form that fuses with the producer. The rule that does it is expressed as a rewrite from foldr k z applied to a build-wrapped producer into the producer’s own function applied to k and z. The consequence is that a foldr-based consumer of a build-based producer, such as a sum over an enumeration, compiles to a loop with no list at all, and map f (map g xs) compiles to one traversal. foldl does not participate in this rule; foldl' is a separate loop and fuses only through a different mechanism. The practical rule that follows is that foldr is the fold to write when the result is built lazily or when the producer and consumer should fuse, and foldl' is the fold to write when the result is a strict scalar such as a count or a sum. The fusion machinery itself is covered in fold fusion.

Church numerals and the same shape at another type

The list fold has a type-directed twin. A list can be represented by its own fold: instead of storing the elements, store a function that, given z and f, produces the answer. This is the Church encoding, and for lists it is

newtype Church a = Church { runChurch :: forall b. (a -> b -> b) -> b -> b }

toChurch :: [a] -> Church a
toChurch xs = Church (\f z -> foldr f z xs)

fromChurch :: Church a -> [a]
fromChurch c = runChurch c (:) []

toChurch and fromChurch are mutually inverse up to the extensional equality of the encoded functions, and every list operation has a counterpart that composes the encodings directly. map becomes function composition inside the forall b, and (++) becomes composition of the two functions. The representation has the same asymptotics as the list for foldr-shaped consumers and worse asymptotics for operations that need to inspect the structure, because there is no structure left to inspect. The encoding is the list type written as its own eliminator, which is the same idea as the Church numerals and the same idea as the continuation encoding of a program: the operations are cheap and the structure is unavailable. The general version is the initial algebra of a functor, treated in catamorphisms, where [a] is the least fixed point of F x = 1 + a × x and foldr f z is the unique algebra homomorphism out of it.

Laws, and the ones that fail

The fold has a small set of laws that hold unconditionally, and a larger set that hold only under side conditions. The unconditional ones are the two equations and the fusion rule: a fold composed with a function that is itself a homomorphism is a fold. foldr f z . map g = foldr (f . g) z holds for any f, g, z, by the equations alone.

The conditional ones are where implementations diverge. foldr f z . reverse = foldl (flip f) z needs f to be strict in its first argument, and foldl f z . reverse = foldr (flip f) z needs it to be strict in its second: in each case the lazy side builds a thunk chain of unbounded depth that the strict side does not, so the two agree only when the extra laziness is invisible. The fusion law foldr (++) [] = concat is no help here either, because it names concat rather than the identity, and the identity is recovered only by choosing the element type to be lists. Productiveness of concat on an infinite list of lists rests on (++) being lazy in its right argument, a property the equations do not mention. The laws of the total domain do not automatically transfer to the domain with ⊥.

A third class of law concerns strictness annotations. foldl' satisfies the same two equations as foldl on total values and differs only on values containing ⊥, where it is stricter. This is usually what a programmer wants, and it is never what a proof about foldl establishes.

Where the abstraction leaks

foldr is total on finite lists and productive on infinite ones, but it is not a good fit for every consumer. A function that needs to inspect both ends of the list, such as a palindrome check or a zip that must align lengths, cannot be written as a single fold without an intermediate structure. A function that must fail early on a malformed prefix needs the short-circuit behaviour that foldr gives only when the combining function is non-strict in its second argument. And a function whose recursion is not structural, such as a merge of two sorted lists, has no fold at all; it recurses on both arguments, and the universal property does not apply to it.

The honest summary is that foldr is the eliminator for the list functor and nothing more. It captures exactly the recursion that follows the spine of one list, and it is complete for that class. Everything else needs a different recursion scheme, which is what the later articles in this cluster build: tail-recursive accumulation and continuations for the loops that folds express badly, and catamorphisms over arbitrary functors for the same universal property at other types.