Developing Natural Numbers

Abstracting out iteration on naturals   [6]

This common pattern in the definition of functions on naturals by a process of iteration over (one of) the argument(s) can be abstracted out into a separate function, here called itn for "iteration on naturals". Once we abstract out the common pattern of iteration with this function, the true character of the arithmetic operators is even more apparent. The iteration function takes two other arguments, here called z and s, and it essentially recurses over the structure of its natural argument and replaces every Zero by a z and every application of Succ by an application of s. This is why (as expressed in green at the bottom of the code) when iteration is applied to Zero and Succ,we get just the identity function on naturals.

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)

data Nat = Zero | Succ Nat  deriving ...

-- other conversions, etc. elided --

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

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

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






itn Zero Succ  <==>  id

Notes

• you can read the new definition of add (for example) as:

  "add of n and m is defined by iteration, on n, of successor, controlled by m"