A Peano natural number type and its primitive recursion scheme are defined:

data PN = Z | S PN prim c f Z = c prim c f (S n) = f n (prim c f n)

We wish to implement the equality predicate of two Peano natural numbers,
and without recursion apart from `prim`

.

To this end, it benefits us greatly to first study how to apply
`prim`

symbolically. Many people understand `prim`

by abbreviating `g = prim c f`

to deduce:

g = prim c f⇒

g Z = c g (S n) = f n (g n)

The converse also holds (proof by induction) and is more important. So:

g Z = c g (S n) = f n (g n)⇒

g = prim c f

It is important because it lets us first write a function like `g`

— using explicit recursion as we see fit — and then recognize a pattern and convert
it to `prim`

. The symbols will do the work.

More specifically on the pattern: if your function looks like:

g Z = c g (S n) = ... n ... (g n) ... (g n) ... n ...

in the second equation, you look at how
you recurse with `g n`

, and how you use `n`

otherwise.
Then you can abstract that out into a λ function and rewrite:

g Z = c g (S n) = (\p r -> ... p ... r ... r ... p ...) n (g n)

(If necessary, choose fresh names instead of `p`

,`r`

to avoid name clashes. If you don't use `(g n)`

, or if you don't use
`n`

, that's fine, it just means the λ function has unused parameters.)

Then `(\p r -> ... p ... r ... r ... p ...)`

is your
`f`

and you can convert to `prim`

:

g = prim c (\p r -> ... p ... r ... r ... p ...)

This symbolic conversion scheme is exactly what
we need because we could implement the equality predicate at ease with
explicit recursion, but not so at ease with `prim`

.

Now we begin. The equality predicate is pretty obvious with explicit recursion:

equal Z Z = True equal Z (S n) = False equal (S m) Z = False equal (S m) (S n) = equal m n

First I convert the first two equations; in fact I consider
`equal Z`

to be one function `g`

, and so I add parentheses to
emphasize that it is one single thing:

(equal Z) Z = True (equal Z) (S n) = False = (\_ _ -> False) n ((equal Z) n)⇒

equal Z = prim True (\_ _ -> False)

Next, I convert the other two equations, considering `equal (S m)`

to be one function `g`

:

(equal (S m)) Z = False (equal (S m)) (S n) = equal m n

Although there is a recursion to `equal`

, it is not of the right
form: `g = equal (S m)`

here, so the right form of recursion
`g n`

would be `equal (S m) n`

, but we only have
`equal m n`

. So we pretend this is not a recursion for the moment.
(It will be dealt with soon anyway.) But then we are using `n`

“otherwise”. So the λ function here is `(\p _ -> equal m p)`

.
So the conversion is:

(equal (S m)) Z = False (equal (S m)) (S n) = (\p _ -> equal m p) n ((equal (S m)) n)⇒

equal (S m) = prim False (\p _ -> equal m p)

At this stage we have these new equations:

equal Z = prim True (\_ _ -> False) equal (S m) = prim False (\p _ -> equal m p)

Now it is `equal`

's turn to be `g`

and be converted.
The recursion is also of the right form: we expect `g m`

here,
which is `equal m`

, which does occur now. (On the other hand,
`m`

does not occur “otherwise”.) So:

equal Z = prim True (\_ _ -> False) equal (S m) = (\_ r -> prim False (\p _ -> r p)) m (equal m)⇒

equal = prim (prim True (\_ _ -> False)) (\_ r -> prim False (\p _ -> r p))

That is the answer.

I have more Haskell Notes and Examples