Search code examples
haskellchurch-encoding

Church encodings (conditionals)

I'm trying to write out some lambda calculus, but I can't get church conditionals to work. I should probably say that I'm a Haskell noob.

I've looked at solutions online and on SO, but they all involve introducing a new type and other tricks, but I want to keep it as close to the original syntax as possible. For example:

tru :: Integer -> Integer -> Integer
tru = \x -> \y -> x

fals :: Integer -> Integer -> Integer
fals = \x -> \y -> y

main = do
  print (tru 2 3)
  print (fals 5 6)

Matches the exact syntax for church booleans:

\a.\b.a
\a.\b.b

Any way to match the exact syntax for church if/else? I'm trying to replicate \p.\a.\b.p a b, but I'm not sure what I'm doing wrong:

ifelse :: Integer -> Integer -> Integer -> Integer -> Integer -> Integer
ifelse = \p -> \a -> \b -> p -> a -> b

main = do
  print (tru 2 3)
  print (fals 5 6)
  print (ifelse tru 42 58)
Solution

  • You want something like

    ifelse :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
ifelse = \p -> \a -> \b -> p a b

    or even

    ifelse = id

    Also keep in mind that your Church booleans can only be applied to integers, which can be restrictive. You can make your encodings a bit more general by giving them a polymorphic type.

    -- Warning: untested
{-# LANGUAGE RankNTypes #-}
type Cbool = forall a. a->a->a
tru :: Cbool
tru = const
fals :: Cbool
fals = const id
ifelse :: Cbool -> a -> a -> a
ifelse = id
type Cnat = forall a. (a->a)->a->a
zero :: Cnat
zero = \s z -> z   -- const id
-- etc