Developing Natural Numbers   [5]

Overt definitions for arithmetic operations

A more honest way to define the arithmetic functions is to define them directly on natural numbers, using pattern matching and recursion. We can easily define functions for addition, multiplication and exponentiation as follows: it is clear from the code that addition is iterated succession, multiplication is iterated addition and exponentiation (pow) is iterated multiplication. In each case, the amount of "iteration" is controlled by the second argument.

data Nat = Zero | Succ Nat  deriving ...

-- other conversions, etc. elided --

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

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)


> add two four 
Succ (Succ (Succ (Succ (Succ (Succ Zero)))))

> add two four == ibn (+) two four
True

Notes

• it might seem more "natural" to pattern-match on the first argument, but as we will see on the next couple of slides, the style used here lends itself to some consolidation
• note the consistent usage: each time we have a function defined with two cases, a base case using Zero and a recursive case using Succ