Developing Natural Numbers   [8]

Iteration on (non-negative) integers

Once we see how useful the notion of iteration on naturals is, we can make a (very) similar definition for iteration on integers. The same basic idea applies: we give two parameters (z and s) which will be used to "replace" zero and successor in the construction of an integer. With integers, however, we must overtly "deconstruct" them to see the zero/successor structure, since it is not directly exposed in terms of constructors. We can put this iteration on integers (here called iti) directly to use in re-defining the conversion function from integers to naturals. Note especially how similar the definitions of the general iterators are, and how their use highlights the relationship between the conversions.

data Nat = Zero | Succ Nat  deriving ...

...

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




iton (0::Int) = Zero
iton (i+1)    = Succ (iton i)

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

data Nat = Zero | Succ Nat  deriving ...

...

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

iti z s (0::Int) = z
iti z s (i+1)    = s (iti z s i)

iton = iti  Zero    Succ


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

Notes

• one difference between integers and naturals is that naturals (as Nats) are built as data structures, from constructors, whereas integers (as Ints) are supplied asbtractly by the language, in terms of available operations and features (such as pattern-matching)
• another difference between integers and naturals, of course, is that the integers include negative numbers, whereas the naturals don't: what happens if we call a function defined by integer iteration (iti) on a negative integer?