## Exercise 3.16 Define a single-argument foldN' and define each version in terms of the other. By ‘single-argument’ is meant that the z and s arguments of foldN are unified; foldN' will still need a Nat argument, of course. We state the type, by analogy with foldL': foldN′ ∷ (Maybe α → α) → Nat → α and try to reason from the following specification: foldN′ t = foldN z s The calculation proceeds by induction on the Nat argument. Case Zero: foldN′ f Zero = foldN z s Zero ≡ { foldN.1 } foldN′ f Zero = z ≡ { define: f Nothing = z } foldN′ f Zero = f Nothing which gives us the first equation for foldN′. Case Succ n: foldN′ f (Succ n) = foldN z s (Succ n) ≡ { foldN.2 } foldN′ f (Succ n) = s (foldN z s n) ≡ { hypothesis } foldN′ f (Succ n) = s (foldN′ f n) ≡ { define: f (Just m) = s m } foldN′ f (Succ n) = f (Just (foldN′ f n)) which gives us the second equation. This completes the calculation. foldN′ ∷ (Maybe α → α) → Nat → α foldN′ f Zero = f Nothing foldN′ f (Succ n) = f (Just (foldN′ f n)) Defining foldN in terms of foldN' is just a matter of collecting the helper definitions in the above calculation: foldN z s = foldN' f where f Nothing = z f (Just m) = s m To define foldN' in terms of foldN, we have the specification foldN' f = foldN z s and calculate as follows: foldN z s Zero = foldN' f Zero ≡ { foldN.1, foldN'.1 } z = f Nothing which gives a value for z. Proceeding, foldN z s (Succ n) = foldN' f (Succ n) ≡ { foldN.2, foldN'.2 } s (foldN z s n) = f (Just (foldN' f n)) ≡ { hypothesis } s (foldN z s n) = f (Just (foldN z s n)) ≡ { generalize (foldN z s n) to m } s m = f (Just m) which gives a definition for s. We have: foldN' f = foldN (f ∘ Just) (f Nothing)