Playing with Church Encoding

Church.hs

{-# LANGUAGE RankNTypes #-}
module Church where

import Prelude hiding (and, fst, snd, or, either, succ, toInteger)

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

and :: a -> b -> Prod a b
and x y p = p x y

fst :: Prod a b -> a
fst p = p (\x y -> x)

snd :: Prod a b -> b
snd p = p (\x y -> y)

test :: Prod Int String
test = and 666 "foo"

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

inl :: a -> Sum a b
inl x l r = l x

inr :: b -> Sum a b
inr y l r = r y

either :: Sum a b -> (a -> c) -> (b -> c) -> c
either s l r = s l r

test' :: Sum Int String
test' = inl 666

newtype NatC a = NatC { unNatC :: forall c. c -> (a -> c) -> c }

newtype Fix f = Fix { unFix :: (f (Fix f)) }

type Nat = Fix NatC

zero :: Nat
zero = Fix (NatC (\z s -> z))

succ :: Nat -> Nat
succ n = Fix (NatC (\z s -> s n))

plus :: Nat -> Nat -> Nat
plus (Fix (NatC n)) m = n m (\n' -> succ (plus n' m))

toInteger :: Nat -> Integer
toInteger (Fix (NatC n)) = n 0 (\n' -> 1 + toInteger n')

newtype ListC a r = ListC { unListC :: forall c. c -> (a -> r -> c) -> c }

type List a = Fix (ListC a)

nil :: List a
nil = Fix (ListC (\n c -> n))

cons :: a -> List a -> List a
cons x xs = Fix (ListC (\n c -> c x xs))

toList :: List a -> [a]
toList (Fix (ListC xs)) = xs [] (\x xs' -> x : toList xs')