= Solution
Prove the <natural-number fold fusion law> pointwise. At `Zero`,
``
f (foldNat g a Zero) = f a = b = foldNat h b Zero
``
Assuming the equation at `m`, the `Succ m` calculation is:
``
f (foldNat g a (Succ m))
= f (g (foldNat g a m))
= h (f (foldNat g a m))
= h (foldNat h b m)
= foldNat h b (Succ m)
``
The compatibility premise `f . g = h . f` justifies the middle rewrite. This proves the theorem for finite total constructor values by <structural induction>.
For the full lazy <Haskell> interpretation, also handle the <bottom value>: `foldNat g a` is strict in its outer `Natural` constructor, so its value on bottom is bottom; the assumed <strict function> property of `f` makes the left side bottom too. The same zero/successor induction now covers finite partial constructor chains. Pure definable functions preserve the limits of these information approximations, extending equality to infinite `Succ` chains. This explains the strictness premise; finite total induction alone would not use it.<Haskell 2010 Language Report>[§3.1: bottom values; §6.2: strict evaluation]{ref}
Back to article page
