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
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.
Because we have no information about the type
a, there are only two possible inhabitants,
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
xor. If you like puzzles (this one isn’t too hard), you may enjoy playing type tetris to come up with the answers :-)
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:
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:
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.
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:
if' is just the identity function, we can reduce this to the following:
Finally, recognise that if
c2 true false will be
c2 true false will be false. So we can reduce this further, to:
We can apply the same trick with
and', and it comes out looking very similar:
Not and Xor
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
c2 false true).
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:
Now all we need is the
not' function, which we already know how to write:
Alternatively, we could have written it by observing it’s simply modifying a
Boolean to take the other branch. That is:
Just in case you want to test these, here is a little function to print the truth table for a binary boolean function.
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 —