--- 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