Cons.hs show function representation of pairs and positive integers in Haskell.

Cons.hs

{-# LANGUAGE RankNTypes #-}

-- | Laws:
--
-- > car (ChurchTuple a b) == a
-- > cdr (ChurchTuple a b) == b
newtype ChurchTuple a b = ChurchTuple { unChurchTuple :: forall c. ((a -> b -> c) -> c) }

churchTuple :: a -> b -> ChurchTuple a b
churchTuple a b = ChurchTuple $ \m -> m a b

fst :: ChurchTuple a b -> a
fst (ChurchTuple f) = f const

snd :: ChurchTuple a b -> b
snd (ChurchTuple f) = f $ \_ b -> b

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

true :: ChurchBool
true = ChurchBool const

false :: ChurchBool
false = ChurchBool $ \_ y -> y

churchIf :: ChurchBool -> a -> a -> a
churchIf (ChurchBool c) = c

churchOr :: ChurchBool -> ChurchBool -> ChurchBool
churchOr (ChurchBool c1) = c1 true

churchAnd :: ChurchBool -> ChurchBool -> ChurchBool
churchAnd (ChurchBool c1) c2= c1 c2 false

churchNot :: ChurchBool -> ChurchBool
churchNot (ChurchBool c) = c false true

newtype ChurchInt = ChurchInt { unChurch :: forall a. (a -> a) -> a -> a }

zero :: ChurchInt
zero = ChurchInt $ \f x -> x

add1 :: ChurchInt -> ChurchInt
add1 (ChurchInt n) = ChurchInt $ \f x -> f (n f x)

sub1 :: ChurchInt -> ChurchInt
sub1 n = ChurchInt $ 
    \f x -> unChurch n (\g h -> h (g f)) (const x) id

-- | Laws:
--
-- > runList xs ChurchTuple nil == xs
-- > runList (fromList xs) f z == foldr f z xs
-- > foldr f z (toList xs) == runList xs f z
newtype ChurchList a = 
    ChurchList { runList :: forall r. (a -> r -> r) -> r -> r }
 
-- | The 'ChurchList' counterpart to '(:)'.  Unlike 'DList', whose
-- implementation uses the regular list type, 'ChurchList' abstracts
-- over it as well.
cons :: a -> ChurchList a -> ChurchList a
cons x xs = ChurchList $ \k z -> k x (runList xs k z)
 
-- | Append two 'ChurchList's.  This runs in O(1) time.  Note that
-- there is no need to materialize the lists as @[a]@.
append :: ChurchList a -> ChurchList a -> ChurchList a
append xs ys = ChurchList $ \k z -> runList xs k (runList ys k z)
 
-- i.e.,
nil :: ChurchList a
nil = ChurchList $ \k z -> z

singleton :: a -> ChurchList a
singleton x = ChurchList $ \k z -> k x z

snoc :: ChurchList a -> a -> ChurchList a
snoc xs x = ChurchList $ \k z -> runList xs k (k x z)

data Iso a b = Iso { to :: a -> b, from :: b -> a }

isoTuple :: Iso (ChurchTuple a b) (a,b)
isoTuple = Iso to from where
  to :: ChurchTuple a b -> (a, b)
  to (ChurchTuple f) = f (,)

  from :: (a, b) -> ChurchTuple a b
  from = uncurry churchTuple

isoBool :: Iso ChurchBool Bool
isoBool = Iso to from where
  to :: ChurchBool -> Bool
  to (ChurchBool c) = c True False

  from :: Bool -> ChurchBool
  from True  = true
  from False = false

isoInt :: Iso ChurchInt Int
isoInt = Iso to from where
  to :: ChurchInt -> Int
  to (ChurchInt n) = n (+1) 0

  from :: Int -> ChurchInt
  from 0 = zero
  from n = add1 (from (n - 1))

isoList :: Iso (ChurchList a) [a]
isoList = Iso to from where
  to :: ChurchList a -> [a]
  to xs = runList xs (:) []

  from :: [a] -> ChurchList a
  from xs = ChurchList $ \k z -> foldr k z xs