Developing Natural Numbers   [4]

A simple variation in "points-free" style

We can make a very modest simplification in the definition of the unary function transformers by using function composition in their definitions, rather than writing out the "value level" arguments overtly: this saves a few parentheses, but more importantly it stresses the "pipeline" of data flow and the way that two inverse functions are composed on either side of the argument function. Note especially that the arguments n and i disappear from both sides of the defining equations: a common mistake is to remove them from the right but forget to do so on the left.

data Nat = Zero | Succ Nat  deriving ...

nats = iterate Succ Zero

[zero,one,two,three,four,five] = take 6 nats

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

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

ifn f n = iton (f (ntoi n))
nfi f i = ntoi (f (iton i))


ibn b n m = iton (b (ntoi n) (ntoi m))
nbi b i j = ntoi (b (iton i) (iton j))

data Nat = Zero | Succ Nat  deriving ...

nats = iterate Succ Zero

[zero,one,two,three,four,five] = take 6 nats

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

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

ifn f = iton . f . ntoi
nfi f = ntoi . f . iton

ibn b n m = iton (b (ntoi n) (ntoi m))
nbi b i j = ntoi (b (iton i) (iton j))

Notes

• we can't so easily convert the binary function transformers ibn and nbi since they require a different sort of composition (one which composes unary functions with binary ones)