In this article, you will look at Church Numerals from another perspective. Additionally, you will explore debugging in GHCi, the interactive Haskell prompt.
Alonzo Church’s thesis states: computable things can be defined as terms in the pure untyped lambda calculus. Just as an example to show why this could be the case, let us consider functions between numbers. If the thesis holds, any computable function between numbers is definable as a lambda term.
We define Church numerals (or Church’s numbers, if you prefer) to be the following lambda terms:
 = λs.λz.z
 = λs.λz.s (z)
 = λs.λz.s (s (z))
[n] = λs.λz.sn (z)
In the equations above, we have that n stands for any number larger than zero. The notation sn is not a lambda term in itself. Instead, it is shorthand for the application of the term s, repeated n times. An illustration of this is:  = λs.λz.s5 (z) = λs.λz.s (s (s (s (s (z))))).
Observe that these Church numerals consist of two nested lambda terms. The first one binds variable s, and the second one binds variable z. We will shortly see this pattern from a different perspective.
Now we shall consider the function that adds two numbers, typically written as x+y for two numbers x and y. This function is computable and can also be defined as a term:
[x+y] = λs.λz.[x] s ([y] s z)
For example if we look at 0 + 1, we see that it is represented by the term:
[0+1] = λs.λz. s ( s z)
= λs.λz.(λs.λz.z) s ((λs.λz.s (z)) s z)
→β λs.λz.(λs.λz.s (z)) s z
=η λs.λz.s (z)
In the first line, we fill in the variables of the definition: all x’s become 0 and all y’s become 1. In the second line, we replace  and  by the definition of Church numerals as given above: here we defined that  equals λs.λz.z and that  equals λs.λz.s (z). The third line is a beta-reduction step and the fourth line is an eta-conversion. The resulting term is now equal to the definition we had for the number 1.
Numbers as Data
We will now look at Church numbers from a different perspective: as data instead of functions. For this we need Haskell because it allows us to define data types. We name the data type below after Giuseppe Peano, and we call values of this type Peano numbers:
data Peano = Z | S Peano deriving Show
The type Peano has two constructors: “Z” and “S”. In Haskell, constructors can be seen as special functions. This is evidenced by checking the type of a constructor: it is either constant or it involves the arrow we also know is used for the type of functions. For example in GHCi after entering the type Peano, we can see the type printed of expressions as below.
*Main> :t Z Z :: Peano *Main> :t S S :: Peano -> Peano *Main> :t S (Z) S (Z) :: Peano *Main> :t S (S (Z)) S (S (Z)) :: Peano
These expressions in Haskell are the Peano numbers. We could compare Peano numbers to terms of the definition of Church numerals.
The names “Z” and “S” have meaning. We could think of constructor “Z” as standing for the number zero. And the constructor “S”, having the type
Peano -> Peano, is a function between two numbers. It is the successor function: given a number, return the number that is incremented by one.
Could we then also define the function of addition? Given two numbers, return the sum of the two. Yes, and in Haskell it looks like this:
plus :: Peano -> Peano -> Peano plus Z y = y plus (S x) y = S (plus x y)
That this function is correct could perhaps best be visualized. Consider two data structures, each representing a Peano number. The plus operation moves the second number along the spline of the structure of the first number. Then it deposits the value in place of the “Z” zero constructor. The result is, indeed, the addition of two numbers.
The above figure shows an example addition of 3 and 1. On the far left side, we see the invocation of the function plus with two arguments. The Peano number for 3 as argument x and the Peano number for 1 as argument y. This is the Haskell expression:
plus (S (S (S (Z)))) (S (Z)).
In GHCi we can start the debugger on an arbitrary expression using
:set stop :list command shows the current context and the next expression to evaluate. We apply it to our case:
*Main> :set stop :list *Main> :step plus (S (S (S (Z)))) (S (Z)) Stopped in Main.plus, Test.hs:9:16-27 _result :: Peano = _ x :: Peano = S (S Z) y :: Peano = S Z 8 plus Z y = y 9 plus (S x) y = S (plus x y) 10
GHCi is ready to evaluate the next expression on line, as underlined. We then use
:step to proceed step by step through our program.
[Test.hs:9:16-27] [Test.hs:9:16-27] *Main> :step S Stopped in Main.plus, Test.hs:9:19-26 _result :: Peano = _ x :: Peano = S (S Z) y :: Peano = S Z 8 plus Z y = y 9 plus (S x) y = S (plus x y) 10
Notice how the string “S ” is printed before “Stopped in Main.plus”: this is the regular output what we would expect from evaluating the expression. By stepping through the function, we encounter four different contexts. A context is a set of variables (_result, x, y), their types (Peano) and assigned expressions. If we look closely from left to right in the previous figure, we can see that precisely these contexts are depicted.
The plus function is defined in a special way: first, it traverses down the structure of the first argument until it reaches zero. Then for the zero case, we use a constant value. Finally, for the non-zero cases, we apply again the successor function.
We can generalize this to a traversal function, also called catamorphism or folding function. A traversal function takes as argument a value of some data type, and takes as arguments functions that are compatible with the constructors of the data type. Intuitively, the result is where in the value all constructors are replaced by the supplied functions. Moreover, any data type has a corresponding traversal function.
For Peano numbers, we can now choose to replace its two constructors “Z” and “S” by compatible functions. By compatibility we can at least think of functions of the same arity as the constructor: “Z” has arity zero, “S” has arity one. In Haskell we write:
cata :: Peano -> (a -> a) -> a -> a cata Z s z = z cata (S x) s z = s (cata x s z)
The first argument is of type Peano and represents any Peano number. The last two arguments of this function have the same type as the constructors “Z” and “S” for the type Peano, except that we have replaced Peano by the universally quantified type variable α. The return type is also α. The traversal function is polymorphic.
We now turn to different applications of this traversal function. A trivial application is the identity function. For any Peano number n we have the equation:
cata x S Z = x
Replacing the constructor “Z” by constructor “Z” and the constructor “S” by constructor “S” results in precisely the same value. Another application of the traversal function is to give an alternative definition of the successor function:
cata x S (S (Z)) = S (x)
Replacing the constructor “Z” by Peano number 1 and replacing the constructor “S” by itself results in a number larger by one. We could also define the doubling function as follows:
cata x (λx.S (S (x))) Z
Replacing the constructor “Z” by itself and the constructor “S” by a function that applies “S” twice results in a number that is twice as big.
This is indeed a generalization of plus as before. We could write the function plus as:
plus :: Peano -> Peano -> Peano plus x y = cata x S y
And continue towards defining multiplication and exponentiation similarly. Observe that the multiplication of two numbers, n and m, is the repeated application of n times adding m. If, however, n is zero then the result is also zero. We could write this function as:
multiply :: Peano -> Peano -> Peano multiply x y = cata x (plus y) Z
The first argument is the number which determines the number of repeated additions. Hence, we traverse over the first argument. We replace the constructor “Z” by itself and the constructor “S” by the partial application of plus with the second argument. As an illustration why this works, consider these concrete examples:
=(3+) ((3+) ((3+) ((3+) 0)))
=(3+) ((3+) ((3+) 3))
=(3+) ((3+) 6)
=(4+) ((4+) 4)
Similarly, exponentiation of number m by the exponent n is the repeated application of n times multiplying by m. If n is zero then the result is one.
expo :: Peano -> Peano -> Peano expo x y = cata y (multiply x) (S Z)
4^3=(4⋆) ((4⋆) ((4⋆) 1))
=(4⋆) ((4⋆) 4)