Developing Natural Numbers   [2]

Derivation and consolidation

We can generate the (infinite) list of all natural numbers using the Prelude's iterate function: it generates a list by increasing applications of some function to some initial "seed" value. Then we can use the take function and a pattern definition (essentially a list of names defined in one step) to define convenient names for the first handful of naturals. We can also save some work by having Haskell derive the Eq and Ord instances all by itself: the definitions derived will be equivalent to the ones we made by hand.

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 ++ ")"

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

nats = iterate Succ Zero

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

Notes

• the iterate function from the Prelude has type (a -> a) -> a -> [a]; its definition looks like this:

  iterate f x = x : iterate f (f x)

• note that iterate returns an infinite list, so always take a prefix of nats (or be ready to hit that stop button)