-- polymorphically-typed Church encodings, in Haskell

-- we need to turn on higher-rank polymorphism with the "RankNTypes" option
{-# LANGUAGE RankNTypes #-}

type CBool = forall a. a -> a -> a

cTrue :: CBool
cTrue x y = x

cFalse :: CBool
cFalse x y = y

cnot :: CBool -> CBool
cnot b = \x y -> b y x

cand :: CBool -> CBool -> CBool
cand b1 b2 = b1 b2 cFalse

cor :: CBool -> CBool -> CBool
cor b1 b2 = b1 cTrue b2

toBool :: CBool -> Bool
toBool b = b True False

type CNat = forall a. (a -> a) -> (a -> a)

czero, cone, ctwo, cthree :: CNat
czero = \f x -> x
cone = \f x -> f x
ctwo = \f x -> f (f x)
cthree = \f x -> f (f (f x))

csucc :: CNat -> CNat
csucc n = \f x -> f (n f x)

toInt :: CNat -> Int
toInt n = n (+1) 0

fromInt :: Int -> CNat
fromInt n
  | n == 0 = czero
  | n > 0  = csucc (fromInt (n-1))
  
cadd :: CNat -> CNat -> CNat
cadd m n = \f x -> m f (n f x)

cmul :: CNat -> CNat -> CNat
cmul m n = \f x -> m (n f) x

cisZero :: CNat -> CBool
cisZero n = n (\b -> cFalse) cTrue