-- Natural numbers a la Peano, as a Haskell datatype

module Nats where

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

-- some named Nats, for convenience

[zero, one, two, three, four, five, six] = take 7 $ iterate Succ Zero

-- folds for Nats and Ints

foldn :: (a -> a) -> a -> Nat -> a

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

foldi :: (a -> a) -> a -> Int -> a

foldi s z 0 = z
foldi s z n = s (foldi s z (n-1))

-- conversion between Nats and Ints

n2i :: Nat -> Int
n2i = foldn (+1) 0

i2n :: Int -> Nat
i2n = foldi Succ Zero

-- the standard arithmetic operations, as folds

add m = foldn Succ m
mul m = foldn (add m) Zero
exp m = foldn (mul m) one


-- the following is optional (currently commented out), but can
-- be used to "show" Nat calculations in normal decimal format
-- (but you must delete Show from the "deriving list" for Nat)

{-

instance Show Nat where
  show = show . n2i
  
-}