Developing Natural Numbers   [9]

Final code comparison and perspectives

Below is a side-by-side comparison of two versions of the natural number definitions, one shorter and the other longer. The point is not merely that the second version is more concise, but rather that it uses language features and programming techniques to bring out the most important issues (symmetries and other relationships, the crux of a definition) as clearly, and with as little distraction, as possible. These sorts of techniques will pay off even more later in the course, when the domains of discourse, representation techniques and meta-level tools become more complex and subtle. 

data Nat = Zero | Succ Nat

one   =  Succ  Zero
two   =  Succ (Succ Zero)
three =  Succ (Succ (Succ Zero))


instance Eq Nat where
  (==)  Zero     Zero    = True
  (==) (Succ n) (Succ m) = n == m
  (==)  _        _       = False

instance Ord Nat where
  compare  Zero     Zero    = EQ
  compare  Zero    (Succ _) = LT
  compare (Succ _)  Zero    = GT
  compare (Succ n) (Succ m) = compare n m

instance Show Nat where
  show  Zero       = "Zero"
  show (Succ Zero) = "Succ Zero"
  show (Succ n)    = "Succ (" ++ show n ++ ")"


ntoi  Zero    = 0 :: Int
ntoi (Succ n) = 1 + ntoi n

iton (0::Int) = Zero
iton (i+1)    = Succ (iton i)

ifn f n = iton (f (ntoi n))
nfi f i = ntoi (f (iton i))

ibn b n m = iton (b (ntoi n) (ntoi m))
nbi b i j = ntoi (b (iton i) (iton j))


add n  Zero    = n
add n (Succ m) = Succ  (add n m)

mul n  Zero    = Zero
mul n (Succ m) = add n (mul n m)

pow n  Zero    = Succ Zero
pow n (Succ m) = mul n (pow n m)

data Nat = Zero | Succ Nat  deriving (Eq, Ord, Show)

nats = iterate Succ Zero
[zero,one,two,three,four,five] = take 6 nats


itn z s  Zero    = z
itn z s (Succ n) = s (itn z s n)

iti z s (0::Int) = z
iti z s (i+1)    = s (iti z s i)


ntoi = itn (0::Int) (1+)
iton = iti Zero Succ


ifn f = iton . f . ntoi
nfi f = ntoi . f . iton

ibn b n m = iton (b (ntoi n) (ntoi m))
nbi b i j = ntoi (b (iton i) (iton j))


add n = itn n     Succ  
mul n = itn Zero (add n)
pow n = itn one  (mul n)

Notes