# 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 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.