Some fun with churchs lambda calculus in haskell

Church.hs

{-# LANGUAGE RankNTypes #-}

module Church where

import Prelude hiding (succ, pred, and, or, not, fst, snd, head, tail)

newtype Boolean = Bo (forall a . a -> a -> a)

true :: Boolean
true = Bo (\ t _ -> t)

false :: Boolean
false = Bo (\ _ f -> f)

instance Show Boolean where
  show (Bo f) = f "true" "false"

and :: Boolean -> Boolean -> Boolean
and (Bo b) c = b c false

or :: Boolean -> Boolean -> Boolean
or (Bo b) c = b true c

not :: Boolean -> Boolean
not (Bo b) = b false true

newtype Pair a b = Pr (forall c . (a -> b -> c) -> c)

instance (Show a, Show b) => Show (Pair a b) where
  show (Pr p) = p (\ a b -> "(" ++ show a ++ "," ++ show b ++ ")")

pair :: a -> b -> Pair a b
pair f s = Pr (\ b -> b f s)

fst :: Pair a b -> a
fst (Pr p) = p (\ a _ -> a)

snd :: Pair a b -> b
snd (Pr p) = p (\ _ b -> b)

newtype Number = Nr (forall a. (a -> a) -> a -> a)

instance Show Number where
  show (Nr a) = a ("1+" ++) "0"

instance Num Number where
  fromInteger n
    | n < 0 = error "cannot convert negative numbers"
    | n == 0 = zero
    | otherwise  = succ (fromInteger $ n-1)
  a + b = add a b
  a - b = subt a b
  a * b = mult a b
  abs _ = error "not implemented"
  signum _ = error "not implemented"

eval :: Number -> Integer
eval (Nr a) = a (+1) 0

zero :: Number
zero = Nr (\ _ z -> z)

succ :: Number -> Number
succ (Nr a) = Nr (\ s z -> s (a s z))

add :: Number -> Number -> Number
add (Nr a) = a succ

mult :: Number -> Number -> Number
mult (Nr a) b = a (add b) zero

one :: Number
one = succ zero

two :: Number
two = succ one

three :: Number
three = succ two

four :: Number
four = succ three

five :: Number
five = succ four

pow :: Number -> Number -> Number
pow x (Nr n) = n (mult x) one

isZero :: Number -> Boolean
isZero (Nr n) = n (\ _ -> false) true

-- | the most impressive implementation of the predecessor function
pred :: Number -> Number
pred (Nr n) = fst (n ss zz)
  where zz = pair zero zero
        ss p = pair (snd p) (succ $ snd p)

subt :: Number -> Number -> Number
subt a (Nr b) = b pred a

isEqual :: Number -> Number -> Boolean
isEqual a b = isZero (subt a b) `and` isZero (subt b a)

-- * Lists
newtype List a = L (forall s . (a -> s -> s) -> s -> s)

instance Show a => Show (List a) where
  show (L l) = show $ l (:) []

nil :: List a
nil = L (\ _ n -> n)

cons :: a -> List a -> List a
cons h (L tl) = L (\ c n -> c h (tl c n))

infixr 3 +:
(+:) :: a -> List a -> List a
(+:) = cons

isNil :: List a -> Boolean
isNil (L l) = l (\ _ _ -> false) true

-- I have to cheat a bit here with undefined
head :: List a -> a
head (L l) = l (\ a _ -> a) undefined  

tail :: List a -> List a
tail (L l) = fst (l ss nn)
  where nn = pair nil nil
        ss a p = pair (snd p) (a +: snd p)