-- G54FOP
-- system T
data Nat = Zero | Suc Nat
rec :: (Nat -> a -> a) -> a -> Nat -> a
rec h a Zero = a
rec h a (Suc n) = h n (rec h a n)
num :: Int -> Nat
num 0 = Zero
num n = Suc (num (n-1))
nVal :: Nat -> Int
nVal = rec (\_ -> (+1)) 0
instance Show Nat where
show = ("num "++).show.nVal
----------
-- Terms of system T are built using only
-- abstraction, application, numerals and rec
plus :: Nat -> Nat -> Nat
plus = \n -> \m -> rec (\m -> \k -> Suc k) n m
mult :: Nat -> Nat -> Nat
mult = \n m -> rec (\m k -> plus k n) (num 0) m
expo :: Nat -> Nat -> Nat
expo = \n m -> rec (\m k -> mult k n) (num 1) m
fact :: Nat -> Nat
fact = \n -> rec (\m k -> mult k (Suc m)) (num 1) n
prd :: Nat -> Nat
prd = \n -> rec (\m k -> m) Zero n
-- Ackermann Function: definition by pattern-matching
ackermann :: Int -> Int -> Int
ackermann 0 m = m+1
ackermann n 0 = ackermann (n-1) 1
ackermann n m = ackermann (n-1) (ackermann n (m-1))
-- Ackermann function in system T
ack :: Nat -> Nat -> Nat
ack = \n ->
rec (\n ackn ->
\m -> rec (\m ackSnm -> ackn ackSnm)
(ackn (num 1))
m)
(\m -> Suc m) n
-- Fibonacci Numbers in two ways
-- First using pairing, like in the untyped calculus
type TBool = Nat -> Nat -> Nat
type NatPair = TBool -> Nat
tr :: TBool
tr = \x y -> x
fl :: TBool
fl = \x y -> y
pair :: Nat -> Nat -> NatPair
pair = \n m -> \b -> b n m
first :: NatPair -> Nat
first = \p -> p tr
second :: NatPair -> Nat
second = \p -> p fl
fibP :: Nat -> NatPair
fibP =
\n -> rec (\m fibPn -> pair (second fibPn)
(plus (first fibPn) (second fibPn)))
(pair (num 0) (num 1)) n
fib1 :: Nat -> Nat
fib1 = \n -> first (fibP n)
-- Second way: using higher-order recursion
fibFrom :: Nat -> (Nat -> Nat -> Nat)
fibFrom = rec (\n fibn a b -> fibn b (plus a b)) (\a b -> a)
fib2 :: Nat -> Nat
fib2 = \n -> fibFrom n (num 0) (num 1)