Left fold (foldl :: (b -> a -> b) -> b -> [a] -> b)

A list reduction carrying an accumulator from left to right: foldl s z [] = z and foldl s z (x:xs) = foldl s (s z x) xs. In a lazy language this does not by itself force each intermediate accumulator; its association and evaluation strictness are separate issues. An infinite input spine prevents this operation from returning a result.^[ref]

A right fold can build a function that accepts the initial accumulator later. Its empty result is id; its step prepends one update before the continuation supplied by the tail. The invariant foldr c id xs a = foldl s a xs, quantified over all a, follows from the two fold equations. Both applied sides give the bottom value on an undefined spine; finite approximation then covers infinite lazy lists. The larger result type retains information that a direct same-result-type fold can lose.

If $f$ is a strict function and $f(g(a,x))=h(f(a),x)$ for every $a,x$, then f (foldl g a xs) = foldl h (f a) xs. Prove the equation simultaneously for all accumulators by structural induction on the list. The empty case is immediate; at a cons, apply the hypothesis with accumulator g a x and then rewrite its image using the assumed equation. At the bottom value, strictness supplies the required equality. For pure definable functions, equality on finite partial lists extends to infinite lazy lists by finite approximations. For finite terminating spines alone, strictness is unnecessary.