## 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)