Church Booleans in Haskell (and Morte!)

What’s a church boolean, and why should I care?

I’ll preface this post with why I’m writing it. One day, with my almost-nonexistent knowledge of the lambda calculus, the following question occurred to me:

If the lambda calculus only has functions, how can I do conditional statements?

It seems pretty essential for a model of computation to have some notion of conditionals, but lambda calculus has none! How do you make decisions? In my familiar world of register machines and CPUs they’re simply primitives- no help there!

So, first step: I googled “lambda calculus conditionals”, and found this helpful blog post. Therein, I discover that one can encode boolean true and false values using what are known as Church Booleans.

This post will cover how to represent church booleans in Haskell, and how to write the boolean logic functions or, and, not, and xor.

Note: Throughout this post, I will be using the “RankNTypes” language extension.

Encoding true and false using only functions

The intuition is this: A conditional (boolean) value represents a choice between two things. Therefore, we represent it with a function of two arguments, returning one of them.

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

Because we have no information about the type a, there are only two possible inhabitants, true and false.

true :: Boolean
true x y = x

false :: Boolean
false x y = y

true returns its first argument, and false returns its second argument. Think of them as representing each of two possible branches.

Before you proceed: I am about to write the functions if, and, or, and xor. If you like puzzles (this one isn’t too hard), you may enjoy playing type tetris to come up with the answers :-)

Writing an if' function

Now we want to write an if' function to behave in the same manner as Haskell’s if-then-else statement. If we were using Haskell’s Bool type, we could write it like this:

if' :: Bool -> a -> a -> a
if' c x y = if c then x else y

But we don’t, so let’s do it the Church way. How do we turn a function picking a branch, and two branch options (x and y), into a result? Well… we can just apply the function to both options:

if' :: Boolean -> a -> a -> a
if' cond x y = cond x y
-- we could just write "if' = id"

This anti-climactic function could also be written if' = id: it’s doing nothing more than applying cond to both arguments. Turns out the if' function is pretty useless when working with Church Booleans!

Or, And, Xor

Let’s write some Boolean logic functions.

Or

We know its type: Boolean -> Boolean -> Boolean. Now that we have if', it should be simple. If the first argument is true, then the or' is true. Otherwise, we need to check the second:

Using if':

orWithIf :: Boolean -> Boolean -> Boolean
orWithIf c1 c2 = if' c1 true (if' c2 true false)

Now, since if' is just the identity function, we can reduce this to the following:

or'' :: Boolean -> Boolean -> Boolean
or'' c1 c2 = c1 true (c2 true false)

Finally, recognise that if c2 is true, then c2 true false will be true. If c2 is false, then c2 true false will be false. So we can reduce this further, to:

or' :: Boolean -> Boolean -> Boolean
or' c1 c2 = c1 true c2

And

We can apply the same trick with and', and it comes out looking very similar:

and' :: Boolean -> Boolean -> Boolean
and' c1 c2 = c1 c2 false

Not and Xor

To write xor, it’s the same story. We check c1, but this time we need to return false if c2 is also true. That’s why we have flipped the arguments in the first argument to c1 (i.e., c2 false true).

xor' :: Boolean -> Boolean -> Boolean
xor' c1 c2 = c1 (c2 false true) (c2 true false)

Note that the first argument to c1 is essentially playing the role of the not' function. Also, the final argument to c1, that is c2 true false, can be reduced using the same trick as before. We could write xor again (if we had a not' function) like this:

xor :: Boolean -> Boolean -> Boolean
xor c1 c2 = c1 (not' c2) c2

Now all we need is the not' function, which we already know how to write:

not' :: Boolean -> Boolean
not' f = f false true

Alternatively, we could have written it by observing it’s simply modifying a Boolean to take the other branch. That is:

not'' :: Boolean -> Boolean
not'' = flip

Testing

Just in case you want to test these, here is a little function to print the truth table for a binary boolean function.

table :: (Boolean -> Boolean -> Boolean) -> IO ()
table f = do
  putStrLn (f false false x y) -- 0 0 
  putStrLn (f false true  x y) -- 0 1
  putStrLn (f true  false x y) -- 1 0 
  putStrLn (f true  true  x y) -- 1 1
  where x = "true"
        y = "false"

We can run it and test xor in GHCi like this:

*Main> table xor
false
true
true
false

Which is exactly what we expect.

Bonus Optional Morte Implementation!

Now, since i’ve recently been reading about Gabriella Gonzalez’s very intriguing morte language, I thought I would attempt an implementation of the and function in it. The code below, when run through morte, will output the result of reducing “and true true” as much as possible. Naturally, this should result in “true”.

Caveat lector: This may not be the simplest (or best) way to write this function. I have used “forall” in many places where it may be unnecessary. I am including it here because it was tricky to get right :)

-- Let binding for "true" and "false"
(  \(true  : forall (a : *) -> a -> a -> a)
-> \(false : forall (a : *) -> a -> a -> a)
-> (
    -- Let binding for the "and" function
      (  \(and :  (forall (a : *) -> a -> a -> a)
               -> (forall (a : *) -> a -> a -> a)
               -> (forall (a : *) -> a -> a -> a)
          )
         -- Actual "body" of the program: reduce the function "and true true"
      -> and true true
      )
      -- definition of and
      (   \(f : forall (t : *) -> t -> t -> t)
       -> \(g : forall (t : *) -> t -> t -> t)
       -> f (forall (a : *) -> a -> a -> a)
            (g (forall (a : *) -> a -> a -> a) true false)
            false
      )
   )
)

-- Definitions of true and false:
(\(a : *) -> \(x : a) -> \(y : a) -> x) -- true
(\(a : *) -> \(x : a) -> \(y : a) -> y) -- false

We can see that it is reduced to an expression with type equivalent to our Haskell’s Boolean, with a definition corresponding to true (i.e., a function returning its first argument).

-- Type
∀(a : *) → a → a → a
-- Reduced function
λ(a : *) → λ(x : a) → λ(y : a) → x

Replacing “and true true” in the code with “and true false” will naturally result in the definition of false:

λ(a : *) → λ(x : a) → λ(y : a) → y

If you found this interesting, I recommend the Wikipediage page on Church Encoding. It shows encodings for many other types, including natural numbers (Church numerals) and lists.