#  Church Encoding in Elixir

Or: The Coolest Thing I Know

### Church Encoding in Elixir [09.09.2016]

Alright, so in the last episode I introduced Quark. I did that because I think it's neat. We don't need it for anything we're going to do here, and I'm not 100% sure it adds anything even. However, we're going to use it to implement Church Encoding, which is a way to represent data and operators in the Lambda Calculus. It's fun I promise!

## Project

So here's the deal. Imagine we live in a world where we only have functions. We would like to have numbers. And booleans. And control flow. But we don't. We just have functions. And some concept of data (which in theory could be functions too but we'll use some arbitrary values instead).

I actually think of this as the coolest thing I know. I want to share it!

How do we get from functions to numbers? Turns out Alonzo Church figured this out in 1936 or so. Let's figure it out.

### Starting Point

So we have the project we built out in the last episode as a starting point. We want to define what numbers are. We only have functions, remember. Let's start out by defining zero and we'll explain how this works as we go.

``````  import Church # We'll make this momentarily
@x 99999 # This is just ANY VALUE AT ALL.  Use an atom.  Whatever!
def f(x), do: x - 5 # This is just any function that can operate on our values

# definition: A church numeral applies a function n times
test "church numeral 0" do
assert @x = zero.(&f/1).(@x)
end
``````

OK, so we'll claim that we can define numbers by saying we apply the function given to us n times and that's n. So for zero, we just verify that we didn't apply the function. We could make this function raise or something if we wanted to, but in general it doesn't much matter. So now let's define what `zero` is in a new Chuch module:

``````vim lib/church.ex
``````
``````defmodule Church do
import Quark.Partial
defpartial zero(_f, x), do: x
end
``````

So here we've just defined a function, using Quark.Partial (but that part's not important!), that takes two arguments and returns the second argument. The arguments are a function and a value. This is what our definition of a Church Numeral is - a function that takes two arguments: a function and a value. So this is simple enough and obviously our test will pass, so let's run it and make sure I haven't goofed anything up.

OK, that works. Now let's define one:

``````  test "church numeral 1" do
assert f(@x) == one.(&f/1).(@x)
end
``````

Here we're saying that calling `one` with our function and our value results in the function being called on the value. So that's all `one` is. Let's write this one as well:

``````  defpartial one(f, x), do: f.(x)
``````

That's...super straightforward. The test should pass. Now, let's go on and define two and call it done for now and move on past numbers:

``````  test "church numeral 2" do
assert @x |> f |> f == two.(&f/1).(@x)
end
``````
``````  defpartial two(f, x), do: f.(f.(x))
``````

This is pretty straightforward as well. We can see how we can just keep applying `f` an increasing number of times to define more numbers. This isn't that exciting yet I don't think. We'll keep moving.

We'd like to have booleans. We don't really. Let's just define a couple of things that represent true and false. First, a test on true:

``````  @y 888888
# I'm naming this function something stupid because true is a keyword.
test "church true" do
assert @x == lol_true(@x, @y)
end
``````

Here we're saying that `true` is just a function that takes two arguments and returns the first one. Why is this what true means? Because we will it to be. This is fine. If that's what true is, then false is the other thing:

``````  test "church false" do
assert @y == lol_false(@x, @y)
end
``````

OK so now we've made up what numbers are and what booleans are with just functions. Let's implement true and false - it's so easy, as expected:

``````  defpartial lol_true(a, _b), do: a
defpartial lol_false(_a, b), do: b
``````

Righto, so now all our tests still pass. Up til now we've got no real properties of our system that are valuable, so that part sucks a little. We now have enough built up that we can implement something neat though!

### The part that broke Josh's brain

Let's define a function that can tell us whether its argument is zero or something else!

This...this bit hurt my head a lot. So we'll start with a test:

``````  test "church is_zero" do
assert lol_true == is_zero(zero)
assert lol_false == is_zero(one)
assert lol_false == is_zero(two)
``````

Here we're just using functions from our `Church` module to say that we should be able to say whether this upcoming `is_zero` function works like we want. So we can kind of fake it at first:

``````  defpartial is_zero(f) do
lol_true
end
``````

OK, so this passes one test. That part's easy enough. But it's not clear (or at least it wasn't to me) where to go from here at all. I didn't even figure it out from first principles...even with some lambda-calculus definitions that showed the next step, it wasn't clear where to go next for me.

Here's the first bit of the trick. We know that zero takes two arguments and returns the second one. So we can turn this first bit into this:

``````  defpartial is_zero(f) do
f.(lol_true).(lol_true)
end
``````

So this is the same thing. The first value doesn't matter at all. Zero returns the second value. So in the zero case, this is fine, but in the other cases this isn't fine. What if we just pass `lol_false` as the first argument now?

``````  defpartial is_zero(f) do
f.(lol_false).(lol_true)
end
``````

OK so if we run this, we get a failure:

``````  1) test church is_zero (QuarkPlaygroundTest)
test/quark_playground_test.exs:72
Assertion with == failed
code: lol_false == is_zero(one)
lhs:  #Function<2.87110487/1 in Church.lol_false/0>
rhs:  #Function<13.87110487/1 in Church.lol_false/0>
stacktrace:
test/quark_playground_test.exs:74: (test)
``````

This is because we expected to get `lol_false` back but instead we got some other function. This is because in the case of something other than zero, the first argument here is applied to the value recursively some number of times. So we get an application of `lol_false` rather than `lol_false` itself. Let's just wrap `lol_false` in a function that ignores the argument and returns `lol_false` then:

``````  defpartial is_zero(f) do
l_x = fn _ -> lol_false end
f.(l_x).(lol_true)
end
``````

And this works. So let's talk through why it works.

Assume we have `zero` as `f`. Then it returns `lol_true` because that's how `zero` is defined, so that part works.

Assume we have `one` as `f`. In that case, we apply the first function to `lol_true`, which returns false...because that's what our function always returns.

Assume we have `two` as `f`. In that case, we apply the first function to `lol_true` and it returns `lol_false`. Then we apply that function again....and it still returns `lol_false`. So this function, if we apply it any times at all, will return `lol_false` every time it's applied, regardless of what it's given.

So this is neat. This right here was the eureka moment that actually made my brain feel bigger. Maybe it's silly or trivial or whatever, but it was great for me. Let's get some more stuff out of these little functions:

``````  # we want to define a boolean and that works with our true/false types
# So we want a function that satisfies these properties:
test "church and" do
assert lol_false == lol_and(lol_true,  lol_false)
assert lol_false == lol_and(lol_false, lol_true)
assert lol_false == lol_and(lol_false, lol_false)
assert lol_true  == lol_and(lol_true,  lol_true)
end
``````

So how do we do that? Let's work through it:

``````  # So here's a dumb and wrong solution
defpartial lol_and(a, b) do
a
end
``````

Run the tests and we can see that they fail. If we get them to pass, we have something that works like we want. It's worth noting, also, that we assume that `a` and `b` may only by one of `lol_true` or `lol_false`. So let's keep playing. If the first argument is true, then this returns true...but that's somewhat silly. We know that `lol_true` returns the first argument, so we can change that to something like this:

``````  defpartial lol_and(a, b) do
a.(a).(lol_false)
end
``````

So here we can sort of see a nice property. If `a` is `lol_true` then it returns itself, which is true...but of course, that won't matter. If it's false, it will return `lol_false` which is part of what we want. But it's not fundamentally any different than what we had previously in terms of the actual behaviour. But let's talk about it. If `a` is false, we'll return false here, which is what we want. If it's true, we'll return `a` itself. So what if we replace that with `b`?

``````  defpartial lol_and(a, b) do
a.(b).(lol_false)
end
``````

So this works! Neat! Why does it work? Well, because we only have four options:

1) a is false, b is true. If a is false it returns `lol_false` and we're done. 2) a is false, b is false. If a is false, it returns `lol_false` and we're done. 3) a is true, b is false. If a is true it returns b, which is false, so we're done. 4) a is true, b is true. If a is true, then it returns b. If b is true, then that means it returned true so we're done.

So we can just verify that all four cases have this outcome by looking, based on how we defined true and false. I think that's neat!

## Summary

So this kind of leaves us with...something. We have booleans and natural numbers. We have if/unless if you squint at `lol_true` and `lol_false`. The obvious next steps are to define `or` and to define less than or equal and equal. Try to implement at least `or` on your own, and maybe soon we'll look at that as well as a few more building blocks. I love this stuff...I hope it isn't boring. See you soon!