The Church numerals (WIP)

Posted on March 18, 2021 by Suguivy


Numbers are a way that we have to enumerate or to count things. We can represent they in various ways. For example, in our traditional positional numeric system numbers are represented as a sequence of symbols, in which the value of the number is determined by its symbols and their position. But we can represent it by other means.

Brief introduction to the λ-calculus

The lambda calculus (or λ-calculus) is a formal system and a model of computation based on function application.

This can sound very weird or abstract, but is not so difficult. You can think it as a programming function. For example, a function that returns its same argument can be represented as:


We can apply an argument to the function using a rule called β-reduction:

(λx.x) 1

x is binded to 1:


Also, functions in lambda calculus have only one parameter.

The Church numerals

Now that we hace introduced the lambda calculus, we will introduce the Church Numerals The church numerals are a representation of natural numbers using functions.

The numbers can be represented in Haskell as is:

    λ-calculus          Haskell                   Also Haskell
0   λf.λx.x             \f -> \x -> x             \f x -> x
1   λf.λx.f x           \f -> \x -> f x           \f x -> f x
2   λf.λx.f (f x)       \f -> \x -> f (f x)       \f x -> f (f x)
3   λf.λx.f (f (f x))   \f -> \x -> f (f (f x))   \f x -> f (f (f x))

This is:

  • The number zero is represented as a function that takes a function and a value, and returns the value.
  • The number one is represented as a function that takes a function and a value, and returns the application of the function to the value.
  • …and so on.

Representing church numerals

We are going to use Haskell and Python to represent the numerals.

We can define the number zero as is:

In Python:

def zero(f, x):
    return x

In Haskell:

To work easily, we have created a type alias:

type Church a = (a -> a) -> a -> a

zero :: Church a
zero f x = x

To work easily with the numerals, we can create two functions, one for convert integers to church numerals and vice versa:

In Python:

def zero(f, x):
    return x

def church(n):
    if n == 0:
        return lambda f,x: x
        pred_church = church(n-1)
        return lambda f,x: f(pred_church(f,x))

def unchurch(c):
    return c(lambda x: x+1, 0)

In Haskell:

church :: Integer -> Church a
church 0 = \_ x -> x
church n = \f x -> f (predChurch f x)
    where predChurch = church (n-1)

unchurch :: Church Integer -> Integer
unchurch = c succ 0