Church-encoded natural numbers by Mark Seemann
Natural numbers don't have to be built into programming languages. An introduction for object-oriented programmers.
This article is part of a series of articles about Church encoding. The previous article, about Church-encoding of Boolean values, concluded with the question: how do you determine whether an integer is even or odd?
That sounds easy, but turns out to be more complicated that you might think at first glance.
Built-in options #
How would you normally check whether a number is even? In some languages, like Haskell, it's built into the base library:
Prelude> even 1337 False Prelude> even 42 True
In C#, surprisingly, I don't think it's built-in, but it's easy to implement a method to answer the question:
public static bool IsEven(this int i) { return i % 2 == 0; }
You could implement an IsOdd method either by using the != operator instead of ==, but otherwise copy the implementation of IsEven; or, alternatively, call IsEven and negate the result.
This works fine in normal C# code, but in this article, the agenda is different. We're investigating how programming with the previous article's IChurchBoolean API would look. The above built-in options use Boolean language primitives, so that's not really instructive.
Boolean conversions #
It's easy to convert between Church-encoded Boolean values and built-in Boolean values. For reasons I'll explain shortly, I still don't think that's instructive in this particular context, but for good measure I'll cover how to do it.
A method like the above IsEven returns bool. If you, instead, want an IChurchBoolean, you can use this simple conversion method:
public static IChurchBoolean ToChurchBoolean(this bool b) { if (b) return new ChurchTrue(); else return new ChurchFalse(); }
Alternatively, you can also use the ternary operator, but an ugly cast is necessary to make the C# compiler happy:
public static IChurchBoolean ToChurchBoolean(this bool b) { return b ? (IChurchBoolean)new ChurchTrue() : new ChurchFalse(); }
Regardless of which implementation you choose, you'd be able to interact with the result as an IChurchBoolean values, as this small interactive session demonstrates:
> 42.IsEven().ToChurchBoolean().Match("Even", "Odd") "Even" > 1337.IsEven().ToChurchBoolean().Match("Even", "Odd") "Odd"
Still, converting from bool to IChurchBoolean doesn't address the underlying question: is it possible to write programs without built-in Boolean primitives?
The conversion function ToChurchBoolean uses built-in Boolean values and functions, so it doesn't show whether or not it would be possible to make do without those.
Before we abandon that line of inquiry, however, I think it's only fair to share a conversion method that goes the other way:
public static bool ToBool(this IChurchBoolean b) { return b.Match(true, false); }
This function enables you to convert an IChurchBoolean value into a primitive C# bool, because when b represents true, the first argument (i.e. true) is returned, and when b represents false, the second argument (i.e. false) is returned.
Peano numbers #
If we can't use built-in primitives or operators that return them (e.g. ==), we may not be able to move forward with built-in numbers, either. What we can do, however, is to follow the lambda calculus to implement natural numbers using Church encoding. This will enable us to determine if a natural number is even or odd.
Lambda calculus models natural numbers according to Peano's model. In short, a natural number is either zero (or one, depending on the specific interpretation), or a successor to another natural number. As an example, using the Successor class that I'll develop later in this article, the number three can be represented as new Successor(new Successor(new Successor(new Zero()))) - it's the number after the number after the number after zero.
Like Church-encoded Boolean values, a Church-encoded natural number is a function that takes two arguments, corresponding to zero, and a successor function:
zero = λf.λx.x one = λf.λx.f x two = λf.λx.f (f x) three = λf.λx.f (f (f x)) ...
Each of these functions takes an initial value x, as well as a function f. In the lambda calculus, neither x nor f have any implied interpretation; it's the number of applications of f that defines the number.
In most translations into programming languages that I've encountered, however, x is usually interpreted as zero, and f as the successor function. In Haskell, for example, a common way to model Peano numbers is to use a sum type:
data Peano = Zero | Succ Peano deriving (Eq, Show)
Basically, this means that a value of the Peano type can either be the atom Zero, or a Succ value. Notice that Succ contains another Peano value; the data type is recursive.
You can write Haskell values like these:
*Peano> zero = Zero *Peano> one = Succ Zero *Peano> two = Succ (Succ Zero) *Peano> three = Succ (Succ (Succ Zero))
Alternatively, you can also define the numbers based on previous definitions:
*Peano> zero = Zero *Peano> one = Succ zero *Peano> two = Succ one *Peano> three = Succ two
This variation of Peano numbers uses an explicit sum type, but as the lambda calculus representation suggests, you can also use Church encoding to represent the two cases.
Church-encoded natural numbers #
If you recall Church-encoded Boolean values, you may remember that they are functions that take two values: a value to be used in case of true, and a value to be used in the case of false. You can do something similar with natural numbers. Zero is like true and false, in the sense that it's nothing but a label without any associated data. Succ, on the other hand, contains another Peano value. The way to do that is to turn the successor case into a function. Doing that, you'll arrive at an interface like this:
public interface INaturalNumber { T Match<T>(T zero, Func<INaturalNumber, T> succ); }
The first argument, on the left-hand side, is the case to use when an object represents zero. The second argument, on the right-hand side, is a function that will ultimately produce the value associated with a successor. The implied contract here is that the INaturalNumber passed as input to succ is the predecessor to 'the current value'. This may seem counter-intuitive, but hopefully becomes clearer when you see the Successor class below. The crucial insight is that a successor value has no intrinsic value; it's entirely defined by how many predecessors it has.
The zero implementation is similar to how Church-encoding implements true:
public class Zero : INaturalNumber { public T Match<T>(T zero, Func<INaturalNumber, T> succ) { return zero; } }
Notice that the Zero class implements INaturalNumber by always returning zero, and consequently always ignoring succ.
Another class, Successor, handles the right-hand side of the Match method:
public class Successor : INaturalNumber { private readonly INaturalNumber predecessor; public Successor(INaturalNumber n) { this.predecessor = n; } public T Match<T>(T zero, Func<INaturalNumber, T> succ) { return succ(predecessor); } }
Notice that Successor composes its predecessor via Constructor Injection, and unconditionally calls succ with its predecessor when Match is invoked.
Working with natural numbers #
What can you do with this INaturalNumber API, then?
Initially, you can define some numbers, like the above Haskell examples:
public static class NaturalNumber { public static INaturalNumber Zero = new Zero(); public static INaturalNumber One = new Successor(Zero); public static INaturalNumber Two = new Successor(One); public static INaturalNumber Three = new Successor(Two); public static INaturalNumber Four = new Successor(Three); public static INaturalNumber Five = new Successor(Four); public static INaturalNumber Six = new Successor(Five); public static INaturalNumber Seven = new Successor(Six); public static INaturalNumber Eight = new Successor(Seven); public static INaturalNumber Nine = new Successor(Eight); // More memmbers go here... }
Here, I arbitrarily chose to define the numbers from zero to nine, but you could go on for as long as you care.
You can also convert these Church-encoded numbers to primitive int values, like this:
public static int Count(this INaturalNumber n) { return n.Match( 0, p => 1 + p.Count()); }
Here are some examples from a C# Interactive session:
> NaturalNumber.Zero.Count() 0 > NaturalNumber.One.Count() 1 > NaturalNumber.Seven.Count() 7
The implementation of Count is recursive. When n is a Zero instance, it'll return the first argument (0), but when it's a Successor, it'll invoke the lambda expression p => 1 + p.Count(). Notice that this lambda expression recursively calls Count on p, which is the Successor's predecessor. It'll keep doing that until it reaches a Zero instance.
Recursion is a central part of the lambda calculus; you can't do anything useful without it. If you're a C# or Java programmer, you may be concerned, because recursion tends to be problematic in such languages. Deeply recursive functions will sooner or later crash because of a stack overflow.
You shouldn't, however, be concerned. First, I'm not trying to convince you to write all your future C# or Java code using Church-encoded numbers and Boolean values. The point of this article series is to investigate the fundamentals of computations, and to gain a better understanding of sum types. As such, the code examples presented here are only demonstrations of the underlying principles. Lambda calculus itself serves the same purpose: it's a universal model of computation; it wasn't intended to be a practical programming language - in fact, there were no programmable computers in 1936.
Furthermore, the problem with recursion causing stack overflow isn't universal. Languages like F# and Haskell support tail recursion, thereby enabling recursive functions to run to arbitrary depths.
Pattern matching #
In the previous article, I hinted that there's a reason I decided to name the interface method Match. This is because it looks a lot like pattern matching. In F#, you could write count like this:
type Peano = Zero | Succ of Peano // Peano -> int let rec count n = match n with | Zero -> 0 | Succ p -> 1 + count p
This implementation, by the way, isn't tail-recursive, but you can easily refactor to a tail-recursive implementation like this:
// Peano -> int let count n = let rec countImp acc n = match n with | Zero -> acc | Succ p -> countImp (1 + acc) p countImp 0 n
Both variations use the match keyword to handle both the Zero and the Succ case for any Peano value n. That's already close to the above C# code, but using the optional C# language feature of named arguments, you can rewrite the implementation of Count to this:
public static int Count(this INaturalNumber n) { return n.Match( zero: 0, succ: p => 1 + p.Count()); }
This starts to look like pattern matching of sum types in F#. The argument names aren't required, but using them makes it clearer which cases the Match method handles.
Addition #
You can now start to add features and capabilities to the natural numbers API. An obvious next step is to implement addition:
public static INaturalNumber Add(this INaturalNumber x, INaturalNumber y) { return x.Match( zero: y, succ: p => new Successor(p.Add(y))); }
Again, the implementation is recursive. When x is zero, you simply return y, because zero + y is y. When x is a Successor, you recursively add y to its predecessor, and put the result in a new Successor. You can think of the predecessor p as one less than the successor. By recursively subtracting one from any Successor object, you'll eventually match the zero case, which will then return y. When the stack unrolls, each stack puts the previous result into a new Successor. This happens exactly the correct number of times corresponding to the value of x, because that's the size of the stack when Add hits zero.
Here are some examples:
> NaturalNumber.One.Add(NaturalNumber.Two).Count() 3 > NaturalNumber.Four.Add(NaturalNumber.Three).Count() 7 > NaturalNumber.Seven.Add(NaturalNumber.Six).Count() 13
You can also implement multiplication, but that's a bit more complicated, and not relevant to the topic of this article (which is how to determine if a number is even or odd).
Testing for zero #
In addition to basic arithmetic, you can also define functions that tell you something about a natural number. We'll start gently with a function that tells us whether or not a number is zero:
public static IChurchBoolean IsZero(this INaturalNumber n) { return n.Match<IChurchBoolean>( zero: new ChurchTrue(), succ: _ => new ChurchFalse()); }
The IsZero method simply returns a ChurchTrue object when n is a Zero instance, and a ChurchFalse object for all other numbers.
You can see that this works in this C# Interactive session:
> NaturalNumber.Two.IsZero() ChurchFalse { } > NaturalNumber.Zero.IsZero() ChurchTrue { } > NaturalNumber.Three.IsZero() ChurchFalse { }
You can also Match on the returned Boolean value to return e.g. a string:
> NaturalNumber.Nine.IsZero().Match(trueCase: "Zero", falseCase: "Not zero") "Not zero" > NaturalNumber.Zero.IsZero().Match(trueCase: "Zero", falseCase: "Not zero") "Zero"
This already demonstrates that you can implement predicates and branching logic from first principles, without resorting to built-in Boolean primitives or operators.
Detecting even numbers #
Testing whether a natural number is even or uneven requires a bit more work. It's probably easiest to understand if we first consider an F# implementation:
// Peano -> ChurchBoolean let rec isEven n = match n with | Zero -> ChurchTrue | Succ Zero -> ChurchFalse | Succ (Succ p) -> isEven p
Zero is even, so when n matches Zero, isEven returns ChurchTrue. Conversely, when the input is Succ Zero (i.e. one), the return value is ChurchFalse because one is odd.
The zero and one cases serve as exit cases for the recursive algorithm. Since we've handled Zero and Succ Zero (that is, zero and one), we know that any other case must be at least twice nested. This means that the Succ (Succ p) pattern matches all other cases. You can think of p as n - 2.
The algorithm proceeds to recursively call isEven with p (i.e. n - 2). Sooner or later, these recursive function calls will match either the Zero or the Succ Zero case, and exit with the appropriate return value.
C# doesn't have as sophisticated pattern matching features as F#, so we're going to have to figure out how implement this algorithm without relying on a nested pattern like Succ (Succ p). As an initial step, we can rewrite the function in F#, using two matches instead of one:
// Peano -> ChurchBoolean let rec isEven n = match n with | Zero -> ChurchTrue | Succ p1 -> match p1 with | Zero -> ChurchFalse | Succ p2 -> isEven p2
This isn't as elegant as the previous implementation, but on the other hand, it's straightforward to translate to C#:
public static IChurchBoolean IsEven(this INaturalNumber n) { return n.Match( zero: new ChurchTrue(), // 0 is even, so true succ: p1 => p1.Match( // Match previous zero: new ChurchFalse(), // If 0 then successor was 1 succ: p2 => p2.IsEven())); // Eval previous' previous }
Like in the F# example, when n is a Zero object, it'll return the value associated with the zero case. Since zero is even, it returns a ChurchTrue object.
In all other cases, a Match on the predecessor p1 is required. If that nested match is zero, then we know that n must have been one, since the predecessor turned out to be zero. In that case, then, return a ChurchFalse object, because one isn't even.
The nested Match considers the predecessor p1. In the succ case of the nested Match, then, we can consider p2; that is, the predecessor to the predecessor to n - in other words: n - 2. The function recursively calls itself with n - 2, and it'll keep doing so until it matches either the zero or the one case.
The implementation works:
> NaturalNumber.Two.IsEven() ChurchTrue { } > NaturalNumber.Three.IsEven() ChurchFalse { }
IsEven is implemented from first principles. The only language features we need are lambda expressions and recursion, although in order to make these examples slightly more idiomatic, I've also used interfaces and classes.
Detecting odd numbers #
You could implement a corresponding IsOdd method similarly to IsEven, but it's easier to use the Boolean operators already in place from the previous article:
public static IChurchBoolean IsOdd(this INaturalNumber n) { return new ChurchNot(n.IsEven()); }
IsOdd is simply the Boolean negation of IsEven. Like IsEven it also works correctly:
> NaturalNumber.Six.IsOdd().Match(trueCase: "Odd", falseCase: "Even") "Even" > NaturalNumber.Seven.IsOdd().Match(trueCase: "Odd", falseCase: "Even") "Odd"
You can implement other operators (like multiplication) and predicates from the building blocks shown here, but I'm not going to cover that here (see the accompanying GitHub repository for more code). I hope that this article gave you a sense of how a programming language can be designed from the low-level building blocks defined by the lambda calculus.
Summary #
Giuseppe Peano described natural numbers as an initial number (zero) and successors to that number. Church formulated Peano numbers in the lambda calculus. Using Church encoding, you can translate this representation to various programming languages, including, as you've seen in this article, C#.
In the previous article, you saw how to model Boolean values as a set of functions with two arguments. In this article, you saw how to model natural numbers with another set of functions that take two arguments. In the next article, you'll see another data type modelled as a set of functions with two arguments. It looks like a patterns is starting to appear.
Next: Church-encoded Maybe.
