Foldable

Foldable is the abstraction of a container whose elements can be visited in order and combined: a list, a tree, an option, a map. It provides one operation, a fold, and every summary of the elements is derived from it: their sum, length, maximum, list of elements, or whether any of them satisfies a predicate. There are two equivalent formulations, a right fold with a combining function and a starting value, and foldMap, which maps every element into a monoid and combines the results. For lists, the universal property of fold characterizes the functions that can be written as folds^[1]. Foldable is a type class in Haskell's Prelude^[6], and in OCaml the same structure appears as the fold functions of the standard library's containers.

§ 01

Overview

A list is built from two constructors, the empty list and ::. The right fold replaces each :: by a function $f$ and the empty list by a value $z$ :

foldr f z [x_{1}, x_{2}, \dots, x_{n}] = f x_{1} (f x_{2} (\dots (f x_{n} z) \dots))

With $f = (+)$ and $z = 0$ it is the sum; with $f = λ x n . n + 1$ the length; with $f = (::)$ and $z = []$ it copies the list. The left fold brackets the other way, starting from the accumulator:

foldl f z [x_{1}, x_{2}, \dots, x_{n}] = f (\dots (f (f z x_{1}) x_{2}) \dots) x_{n}

Any container whose elements have an order can provide a right fold, and Foldable is the interface consisting of that fold. Everything else is written once, in terms of it:

A FOLDABLE signature, a functor deriving the usual operations, and instances for lists, options and trees.

(* A container is foldable if it can fold its elements from the right.
   Everything else is derived from that one function. *)
module type FOLDABLE = sig
  type 'a t
  val fold_right : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
end
 
module type MONOID = sig type t val empty : t val ( <+> ) : t -> t -> t end
 
module Derive (F : FOLDABLE) = struct
  let to_list t = F.fold_right List.cons t []
  let length t = F.fold_right (fun _ n -> n + 1) t 0
  let sum t = F.fold_right ( + ) t 0
  let exists p t = F.fold_right (fun x b -> p x || b) t false
  let maximum t = F.fold_right (fun x m -> match m with None -> Some x | Some y -> Some (max x y)) t None
  let fold_map (type m) (module M : MONOID with type t = m) f t = F.fold_right (fun x acc -> M.( <+> ) (f x) acc) t M.empty
  (* fold_left from fold_right: fold into a function that waits for the
     accumulator. *)
  let fold_left f z t = F.fold_right (fun x k acc -> k (f acc x)) t Fun.id z
end
 
type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree
 
module Tree = struct
  type 'a t = 'a tree
  let rec fold_right f t acc = match t with Leaf -> acc | Node (l, x, r) -> fold_right f l (f x (fold_right f r acc))
end
 
module Opt = struct
  type 'a t = 'a option
  let fold_right f o acc = match o with None -> acc | Some x -> f x acc
end
 
module L = Derive (List)
module T = Derive (Tree)
module O = Derive (Opt)

Running it.

tree:   to_list [1; 5; 7; 2; 9]  length 5  sum 24  max 9  exists (>8) true
option: length (Some 4) 1  length None 0  sum (Some 4) 4
fold_map string_of_int over the tree: "15729"
fold_left (-) 100 [1; 2; 3] via fold_right: 94   List.fold_left: 94

The tree is folded in order, left subtree, node, right subtree, so its elements come out as they would be printed. fold_left is derived from fold_right by folding into a function that is waiting for the accumulator, so a single fold is enough to provide both directions.

§ 02

foldMap and monoids

The second formulation maps each element into a monoid $(M, ⋄, e)$ and combines the results:

foldMap : (a \to M) \to T a \to M foldMap g [x_{1}, \dots, x_{n}] = g x_{1} ⋄ \dots ⋄ g x_{n}

The two formulations define each other. foldMap is a right fold with $⋄$ and $e$ , and a right fold is foldMap into the monoid of functions $b \to b$ under composition^[3]:

foldr f z t = (foldMap f t) z in the monoid (b \to b, \circ, id)

The monoid formulation says what a fold needs from the structure: an order on the elements, and nothing about bracketing, since the monoid is associative. A container can therefore implement foldMap by combining the results for its parts in whatever shape is convenient, a tree fold for a tree, with the same result as a sequential fold. When $M$ is a product of monoids, one foldMap computes several summaries in a single pass.

§ 03

The universal property

For lists, a function $h$ is a right fold precisely when it satisfies two equations, one for each constructor^[1]^[5]:

h = foldr f z ⟺ h [] = z and h (x :: x s) = f x (h x s)

The direction from right to left is a proof principle: to show that a recursive function equals a fold, check the two equations, with no induction needed, since the induction is done once in the proof of the property. It also gives the fusion law, under which a function applied after a fold can be absorbed into it:

g (foldr f z x s) = foldr f^{'} (g z) x s if g (f x y) = f^{'} x (g y)

Many functions on lists are folds: map, filter, append, reverse, and, by tupling the results, pairs of folds, which gives the "banana split" law that two folds over the same list can be computed in one pass^[4]:

map, filter, append and reverse as folds; two folds tupled into one; and the two directions of folding.

(* The universal property of fold_right: h is fold_right f xs v exactly
   when h [] = v and h (x :: xs) = f x (h xs). Functions that satisfy the
   two equations are folds. *)
let map g xs = List.fold_right (fun x acc -> g x :: acc) xs []
let filter p xs = List.fold_right (fun x acc -> if p x then x :: acc else acc) xs []
let append xs ys = List.fold_right List.cons xs ys
let reverse xs = List.fold_right (fun x acc -> acc @ [ x ]) xs []
 
(* Two folds over the same list become one fold into a pair: the average
   needs a single pass. *)
let sum_and_length xs = List.fold_right (fun x (s, n) -> (s + x, n + 1)) xs (0, 0)
 
(* Direction matters when the operation is not associative. *)
let right = List.fold_right ( - ) [ 10; 3; 2 ] 0 (* 10 - (3 - (2 - 0)) *)
let left = List.fold_left ( - ) 0 [ 10; 3; 2 ] (* ((0 - 10) - 3) - 2 *)

Running it.

map (x10) [10; 20; 30; 40; 50; 60]   filter even [2; 4; 6]
append [1; 2; 3; 4; 5; 6; 7]   reverse [6; 5; 4; 3; 2; 1]
sum 21, length 6, average 3.5 in one fold
fold_right (-) [10; 3; 2] 0 = 9    fold_left (-) 0 [10; 3; 2] = -15

When the combining function is associative and $z$ is its unit, the two directions agree, which is Bird's first duality theorem^[2]. Subtraction is neither, and the results differ. The same universal property holds for the fold of any algebraic data type, which is the catamorphism of the type^[7].

§ 04

Strictness

In Haskell, foldr is lazy in the recursive result: foldr (\x b -> p x || b) False stops at the first element satisfying p, and works on infinite lists. In a strict language the recursive result is computed before the combining function is called, so a search written as a right fold visits every element. Passing the rest of the fold as a function makes the evaluation explicit:

A search derived from fold_right, and the same with the rest of the fold delayed.

(* In a strict language, fold_right evaluates the whole list before the
   combining function sees its second argument, so a search derived from
   it cannot stop early. Passing the rest of the fold as a function
   restores early exit. *)
let visited = ref 0
let p x = incr visited; x = 3
 
let exists_fold p xs = List.fold_right (fun x b -> p x || b) xs false
 
(* The rest of the fold is a thunk; || does not force it if p x holds. *)
let exists_lazy p xs = List.fold_right (fun x rest () -> p x || rest ()) xs (fun () -> false) ()

Running it on a list of 10,000 elements.

exists_fold    true   p called 10000 times
exists_lazy    true   p called 4 times
List.exists    true   p called 4 times

The delayed version calls the predicate only until it succeeds, although List.fold_right still walks the whole list to build the delayed calls. For long lists in OCaml, fold_left runs in constant stack space and fold_right does not, which is why libraries provide early-exit functions such as List.exists directly. In Haskell the opposite problem arises: foldl builds a chain of unevaluated additions, and the strict foldl' is used for sums.

§ 05

In programming languages

Haskell's Foldable class has foldMap and foldr as its minimal definitions and provides about twenty derived functions; since GHC 7.10 the Prelude's list functions such as length, sum and elem are defined for any Foldable^[6]. One consequence that surprised users is that length (1, 2) is 1, because a pair is a container of its second component. Traversable extends Foldable with the ability to rebuild the container with effects^[3]^[8].

OCaml has no type classes. Each container module provides its own fold, iter and to_seq, with the argument order varying between modules, and Seq serves as a common currency between them. Other languages call the left fold reduce: JavaScript's Array.prototype.reduce, Python's functools.reduce, Java's Stream.reduce, whose documentation requires an associative function so that streams can be reduced in parallel.

§ 06

History

Folds over lists are as old as functional programming; APL's reduction operator and Lisp's reduce are early forms. The algebraic view, in which the fold of a data type is determined by its constructors, was developed in the Bird–Meertens formalism and by Malcolm^[5], and Meijer, Fokkinga and Paterson gave the fold of any recursive type its name, the catamorphism, in 1991^[4]. Hutton's 1999 tutorial made the universal property widely known^[1]. The Foldable class was introduced alongside Traversable by McBride and Paterson^[3] and moved into Haskell's Prelude in 2015^[6].