= Solution
Use the <right fold> definition `xs ++ ys = foldr (:) ys xs`, the right-identity law `xs ++ [] = xs`, and the finite-<list> involution law `reverse (reverse xs) = xs`. The last two laws are the additional results used here. Part (b) now gives
``
xs ++ ys
= foldr (:) ys xs
= foldl (flip (:)) ys (reverse xs)
``
Set `ys = []` to obtain `xs = foldl (flip (:)) [] (reverse xs)`. Substitute `reverse xs` for `xs` and simplify the double reversal:
``
reverse xs
= foldl (flip (:)) [] (reverse (reverse xs))
= foldl (flip (:)) [] xs
``
The derived <Haskell> definition is therefore
``
reverse :: [a] -> [a]
reverse = foldl (flip (:)) []
``
\b[Each step prepends the next element to the accumulator.] This is a <left fold> derivation from <list concatenation>, rather than merely a proposed implementation.
Back to article page
