This is old and most likely broken

ChurchEncoding.hs

module ChurchEncoding where

newtype Church a = Church { unChurch :: (a -> a) -> a -> a }



church :: Integer -> Church Integer
church 0 = Church $ \f -> \x -> x
church n = Church $ \f -> \x -> f $ unChurch (church (n - 1)) f x

unchurch :: Church Integer -> Integer
unchurch (Church cn) = cn (+ 1) 0

-- plus: \m.\n.\f.\x.m f (n f x)
churchPlus :: Church Integer -> Church Integer -> Church Integer
churchPlus (Church m) (Church n) = Church $ \f -> \x -> m f (n f x)

(.+) :: Church Integer -> Church Integer -> Church Integer
(.+) = churchPlus


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

-- mult: \m.\n\.f\.m (n f)
churchMult :: Church Integer -> Church Integer -> Church Integer
churchMult m n f = m (n f)

(.*) :: Church Integer -> Church Integer -> Church Integer
(.*) x y = churchMult x y

-- exp: \m.\n.n m
--churchExp :: Church a -> Church (a -> a) -> Church a
--churchExp :: Church Integer -> (_ -> _) -> _
--churchExp m n f  x = n m

--(.**) :: Church Integer -> Church Integer -> Church Integer
--(.**) m n = churchExp m n

-- pred: \n.\f.\x.n(\g.\h.h(g f)) (\u.x)(\u.u)
--churchPred :: Church Integer -> Church Integer
churchPred n f x = n g (\u -> x) (\u -> u)
    where g = \g -> \h -> h(g f)
---- Booleans
--type ChurchBool a = Church a -> Church a -> Church a

-- true: \a.\b.a
true' :: a -> a -> a
true' a b = a

-- false: \a.\b.b
false' :: a -> a -> a
false' a b = b

newtype ChurchBool a = ChurchBool { unChurchBool :: a -> a -> a }

true, false :: ChurchBool a
true = ChurchBool (\a b -> a)
false = ChurchBool (\a b -> b)

-- if: \p.\a.\b.p a b
if' :: (a -> a -> a) -> a -> a -> a
if' p a b = p a b

-- not: \p.\a.\b.p b a
not' :: (a -> a -> a) -> a -> a -> a
not' p a b = p b a

-- xor: \a.\b.a (not b) b
--xor' :: (a -> a -> a) -> (a -> a -> a) -> (a -> a -> a)
--xor' a b = a (not' b) b

-- or: \p.\q.p p q

ifTest = if' false' 1 0
notTest = not' false' 1 0


-- and: \p.\q.(p q) p

--churchAnd :: ChurchBool a -> ChurchBool a -> ChurchBool a
--churchAnd (ChurchBool f) (ChurchBool h) =
--  ChurchBool $ (\a b -> a) f h-- \a b -> f a (h a b)
    
--churchAnd :: (a -> a -> a) -> (a -> a -> a) -> (a -> a -> a)
churchAnd
  :: (Church a -> Church a -> Church a)
  -> (Church a -> Church a -> Church a)
  -> Church a -> Church a -> Church a
churchAnd p q m n = p (q m n) n

churchAndTest :: (Bool, Integer)
churchAndTest = (0 == expr, expr)
  where
    expr = unchurch (churchAnd true' false' a b)
    a = church 0
    b = church 1