## Exercise 3.18
Express addN, mulN, powN in terms of foldN.
Each function has the type
f ∷ Nat → Nat → Nat
addN is really familiar, but it's good practice to calculate it.
Using the universal property, we have
addN m = foldN z s
iff
addN m n = case n of
Zero → z
Succ p → s (addN m p)
So we have the equations
addN m Zero = z
addN m (Succ n) = s (addN m n)
Since m + Zero = m for all natural numbers m, we have z = m. And, by
associativity, we have
addN m (Succ n) = Succ (addN m n)
and thus
s = Succ
The completed definition:
addN ∷ Nat → Nat → Nat
addN m = foldN m Succ
Again using the universal property, we get similar equations for mulN:
mulN m Zero = z
mulN m (Succ n) = s (mulN m n)
We use the definition of multiplication to state:
mulN m Zero = Zero = z
mulN m (Succ n) = addN m (mulN m n),
= { define s = addN m }
s (mulN m n)
giving us the following definition:
mulN ∷ Nat → Nat → Nat
mulN m = foldN Zero (addN m)
Finally, powN (powN b n = b ^ n).
powN b Zero = z
powN b (Succ n) = s (powN b n)
We have:
powN b Zero = (Succ Zero) = z
powN b (Succ n) = mulN b (powN b n)
= { define s = mulN b }
s (powN b n)
which gives the fold:
powN ∷ Nat → Nat → Nat
powN b = foldN (Succ Zero) (mulN b)