= Solution
Again use <structural induction> on the finite <list>. At `[]`, both the <right fold> and the <left fold> return `e`. For `x:xs`, use `reverse (x:xs) = reverse xs ++ [x]`, part (a), and the definition of `flip`:
``
foldl (flip f) e (reverse (x:xs))
= foldl (flip f) e (reverse xs ++ [x])
= foldl (flip f) (foldl (flip f) e (reverse xs)) [x]
= flip f (foldl (flip f) e (reverse xs)) x
= f x (foldl (flip f) e (reverse xs))
= f x (foldr f e xs)
= foldr f e (x:xs)
``
The penultimate equality uses the <induction hypothesis>. Thus \b[`foldr f e xs = foldl (flip f) e (reverse xs)`]. Finiteness matters: reversing an infinite <list> does not produce its first element, whereas some <right folds> do.
Back to article page