[266] Church Encoding in Elixir

Or: The Coolest Thing I Know

Subscribe now

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!

Resources