Church Booleans

In the last post, I covered the basics of Lambda calculus and its lack of built-in data types. Church encoding defines a way to represent data types as pure functions. In this post, I'll explore church booleans and control flow, and implement them using Python.

Booleans as functions

Booleans are plain functions that take two arguments.

• true always returns the first argument,
• false always returns the second argument.

𝛌a.𝛌b a   # True
𝛌a.𝛌b b   # False

In Python, I can define these two functions for booleans.

def true(a, b):
    return a

def false(a, b):
    return b

true(1, 2)  # -> 1
false(1, 2) # -> 2

To understand why this works more clearly we'll look at control flow.

Control flow constructs in Python

In Python, if is a special language construct that looks like this:

if TRUE:
  BRANCH 1
else:
  BRANCH 2

Why can't it be a function? I'll try to define if as a function using the boolean functions.

def bad_if(bool_func, b1, b2):
    return bool_func(b1, b2)

If the implementation is correct, it must evaluate exactly one branch. To check this, I'll call the bad_if function with two branches.

>>> bad_if(false, 2+2, 2-2)
0
>>> bad_if(true, 2+2, 2-2)
4

At first glance it looks correct. But we need to make sure that Python isn't evaluating both branches. I'll call bad_if with two print statements instead.

>>> bad_if(true, print("Branch 1"), print("Branch 2"))
Branch 1
Branch 2

This shows that Python did actually evaluate both branches. This happens because Python eagerly evaluates the arguments before the function call. It then passes the value of the evaluation to the function. So the bad_if call is equivalent to this:

b1 = print("Branch 1")   # -> None
b2 = print("Branch 2")   # -> None
bad_if(true, b1, b2)     # -> None

Because of the eager evaluation, Python needs a special syntax for control flow to avoid accidentally evaluating both branches.

Conditionals in Lambda Calculus

In contrast to Python's eager evaluation, Lambda calculus only evaluates the arguments when β-reduction requires the value. So a function call similar to bad_if behaves very differently in Lambda calculus.

bad_if(true, print("Branch 1"),
             print("Branch 2"))
true(print("Branch 1"), print("Branch 2"))   # Reduce bad_if
print("Branch 1")                            # Reduce true, returns first argument.

Because of lazy evaluation, if the argument is not used then it will not be evaluated. So, we can define if as a pure function in Lambda calculus.

𝛌f.𝛌a.𝛌b (f a b)

To force lazy evaluation in Python, we can wrap the branches in a Lambda. We can then call the functions returned by the boolean function.

def good_if(bool_func, b1, b2):
    # Notice we are calling the result from bool_func.
    return bool_func(b1, b2)()

I'll call the good_if with two branch lambdas. We can see that it correctly evaluates exactly one branch.

>>> good_if(true, lambda: print("branch 1"), lambda: print("branch 2"))
branch 1
>>> good_if(false, lambda: print("branch 1"), lambda: print("branch 2"))
branch 2

Conclusion

Church encoding shows how expressive Lambda calculus can be, and how higher-level constructs can be built from regular functions. There's much more to explore in future posts.