Continuation representation of a left fold (source code)

= Continuation representation of a left fold
{title2=`foldl s n xs = foldr (\x k a -> k (s a x)) id xs n`}

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.