# 3.3 Origami by numbers

    data Nat = Zero | Succ Nat

We have a fold for natural numbers.

    foldN ∷ α → (α → α) → Nat → α
    foldN z s Zero     = z
    foldN z s (Succ n) = s (foldN z s n)

This is actually a rearranged version of the familiar ‘iterate’
function which expresses the repeated application of a given
function:

    iter ∷ Nat -> (a -> a) -> (a -> a)
    iter n f x = foldN x f n

(iter n) is the Church numeral of n.


## Unfolds for naturals

We have both a single-function and multi-function version of unfoldN,
as with unfoldL.

    unfoldN′ ∷ (a → Maybe a) → a → Nat
    unfoldN′ f x = case f x of
                     Nothing → Zero
                     Just y  → Succ (unfoldN′ f y)

    unfoldN ∷ (a → Bool) → (a → a) → a → Nat
    unfoldN p f x = if p x then Zero else Succ (unfoldN p f (f x))

“[T]his is the minimisation function from recursive function theory,
which takes a predicate p, a function f, and a value x, and computes
the least number n such that p (iter n f x) holds.” (p. 50)


## Beyond primitive recursion

The fact that we can express minimization functions as unfolds on
naturals means that we've gone past primitive recursion.   “Indeed,
using only folds and unfolds on naturals, we can capture the full
power of iterative imperative programs.” (p. 50)

We can use a hylomorphism to express the equivalent of the ‘while
loop’ of imperative programming.

    untilN ∷ (a -> Bool) -> (a -> a) -> a -> a
    untilN p f x = foldN x f (unfoldN p f x)

untilN repeatedly applies f (with initial argument x) until p is true.
The version above is simple but inefficient; it first computes the
number of applications required, then performs the iteration.  This is
a classic opportunity for deforestation.