= Solution
First define argument reversal, with its most general <polymorphic> <type signature>:
``
flip :: (a -> b -> c) -> b -> a -> c
flip f y x = f x y
``
Use `concat = foldr (++) []`. In the <right-fold fusion law>, choose `f = foldr fn e`, `g = (++)`, `a = []`, `b = e`, and `h = flip (foldr fn)`. The base-image condition follows from `foldr fn e [] = e`; strictness follows because a <right fold> inspects its input spine. Part (c) supplies exactly the compatibility condition:
``
f (xs ++ ys)
= foldr fn (foldr fn e ys) xs
= flip (foldr fn) xs (f ys)
= h xs (f ys)
``
Consequently,
$$
\boxed{\operatorname{foldr}\ fn\ e\circ\operatorname{concat}=\operatorname{foldr}\bigl(\operatorname{flip}(\operatorname{foldr}\ fn)\bigr)\ e.}
$$
The accumulator argument of `foldr fn` comes before the inner <list>, whereas the outer <right fold> supplies the inner <list> first; `flip` reconciles those orders. The proof uses fusion and the already proved concatenation identity, without a further <induction>.
Back to article page
