https://twitter.com/inamiy/status/1317703510910148608

church-encoding.hs

{-# LANGUAGE RankNTypes #-}

module Church where

-- Church encoding of boolean.
-- 1st arg as `true`, 2nd arg as `false`.
type Bool' = forall x. x -> x -> x

true :: Bool'
true = \t f -> t

false :: Bool'
false = \t f -> f

not' :: Bool' -> Bool'
not' = \b t f -> b f t

----------------------------------------

-- Church encoding of natural numbers.
-- 1st arg as `succ`, 2nd arg as `zero`.
type Nat = forall x. (x -> x) -> x -> x

zero :: Nat
zero f x = x

one :: Nat
one f x = f x

two :: Nat
two f x = f (f x)

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

plus :: Nat -> Nat -> Nat
plus m n s z = m s (n s z)

times :: Nat -> Nat -> Nat
times m n s z = m (n s) z

exp' :: Nat -> Nat -> Nat
exp' m n = n m

----------------------------------------

-- Church encoding of Maybe.
-- 1st arg as `nothing`, 2nd arg as `just`.
type Maybe' a = forall b . b -> (a -> b) -> b

just :: a -> Maybe' a
just a = \nothing just -> just a

nothing :: Maybe' a
nothing = \nothing just -> nothing

----------------------------------------

-- Church encoding of List.
-- 1st arg as `nil`, 2nd arg as `cons`.
type List' a = forall b. b -> (a -> b -> b) -> b

nil :: List' a
nil = \nil cons -> nil

cons :: a -> List' a -> List' a
cons a as = \nil cons -> cons a (as nil cons)

----------------------------------------

-- Church encoding of Either.
-- 1st arg as `left`, 2nd arg as `right`.
type Either' a b = forall x. (a -> x) -> (b -> x) -> x
-- ≅ ∀ x. (Either a b -> x) -> x
-- ≅ ∀ r. Cont r (Either a b)
-- ≅ Yoneda Identity (Either a b)

left :: a -> Either' a b
left a = \l r -> l a

right :: b -> Either' a b
right b = \l r -> r b