Right fold has the laws

rfold init op [] = init
rfold init op x:xs = op x (rfold init op xs)

while the left fold laws are

lfold init op [] = init
lfold init op x:xs = lfold (op init x) op xs

Folds express many kinds of sequence operations. One example is Python’s s.join which is a right fold with initial value the empty string and with an operation that combines two strings l and r into l if r == "" and l + s + r otherwise. Equally, Horner’s method, which evaluates the polynomial \(a_0 + a_1x + \cdots + a_nx^n\) using $n$ additions and $n$ multiplications by doing

\[a_0 + x(a_1 + x(a_2 + x(a_3 + \cdots + x(a_{n-1} + xa_n)\cdots)))\]

can be implemented as a right fold of the coefficients with initial value 0 and operation a op b = a + x * b.

Suppose we want to express the function rev which reverses a list as a left fold. (OK we can guess how to do it, but imagine we wanted to work it out systematically). Knowing the laws, we could try to do this by deriving a recurrence for rev and then finding an op and init so that the specialised left fold law agrees with the rev recurrence. For example, rev x:xs is (rev xs) ++ [x]. But this doesn’t fit with lfold because the latter has two list (in this case) arguments. We must generalise rev to operate on two lists.

Define rev2 xs ys to be (rev ys) ++ xs. The base case is rev2 xs [] = xs and the law is rev2 xs y:ys = rev2 y:xs ys. If we want rev2 xs ys to equal lfold xs op ys then applying the left fold law and comparing, we need rev2 y:xs ys to equal lfold (op xs y) ys at which point it is obvious that we must take op xs y to be y:xs, so op is swap-arguments-then-cons. We then recover rev from rev2 by specialising rev2’s first argument to [], corresponding to setting the init argument of lfold to [].

The lesson for me is that I should think of the init part of a fold as a genuine first-class argument rather than a special case I can mostly ignore.

I was sad to hear that Richard Bird died in 2022 - his inspirational Thinking Functionally With Haskell showed me the power of this kind of equational reasoning.