--------------------
-- Natural numbers (short version)
-- Fritz Ruehr * WU CS 451 * Spring 2006
--------------------

-- data type and sample values

data Nat = Zero | Succ Nat  deriving (Eq, Ord, Show)

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


-- iteration

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)

-- conversion of numbers

ntoi = itn (0::Int) (1+)
iton = iti Zero Succ

-- conversion of functions

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))


-- arithmetic operations

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