Developing Natural Numbers   [1]

The Nat data type and some examples

We can define natural numbers á là Peano by using a recursive data type definition. We can then write out numerals in a sort of "unary notation", by repeatedly applying Succ to Zero. Appropriate equality and comparison functions can be defined using standard recursions.

data Nat = Zero | Succ Nat

one   =  Succ  Zero
two   =  Succ (Succ Zero)
three =  Succ (Succ (Succ Zero))  -- or just "three = Succ two"

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

Notes

• the constructor Zero takes no arguments: it is essentially a new constant
• the constructor Succ is pronounced "successor": it takes us from one natural number to the next
• when we define an infix function such as (==), we can use infix syntax or prefix syntax (but in parentheses)
• the underscore pattern (_) can be used when we don't want to name a variable (i.e., when we don't need to refer to it on the right-hand side)