= Solution
Take \b[`h = (.)`]:
``
h :: (b -> c) -> (a -> b) -> a -> c
h f g x = f (g x)
``
This is its standalone <principal type>; in the <right fold>, `c` specializes to the type of a function from the accumulator to itself.
For fixed `f`, `g` and `e`, prove equality pointwise by <structural induction> on the <list>. At `[]` both sides return `e`. For `x:xs`, assume the equality for `xs` and calculate:
``
foldr f e (map g (x:xs))
= f (g x) (foldr f e (map g xs))
= f (g x) (foldr (h f g) e xs)
= h f g x (foldr (h f g) e xs)
= foldr (h f g) e (x:xs)
``
The second equality is the <induction hypothesis>. <Function extensionality> gives the required equality of composed functions. This is an instance of the <right-fold fusion law>.
For the full lazy <Haskell> interpretation, include a <bottom value> for an undefined list spine: both sides are bottom there. The same constructor argument covers every finite approximation with an undefined tail. The <Scott continuity> of the list operations then extends equality to their limits, including infinite <lists>. Ordinary induction on finite total <lists> alone proves only that restricted case.
Back to article page
