Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment