---
title: The Uniqueness of the Natural Numbers
author: nbloomf
date: 2014-05-23
tags: arithmetic-made-difficult, literate-haskell
slug: nats
---

> {-# LANGUAGE NoImplicitPrelude, BangPatterns #-}
> module NaturalNumbers
>   ( Natural(..), Unary()
>   , isZero, prev, naturalRec
> 
>   , _test_nats, main_nats
>   ) where
> 
> import Testing
> import Functions
> import Flip
> import Clone
> import Composition
> import Booleans
> import Tuples
> import DisjointUnions
> import Unary

We have assumed the existence of a set $\nats$ such that there is a unique inductive set homomorphism from $\nats$ to any other inductive set. But it turns out that this set is not *unique* with this property; any other inductive set which is *isomorphic* to $\nats$ enjoys it as well. In fact we've already seen one such set, namely $1 + \nats$.

Here's a handwavy proof. Let $(A,\varphi,e)$ be an inductive set, and suppose the unique map $\theta : \nats \rightarrow A$ is bijective. Then there is a unique inductive set homomorphism $\omega : A \rightarrow \nats$; namely, $\omega = \theta^{-1}$. Now any homomorphism from $A$ factors through the (unique) map $\omega$.

From a mathematical point of view, isomorphic objects are interchangeable. But as we'll eventually see, from a *computational* point of view, isomorphic objects can behave very differently. For this reason we will think of the properties of $\nats$ as a kind of interface, and write our programs against that. Specifically, every element of a $\nats$-like set is either the zero or the successor of some other element, and $\unnext$ discriminates between the two.

Now every inductive set isomorphic to $\nats$ is characterized by (1) its zero element, (2) its successor function, (3) the unique map $A \rightarrow \nats$, and (4) the unique map $\nats \rightarrow A$. We will also need a helper function to recognize the shape of a natural number, and for convenience a helper to convert a Haskell-native ``Integer`` to a natural number.

> class Natural n where
>   zero :: n
> 
>   next :: n -> n
> 
>   unnext :: n -> Union () n
>   
>   natural :: Integer -> n

Our helpers $\iszero$ and $\prev$ can be written against this interface:

> isZero :: (Natural n) => n -> Bool
> isZero = (either (const true) (const false)) . unnext
> 
> prev :: (Natural n) => n -> n
> prev = (either (const zero) id) . unnext

As can the natural recursion operator $\natrec$.

> naturalRec :: (Natural n)
>   => a -> (a -> a) -> n -> a
> naturalRec e phi n =
>   let
>     tau !x k = case unnext k of
>       Left () -> x
>       Right m -> tau (phi x) m
>   in tau e n

From now on we'll write programs against the ``Natural`` interface with ``naturalRec`` instead of ``Unary`` specifically. Of course, ``Unary`` is an instance of ``Natural``:

> instance Natural Unary where
>   zero = Z
> 
>   next = N
> 
>   unnext k = case k of
>     Z   -> Left ()
>     N m -> Right m
> 
>   natural = mkUnary

Okay!


Testing
-------

We proved some theorems about $\unnext$, $\prev$, and $\iszero$ in the last post.

> _test_unnext_zero :: (Natural n, Equal n)
>   => n -> Test Bool
> _test_unnext_zero m =
>   testName "unnext(0) == lft(*)" $
>   eq
>     (unnext (zero `withTypeOf` m))
>     (lft ())
> 
> 
> _test_unnext_next :: (Natural n, Equal n)
>   => n -> Test (n -> Bool)
> _test_unnext_next _ =
>   testName "unnext(next(m)) == rgt(m)" $
>   \m -> eq (unnext (next m)) (rgt m)
> 
> 
> _test_prev_zero :: (Natural n, Equal n)
>   => n -> Test Bool
> _test_prev_zero m =
>   testName "prev(0) == 0" $
>   eq
>     (prev (zero `withTypeOf` m))
>     zero
> 
> 
> _test_prev_next :: (Natural n, Equal n)
>   => n -> Test (n -> Bool)
> _test_prev_next _ =
>   testName "prev(next(m)) == m" $
>   \m -> eq (prev (next m)) m
> 
> 
> _test_isZero_zero :: (Natural n, Equal n)
>   => n -> Test Bool
> _test_isZero_zero m =
>   testName "isZero(0) == true" $
>   eq
>     (isZero (zero `withTypeOf` m))
>     true
> 
> 
> _test_isZero_next :: (Natural n, Equal n)
>   => n -> Test (n -> Bool)
> _test_isZero_next _ =
>   testName "isZero(next(m)) == false" $
>   \m -> eq (isZero (next m)) false


Suite.

> _test_nats :: (TypeName n, Natural n, Show n, Arbitrary n, Equal n)
>   => Int -> Int -> n -> IO ()
> _test_nats size cases n = do
>   testLabel1 "nats" n
>   let args = testArgs size cases
> 
>   runTest args (_test_unnext_zero n)
>   runTest args (_test_unnext_next n)
>   runTest args (_test_prev_zero n)
>   runTest args (_test_prev_next n)
>   runTest args (_test_isZero_zero n)
>   runTest args (_test_isZero_next n)

Main.

> main_nats :: IO ()
> main_nats = do
>   _test_nats 100 100 (zero :: Unary)
> 
>   let a = zero :: Unary
>   let b = true :: Bool
>   let c = tup zero zero :: Pair Unary Unary
> 
>   _test_functions      20 200 a a a a
>   _test_functions      20 200 a b a b
>   _test_flip           20 200 a a a a a a a
>   _test_flip           20 200 a b c a b c a
>   _test_clone          20 200 a a
>   _test_clone          20 200 a c
>   _test_compose        20 200 a a a a a a a
>   _test_compose        20 200 a b c a b c a
>   _test_tuple          20 200 a a a
>   _test_tuple          20 200 a b c
>   _test_disjoint_union 20 200 a a a
>   _test_disjoint_union 20 200 a b c