# 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 Gabriel 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 —