## Exercise 3.19

Express predN in terms of foldN; then, show how it can be generalized.

    predN          ∷ Nat → Maybe Nat
    predN Zero     = Nothing
    predN (Succ n) = Just n

Using the universal property of foldN, we have

    predN = foldN z s

    iff

    predN n = case n of
                Zero   → z
                Succ m → s (predN m)

This gives the equations

    predN Zero     = z
    predN (Succ m) = s (predN m)

The solution to the first is immediate: z = Nothing.  For the second
equation, we reason:

      s (predN m) = predN (Succ m)

    ≡   { predN.2 }

      s (predN m) = Just m

We have a problem: we can’t generalize (predN m), because m would occur
free on the right-hand side.  But we can use what we know about the
predecessor function, namely, that Succ (Pred m) = m, to expand the RHS.
We can't use Succ directly, because of the type of predN.

    ≡   { define: predInv ∷ Maybe Nat → Nat }

      s (predN m) = Just (predNInv (predN m))
        where
          predNInv Nothing  = Zero
          predNInv (Just n) = Succ n

    ≡   { generalizing (predN m) to mx }

      s mx = Just (predNInv mx)
        where
          predNInv Nothing  = Zero
          predNInv (Just n) = Succ n

    ≡   { η-equivalence }

      s = Just ∘ predNInv
        where
          predNInv Nothing  = Zero
          predNInv (Just n) = Succ n

The complete definition is then:

    predN = foldN Nothing (Just ∘ predInv)
      where
        predNInv Nothing  = Zero
        predNInv (Just n) = Succ n

TODO: How can we generalize from this?