-- G54FOP
-- Simply Typed Lambda-Calculus
-- Church Numerals
type Nat a = (a -> a) -> a -> a
church :: Int -> Nat a
church 0 = \f -> \x -> x
church n = suc (church (n-1))
suc :: Nat a -> Nat a
suc = \n -> \f -> \x -> f (n f x)
evNat :: Nat Int -> Int
evNat n = n (+1) 0
cPlus :: Nat a -> Nat a -> Nat a
cPlus = \n m -> \f x -> n f (m f x)
cMult :: Nat a -> Nat a -> Nat a
cMult = \n m -> \f -> n (m f)
cExp :: Nat a -> Nat (a->a) -> Nat a
cExp = \n m -> m n
-- We can "downgrade" a higher-level numeral
-- But not vice versa
natDown :: Nat (a->a) -> Nat a
natDown = \n -> \f -> n (\g -> (\x -> f (g x))) (\x -> x)