churchnumerals.hs

{-# LANGUAGE Rank2Types #-}
import Prelude hiding (succ,pred)
newtype Church = Church (forall a. (a -> a) -> a -> a)

zero,one,two,three :: Church
zero  = Church $ \f x -> x
one   = Church $ \f x -> f x
two   = Church $ \f x -> f (f x)
three = Church $ \f x -> f (f (f x))

churchToNatural :: Church -> Integer
churchToNatural (Church c) = c (1+) 0

listToChurch :: [a] -> Church
listToChurch l = Church $ \f n -> foldr (\_ p -> (f p)) n l
zero' = listToChurch []
one'  = listToChurch [1] -- use of integers is arbitrary
two'  = listToChurch [1,1]

churchToList :: Church -> [Integer]
-- the use of integers here is completely arbitrary
churchToList (Church c) = c (1:) []

pred' :: Church -> Church
pred' = listToChurch . tail . churchToList

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

pred :: Church -> Church
pred (Church n) = fst $ n (\(_, xs) -> (xs, succ xs)) (error "empty list", zero)