The Church Code

You may have heard of the lambda calculus, in which everything is a function. And you may have asked yourself, as I have, ok that's great, but I how do I do anything with just functions? How do I create all those datastructures I've become acustommed to? Do I need to build the datastructures I've become accustomed to? If so, how do I do it?

One answer to this question, is the Church encoding, named after Alonzo Church who first came up with the idea. So how do you use Church encoding?

Well, before I get into that I'm going to describe the environment I'm going to use. I'm going to use the ruby programming language, because it's familar to me, and Haskell's type system makes it difficult to use Church encoding. Secondly I'm gonna define a convience method in ruby called curry:

def curry(&l)
  lambda { |a| lambda { |b| l[a,b] } }
end

curry takes a block of two arguments and transforms it into a Proc w/ a single argument that returns another Proc of a single argument. This is just to save me typing later.

Now that that's out of the way we can start talking about how to turn our functions into values. Consider one of the simplest values in most programming languages, true and false.

# we are going to use the names ctrue and cfalse because
# ruby takes exception to our using true and false
# as variables
ctrue = curry { |a,b| a }
cfalse = curry { |a,b| b }

Now if you didn't stop reading a while ago because you already know all about this stuff, you may be wondering, how are those functions true and false? Actually, let's just make sure that curry method makes sense first.

curry { |a,b| a } -->
lambda { |a| lambda { |b| a } }
# So to call ctrue we'd do the following:
ctrue[1][0] #=> 1

The reason for currying all these functions should become clear fairly soon. Now that that's out of the way, how does this give us true and false? Well, think about an if statement. Now imagine if was defined as a function, like the following:

cif = lambda { |condition| curry { |true_branch, false_branch|
  condition[true_branch][false_branch] } }

Now we can for instance write not:

cnot = lambda { |cond| cif[cond][cfalse][ctrue] }

Now if you've picked up on what's going on with cif you've realized that it's not really necessary. ctrue and cfalse are true and false, and they are also if.

So we can write cnot as

cnot = lambda { |cond| cond[cfalse][ctrue] }

And if we cheat for a moment, we can discover which value a given church encoded boolean is by using the following function

cbool_to_rbool = lambda { |cond| cond[true][false] }

Now we can make sure our cnot method works

>> cbool_to_rbool[ctrue]
=> true
>> not_ctrue = cnot[ctrue]
=> #<Proc:0x02b9876c@(irb):1>
>> cbool_to_rbool[not_ctrue]
=> false

So now what? We've managed to come up with bools out of functions. Doesn't seem very useful yet, although maybe kind of entertaining.

Well we can now also define and and or. A and B is true if A is true and B is true. Put another way, A and B is true if neither A nor B are false.

cand = curry { |a,b| a[b][a] }

So let's walk through this function
if a is true, it will take a the left value and give us b. If b is true, we have true and true -> true, which is what we wanted. if b is false, we have true and false -> false which is again, what we wanted. If a is false, we get a so we had false and anything -> false, which is what we want as well.

Next we can define or.

cor = curry { |a,b| a[a][b] }

If is a true, we get a, if a is false we get b. Therefore we will only get a false result if both a and b are false. Now that we have and, or and not, we can build boolean operation (xor, etc.), and we've done it using only functions. No datastructures in sight.

The next thing we are going to try, is to create some datastructures out of pure functions. The first thing we will create is a pair, that is a list of two values.

cpair = curry { |a,b| lambda { |f| f[a][b] } }
cfst = lambda { |apair| apair[ctrue] }
csnd = lambda { |apair| apair[cfalse] }

cpair is a 3 argument function, it takes the first value for the pair, the second value for the pair, and a function that takes two arguments to use the pair.cfst will let us extract the first value from a pair, and csnd will allow us to extract the second value from a pair. Let's try it out:

>> pair_of_values = cpair["Ok"][5]
=> #<Proc:0x02b7ec40@(irb):12>
>> csnd[pair_of_values]
=> 5
>> cfst[pair_of_values]
=> "Ok"

Now you can see the purpose of using curried functions. It makes it easier for us to partially apply our functions so we can perform multiple operations with an argument of true, selecting the first value. You can also see that we can if we want create tuples of any arity. Since we already have true and false, one way to encode numbers could be to have an N-tuple of bits (true and false) and define the arithmetic operators in terms of logical operations on bits, like the way the ALU of a processor works. An interesting idea, but this is not how Church actually defined numbers with functions.

Instead, he represented natural numbers as the nth composition of a function with itself:

zero = curry { |f, x| x }
one = curry { |f,x| f[x] }
two = curry { |f,x| f[f[x]] }

Writing this definitions can be a bit tedius, so we can define a successor function:

succ = lambda { |n| curry { |f,x| f[n[f][x]] } }
three = succ[two]
four = succ[three]
.
.
.

We also define a function to convert our church numerals to ruby integers so we can see what's going on:

cnum_to_rnum = lambda { |n| n[lambda { |x| x + 1 }][0] }

>> cnum_to_rnum[two]
=> 2

What's happening is that n is composing the function lambda { |x| x + 1 } n times, so in the case of two, it is twice. We then feed it an initial value of zero, so 0 + 1 + 1 = 2.

We can also add our church numerals

plus = curry { |m,n| curry { |f,x| m[f][n[f][x]] } }

>> cnum_to_rnum[plus[two][four]]
=> 6

We can also define multiplication, a predecessor function etc. But I'm getting bored of church numerals so lets move on into how you create algebraic data types. This is going to allow us to create linked lists, trees, pretty much any data structure you can have in a pure functional language.

In Haskell, there is a type Maybe a, (ML has the same type, only they spell it 'a option). The definition in Haskell looks like:

data Maybe a = Just a | Nothing

That is, any value of Maybe Int for instance will either be Nothing or Just some integer value.

We can define this same data structure using just functions. Each constructor, Just and Nothing will be a function. Each value of Maybe a will be a function that takes a function (a -> b) and a value ( b ).

just = lambda { |value| curry { |f,x| f[value] } }
nothing = curry { |f,x| x } # if you recall this is also the definition of cfalse

Haskell also has a type Either a b whose definition looks like:

data Either a b = Left a | Right b

You may have noticed that Maybe a is just a special case of Either a b where we don't care about the second value. Again, we can define this type using only functions. We will have two functions left and right. Both will take a value, and return a function that takes two arguments, two functions, one from a to c and the other from b to c.

left = lambda { |value| curry { |f,g| f[value] } }
right = lambda { |value| curry { |f,g| g[value] } }

Given that an N-tuple can be represented in pairs, and that nested Eithers give us all the sum-types we need we can represent almost any datatype you can define in Haskell (barring things like strictness annotations, FFI, etc.) using pure functions.

For instance, we can define a linked list. In Haskell the definition might look like:

data List a = Cons a (List a) | Empty

Like maybe or either we will have two constructor functions cons, and empty
cons will take two inputs, a head and a tail and return a function taking two functions. The first one will take as parameters the head and the tail, the second will be a value to use if the list is empty. Empty will simple be a function that takes two functions, with the same parameters as the function returned by cons.

cons = curry { |h,t| curry { |cf, ev| cf[h][t] } }
empty = curry { |cf, ev| ev }

Now we can write first and rest to get the first item of the list
and the rest of the list:

first = lambda { |alist| alist[ctrue][nil] }
rest = lambda { |alist| alist[cfalse][nil] }

>> list = cons[1][cons[2][empty]]
=> #
>> h = first[list]
=> 1
>> t = rest[list]
=> #
>> first[t]
=> 2

We can also write the function map for instance:

map = curry { |f,l| l[curry { |h,t| cons[f[h]][map[f][t]] }][empty] }

>> l2 = cons[1][cons[2][cons[3][empty]]]
=> #<Proc:0x00002b1909def588@(irb):10>
>> l3 = map[lambda { |x| x.to_s }][l2]
=> #<Proc:0x00002b1909def588@(irb):10>
>> first[l3]
=> "1"
>> first[rest[l3]]
=> "2"
>> first[rest[rest[l3]]]
=> "3"

Given that we've defined church numerals earlier we can of course use them instead of
ruby numbers. Strings can be represented as lists of characters, and characters as integers, which again can be represented using church numerals. Basically, all you need are functions. I hope you've learned something, or were at least mildly entertained.