Church Encodings

type C_Bool a = (a -> a -> a)

church_true :: C_Bool a
church_true = (\a -> \b -> a)

church_false :: C_Bool a
church_false = (\a -> \b -> b)

church_and :: C_Bool (C_Bool a) -> C_Bool a -> C_Bool a
church_and = (\b1 b2 -> b1 b2 church_false)


-- Try β-normalising And T F?

-- church_and church_true church_false
--   ≡ (\b1 b2 -> b1 b2 (\a b -> b)) (\a b -> a) (\a b -> b)
--   β-> (\b2 -> (\a b -> a) b2 (\a b -> b)) (\a b -> b)
--   β-> (of b2)   (\a b -> a) (\a b -> b) (\a b -> b)
--   β-> (\b -> (\a b -> b)) (\a b -> b)
--   β-> (\a b -> b)  ≡ church_false



case_Bool :: Bool -> a -> a -> a
case_Bool x true_case false_case = case x of
  True -> true_case
  False -> false_case


f :: Bool -> Int
f x = case x of
  True -> 1
  False -> 2

f2 :: Bool -> Int
f2 x = case_Bool x 1 2




data Pet = Cat String | Dog String | Fish

case_pet :: Pet -> (String -> a) -> (String -> a) -> a -> a
case_pet x cat_case dog_case fish_case = case x of
  Cat nm -> cat_case nm
  Dog nm -> dog_case nm
  Fish -> fish_case

g :: Pet -> String
g x = case x of
  Cat nm -> ("Cat " ++ nm)
  Dog nm -> ("Doggie " ++ nm)
  Fish -> ("A Fish")



type C_Num a = (a -> a) -> a -> a


church_zero :: C_Num a
church_zero = \f x -> x

church_one :: C_Num a
church_one = \f x -> f x

church_two :: C_Num a
church_two = \f x -> f (f x)

church_suc :: C_Num a -> C_Num a
church_suc = \n f x -> f (n f x)


-- Try β-normalising Suc 1?

-- church_suc church_one
--   ≡ (\n f x -> f (n f x)) (\f x -> f x)
--   β-> (\f x -> f ((\f x -> f x) f x))
--   β-> (\f x -> f ((\x -> f x) x))
--   β-> (\f x -> f (f x))



church_suc2 :: C_Num a -> C_Num a
church_suc2 = \n f x -> n f (f x)


add :: C_Num a -> C_Num a -> C_Num a
add = \m n f x -> m f (n f x)

multiply :: C_Num (C_Num a) -> C_Num a -> C_Num a
multiply = \m n -> m (add n) church_zero

-- A student asks a great question: why does the type of the "m" parameter to
-- multiply need to be "C_Num (C_Num a)" rather than "C_Num a".
--
-- Simply, because n is being used to repeat actions on an unknown type "a",
-- but m is being used to repeat "add n", an operation on "C_Num a".
--
-- What we can't do (in Haskell's type system, unless we turn on some
-- extensions) is to say that m's type is "(∀t. C_Num t)". If we could say
-- that the m parameter is polymorphic to any instance of "C_Num t" then we
-- could avoid this complication, at the cost of needing more logic in our type
-- system.


church_to_int :: C_Num Int -> Int
church_to_int = \c -> c (\x -> x + 1) 0

print_church :: C_Num Int -> String
print_church = show . church_to_int

-- tests we can try now:
-- print_church church_one
-- print_church church_two
-- print_church (multiply (add church_one church_two) church_two)