# 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
= x
true x y
false :: Boolean
= y false x 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 then x else y if' c x 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
= cond x y
if' 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
= if' c1 true (if' c2 true false) orWithIf c1 c2
```

Now, since `if'`

is just the identity function, we can reduce this to the following:

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

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
= c1 true c2 or' c1 c2
```

### And

We can apply the same trick with `and'`

, and it comes out looking very similar:

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

### 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
= c1 (c2 false true) (c2 true false) xor' c1 c2
```

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
= c1 (not' c2) c2 xor c1 c2
```

Now all we need is the `not'`

function, which we already know how to write:

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

Alternatively, we could have written it by observing it’s simply modifying a `Boolean`

to take the other branch. That is:

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

## 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 ()
= do
table f 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"
= "false" y
```

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.

Paul —