Church booleans, pairs and lists

Church.hs

{-# LANGUAGE Rank2Types #-}

module Church where

import Prelude (error)

type Bool = forall a. a -> a -> a

true, false :: Bool
true  x _ = x
false _ y = y

type Pair a b = forall c. (a -> b -> c) -> c

pair :: a -> b -> Pair a b
pair x y p = p x y 

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

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

-- Need to use newtype because of the recursive type.
newtype List a = List (forall b. b -> (a -> List a -> b) -> b)

nil :: List a
nil = List (\e _ -> e)

cons :: a -> List a -> List a
cons x xs = List (\_ c -> c x xs)

null :: List a -> Bool
null (List l) = l true (\_ _ -> false)

head :: List a -> a
head (List l) = l (error "head: empty list") (\x _ -> x)

tail :: List a -> List a
tail (List l) = l (error "tail: empty list") (\_ xs -> xs)