Solution
= Solution
Change the <right fold>'s result type to an accumulator-transforming <function type>:
``
foldlAsFoldr :: (b -> a -> b) -> b -> [a] -> b
foldlAsFoldr s n xs = foldr c id xs n
where
c x k a = k (s a x)
``
Thus \b[`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:
``
foldr c id (x:xs) a
= c x (foldr c id xs) a
= foldr c id xs (s a x)
= foldl s (s a x) xs
= foldl s a (x:xs).
``
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).