Developing Natural Numbers   [7]

Points-free variations, etc.

We can make some further minor consolidations on two fronts: first, notice that the conversion function ntoi follows the same pattern as the arithmetic operators, and thus can alse be re-defined more concisely in terms of iteration. (In fact, it becomes so transparent as to nearly disappear!) Furthermore, note that we can drop a final argument m from both sides of each of the definitions for the arithmetic operations, leading to a final consolidation which further highlights their character.

data Nat = Zero | Succ Nat  deriving ...

...

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

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

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

data Nat = Zero | Succ Nat  deriving ...

...

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

ntoi = itn (0::Int) (1+)


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

Notes

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

  "ntoi is defined by iteration with zero and one-plus"

  or even (almost too transparently):

  "ntoi is defined by iteration with zero and successor"

• now you can read the definitions of add and mul as:

  "addition to n is defined by iteration, on n, of successor"

  and:

  "multiplication by n is defined by iteration, on zero, of addition by n"