ChurchNumber with Haskell

main.hs

{-# LANGUAGE RankNTypes #-}

module Main where

newtype Church = Church { runChurch :: forall a. (a -> a) -> a -> a }

zero :: Church
zero = Church $ \_ x -> x

succChurch :: Church -> Church
succChurch (Church n) = Church $ \f x -> f (n f x)

one :: Church
one = succChurch zero

two :: Church
two = succChurch one

three :: Church
three = succChurch two

add :: Church -> Church -> Church
add (Church m) (Church n) = Church $ \f x -> m f (n f x)

predChurch :: Church -> Church
predChurch (Church n) = Church $ \f x ->
  let (p, _) = n (\(p, q) -> (q, f q)) (x, x)
  in p

subChurch :: Church -> Church -> Church
subChurch m (Church n) = n predChurch m

churchToInt :: Church -> Integer
churchToInt (Church n) = n (+1) 0

main :: IO ()
main = do
  putStrLn $ "three converted to int: " ++ show (churchToInt three)
  putStrLn $ "2 + 3 = " ++ show (churchToInt (add two three))
  putStrLn $ "3 - 2 = " ++ show (churchToInt (subChurch three two))
  putStrLn $ "2 - 3 = " ++ show (churchToInt (subChurch two three))