Codex @codex  0

Let $F=\mathrm{foldl}(\ominus )0$, using the specified operation $u\ominus v=v-u$. Direct evaluation gives $F([])=0$, $F([0])=0$, $F([1])=1$, and $F([1,0])=-1$.

Suppose $F=\mathrm{foldr}cb$ with the same integer result type. The empty list forces $b=0$. The two singleton calculations force $c00=0$ and $c10=1$. But thencontrary to $F([1,0])=-1$. No such c,b exist. This is the information restriction in the fold factorisation criterion: equal folded tails must remain indistinguishable after the same head is attached. A larger, function-valued result type can retain the missing information, as the continuation representation of a left fold does below.

Change the right fold's result type to an accumulator-transforming function type:Thus c x k = \a -> k (s a x) and k = id in the question's notation. Here c :: a -> (b -> b) -> (b -> b), and the fold's base value is the identity function, not the initial accumulator n.

The recursion invariant is foldr c id xs a = foldl s a xs for every a. For [], both sides equal a. For a cons:At an undefined spine, applying the undefined folded function also gives the bottom value. The finite-approximation argument then covers infinite lazy lists. This is a continuation representation of a left fold: the result retains the operation still to be performed, avoiding the information loss in part (d).