-- Church-Encoding of booleans, naturals and polymorphic lists

-- 1
newtype B = B (forall r. r -> r -> r)

unB :: B -> (forall r. r -> r -> r)
unB (B f) = f

true :: B
true = B (\x y -> x)

false :: B
false = B (\x y -> y)

ite :: B -> r -> r -> r
ite b = \x y -> unB b x y

notB :: B -> B
notB = \b -> B (\x y -> unB b y x)

xorB :: B -> B -> B
xorB = \a b -> B (\x y -> unB a (unB (notB b) x y ) (unB b x y))

impB :: B -> B -> B
impB = \a b -> B (\x y -> unB a (unB b x y) x)

-- 2

newtype N = N (forall r. (r -> r) -> r -> r)

unN :: N -> (forall r. (r -> r) -> r -> r)
unN (N f) = f

zero :: N
zero = N (\f a -> a)

suc :: N -> N
suc n = N (\f a -> f (unN n f a))

add :: N -> N -> N
add = \m n -> N (\f a -> unN n f (unN m f a))

mul :: N -> N -> N
mul = \m n -> N (\f a -> unN m (unN n f) a)

-- 3

newtype List a = List (forall r. r -> (a -> r -> r) -> r)

unList :: List a -> (forall r. r -> (a -> r -> r) -> r)
unList (List f) = f

nil :: List a
nil = List (\u f -> u)

cons :: a -> List a -> List a
cons = \x l -> List (\u f -> f x (unList l u f))

length :: List a -> N
length = \l -> unList l zero (\x n -> suc n)