# Let’s code the roots of Functional Programming: Lambda calculus implemented in Typescript

### Prelude

This is an article about Typescript and Functional Programming. It is not an article about Lambda calculus theory.

We will implement Lambda calculus in Typescript as a way to exercise Functional Programming. We will do this solving a simple problem using only Lambda calculus constructs.

In the end, maybe, also the basics of the theory may result clearer.

### The problem and the language

The problem to solve is simple: if 2 numbers `n` and `m` are equal, then return `n + m` otherwise, return `m — n`.

But we have a language that allows us only to use the following construct

`x => y  // anonymous function with 1 parameter (i.e. unary function) `

where `x` and `y` can be everything. `x` and `y` can even be functions, so that also the following is a valid construct in our language

`x => y => z => z(x)(y)  // x is the parameter and the value returned is y => z => z(x)(y)`

In other words, to solve the problem we have just anonymous functions (a.k.a. “fat arrow” functions). No Javascript native `numbers`, no `==` or `===` operators, no `if then else`. Just functions. Remember, for the rest of the article, that

we have just functions.

#### Lambda calculus

Lambda calculus gives us the theoretical basis to solve this problem using just functions. Actually, Lambda calculus solves any computable problem using just functions.

What is Lambda calculus? There are many sources which provide good descriptions. For the purpose of this article, Lambda calculus is simply the fact that we can use just anonymous functions to solve our problem.

Here we want to see how we can make concrete this concept, implementing Lambda calculus with Typescript and solving, through it, our problem. In the process, we will use extensively, or better, exclusively functional programming techniques, since

we have just functions.

Considering that Lambda calculus is also at the basis of Functional Programming, then yes, we can say we are going to code the roots Functional Programming in Typescript.

The complete code for the solution of the problem and additional Lambda calculus constructs can be found here.

### Numbers without numbers

Our problem starts with 2 numbers but we can not use Javascript numbers since

we have just functions.

So we need to invent a way to define the concept of a number using functions.

Let’s start saying that the numbers ZERO, ONE and TWO are represented respectively by

`ZERO = f => x => x        // in lambda calculus this is λf.λx.x ONE = f => x => f(x)     // in lambda calculus this is λf.λx.fx TWO = f => x => f(f(x))  // in lambda calculus this is λf.λx.f(fx)`

If `f` is a function and `x` is any value, `ZERO` returns `x` never applying `f` to it while `ONE` returns the result of applying `f` to `x` once and `TWO` the result of applying `f` to `x` twice. So basically this is our convention: a number is represented by how many times a function `f` is applied to the argument `x`.

So the mechanism is clear. A number n represents the application of a function `f` to an argument `x` n-times. Remember this concept, we will use it later. By the way, this is called Church encoding of numbers. It is the convention used by the inventor of Lambda calculus, Alonzo Church, to represent natural numbers.

#### The Successor function

So far we have hardcoded the first 3 numbers, but we need to find a more flexible way, a smarter way to define numbers. This way is provided to us by the Successor function

`SUCC = n => f => x => f(n(f)(x)) // equivalent to λn.λf.λx.f(nfx)`

It does not look immediate, right? But let’s reason about it.

Let’s start with the case of `n` equal to `ZERO`. If `n` is `ZERO` (remember that `ZERO` has been defined as `f => x => x`) than applying `SUCC(n)` to `ZERO`, i.e. substituting `n` with the definition of `ZERO`, we get Substitutions in SUCC(ZERO) to reach ONE

If we try `SUCC(ONE)` applying the same mechanical substitution we obtain `TWO`. Then `SUCC(TWO)` is `THREE` and so on and so forth.

#### Few words about currying

We just defined

`SUCC = n => f => x => f(n(f)(x))`

To be pedantic we can say that `SUCC`is a function that takes one parameter, `n`, and returns a function that takes one parameter, `f`, and returns a function that takes one parameter, `x`, and eventually does something with `n` `f` and `x`.

So we can actually say that `SUCC` is a function of 3 parameters, `n` `f` and `x` and that these parameters are applied one at the time. This partial application of single parameters is called currying.

From now on we will freely talk about functions of m parameters, with m ≥ 1, even if behind this concept there is always the currying mechanism since Lambda functions by definition are unary, i.e. accept only 1 parameter.

#### Let’s add some Types

If we look at the structure of a number, as defined by our convention, we see 2 things

• a number is a function that takes 2 parameters, `f` and `x`, and returns something
• the first parameter `f` must itself be a unary function since it can be applied to `x` in the body of each number

So we can start defining some types in Typescript

`type uF = (x: any) => any;                 // unary functiontype NUMBER = (f: uF) => (x: any) => any;  // the type of numbers`

And then also the function `SUCC` can be typed

`SUCC = (n: NUMBER): NUMBER => (f: uF) => (x: any) => f(n(f)(x));`

Typescript gives us the opportunity to add types to function definitions, which can be of great help in guiding us, via Intellisense and type checking, specifically when the problems we want to solve get complicated.

#### But if these are “numbers” can we see them as normal numbers?

Church encoding for numbers is about applying a function to an argument n-times. This is all good, but …

Can we see them as normal numbers, as 0, 1, 2, 36, 49, 112?

Yes, we can. If we pass as `f` a function that increments by 1 a Javascript number and as `x` the JavaScript number 0, we obtain the Javascript number corresponding to the Church encoded number, as we can see in the following example.

At the same time, if we change the function `f` and the initial value, then we can see our Church encoded numbers with different formats. Here, for instance, a Church number n is turned into a string of n characters `*`.

### Booleans without booleans

With booleans, we have to face the same problem as with numbers. We need to define True and False in a language that does not have such concepts, a language where

we have just functions.

Again we revert to a convention. Here the intuition: in the Javascript ternary operator, `condition ? first : second`, True means to choose the first option and False means to choose the second.

We use the same convention here, the Church encoding for Booleans, i.e.

`// TRUE and FALSE are binary functions, they expect 2 parametersTRUE  =  x => y => x   // TRUE returns the first parameterFALSE =  x => y => y   // FALSE returns the second parameter`

We will now see how this convention actually turns out to work well with boolean operators.

#### The AND function

Now let’s see how we can build a function which behaves like `AND`, i.e. it has to expect 2 Church encoded boolean arguments, `p` and `q`, and returns `TRUE` only if both arguments are `TRUE`.

`AND` must have the following form

`AND = p => q => ....   // p and q are Church encoded booleans`

`p` and `q` are the only things we have, so we better use them in the body of the function.

We try to start the implementation of the body with `p` , which itself is a binary function since it is a Church encoded boolean.

`AND = p => q => p(_)(_)  // p expects 2 arguments`

If `p` is `FALSE` , by definition of `FALSE` it chooses the second argument. But if `p` is `FALSE`, then the result of `AND` has to be `FALSE` and therefore the second argument after `p` must be `FALSE`.

`AND = p => q => p(_)(FALSE) // if p is false it selects the 2nd arg`

If `p` is `TRUE` then by definition of `TRUE` the first argument after `p` is chosen. But in this case the result of `AND` depends on the value of `q`. If `q` is `TRUE` then the result is `TRUE` , `FALSE` otherwise. But this means that the first argument after `p` is `q` itself.

`AND = p => q => p(q)(FALSE) // if p is true it selects q as result`

We can now make the last simplification. The second argument of `p` is `FALSE` and is chosen only when `p` is `FALSE`. Which means that we can substitute `FALSE` with `p` for the final version of the function

`AND = p => q => p(q)(p)`

Even the symmetric version works

`AND = p => q => q(p)(q)`

With similar methods, all other boolean operators can be found.

We can add types to the Church encoded booleans and test the correctness of our logic as in this example.

### Comparisons without comparison operators

Our problem asks us to compare 2 numbers, but we do not have comparison operators like `==` or `===`,

we have just functions.

We need to find a different strategy. Bear with me on this journey.

One way to check whether 2 numbers `n` and `m` are equal is to check whether `n` is lessThanOrEqual to `m` and `m` is lessThenOrEqual to `n`. Assuming we have a function `LEQ(m)(n)` that returns `TRUE` if `m`is lessThanOrEqual `n`, we can then define the `EQ` function as

`EQ(m)(n) = AND (LEQ(m)(n)) (LEQ(m)(n))`

Now we need to define `LEQ`.

Let’s assume we have 2 functions, SUB and ISZERO, defined as follows:

• `SUB(m)(n)` subtracts `n` from `m` so that, if `n` is greater than `m` , the result is always `ZERO` otherwise, it is `m-n`
• `ISZERO(n)` returns `TRUE` if `n` is `ZERO`, `FALSE` otherwise

We can now express `LEQ` as

`LEQ(m)(n) = ISZERO(SUB(m)(n))`

Well, we are now left with the problem of defining `ISZERO` and `SUB`.

#### Check if a number is ZERO

`ISZERO` is a function which expects a Church encoded number as its parameter. A Church encoded number `n` is itself a binary function, and it is the only thing we are given so we better use it somehow

`ISZERO(n) = n(x)(y) // we need to find the right x and y`

Let’s start with the case where `n` is `ZERO,` i.e. `n = f => x => x`. `ZERO` by definition always returns the second parameter, therefore `y` must be `TRUE`.

`ISZERO(n) = n(x)(TRUE) // we need to find the right x for n not ZERO`

Now let’s consider `n = ONE`, i.e. `n = f => x => f(x)`. In this case, `f` must return always `FALSE` for any value of `x`. Which means that `f = x => FALSE`.

So eventually `ISZERO` is

`ISZERO(n) = n(x => FALSE)(TRUE)`

We can test this with the following code

#### Subtract `n` from `m`

If we had a function `PRED(n)` which returns the predecessor of `n` then we could say that to subtract `n` from `m` is equivalent to apply n-times the `PRED` function to `m`. But, if you remember what we said at the beginning when we introduced Church encoding for numbers, `n` itself represents the application of a function `f` to an argument `x` n-times. In other words

`SUB(m)(n) = n(PRED)(m)`

Now, with a leap of faith, let’s accept the following definition of PRED

`const PRED = n => f => x => n(g => h => h(g(f)))(u => x)(u => u)`

For those interested, there is an explanation of `PRED` at the end of this article.

#### Sum n to m

Similarly to how we have constructed `SUB` we can construct `SUM` using the Successor function as

`SUM(n)(m) = n(SUCC)(m)`

### Now we can construct the solution

Do we still remember the initial problem?

`if (n = m) {  return n + m;  // return the sum if n and m are equal} else {  return n — m;  // return the difference if not equal}`

Now we have all the tools to solve it with a language where

we have just functions..

Look at this

`EQ(n)(m)      // returns TRUE if n and m are equal, FALSE otherwise(SUM(n)(m))   // argument picked if EQ returns TRUE(SUB(n)(m))   // argument picked if EQ returns FALSE`

This is exactly the solution to our problem, as can be proved running the following code

More details and tests can be seen in the repo.

By the way, if we substitute `EQ` `SUM` `SUB` and all the rest of the definitions we have added as a convenience, the code for our solution is this

### Finally: What’s in it for a Functional Programmer?

We have been playing just with functions. We have defined them, passed them as arguments, expected as parameters, evaluated them. We have become more familiar with them to be used as first-class citizens in our code.

We have done some exercises which have helped us understand the dynamics and mechanics of using functions with a functional programming approach.

For instance, if we see this

`FLIP = f => a => b => f(b)(a)`

we understand that it is a way to use `f` with the order of parameters reversed. And a FLIP equivalent can be found in lodash and rambda libraries. Other magics implemented by FP libraries should now be more clear. If this is the case, we have reached the objective of this article.

### For those really interested: how to build PRED function using Pairs

What is this?

`x => y => f => f(x)(y)`

This is a pair, a 2-dimensional vector., actually the way to encode a pair with functions.

Consider the following

`const PAIR = x => y => f => f(x)(y);const myPair = PAIR(1)(2);`

`myPair` is a structure which contains `1` and `2` as its immutable values. We just need to pass a function to `myPair` to specify what we want to do with its values.

A pair of `n` and `m` can be defined using the notation `(n, m).`

If we want to get hold of the second value of a pair, we can just pass the FALSE function to the pair

`SECOND = p => p(FALSE)    // where p is a pair`

as we can test with the following code

Similarly, the function `FIRST` is

`FIRST = = p => p(TRUE)    // where p is a pair`

We can now define another function, `PHI`, as follows

`PHI = p => PAIR(SECOND(p))(SUCCESSOR(SECOND(p)))  // p is a PAIR`

PHI transforms the pair `(m, n)` into a new pair `(n, n + 1)`.

So,

• `PHI(0,0)` returns `(0,1)`
• `PHI(PHI(0,0))` equals `PHI(0,1)` which returns `(1,2)`
• `PHI(PHI(PHI(0,0)` equals `PHI(1,2)` which returns `(2,3)`

Extrapolating we can say that `n` applications of `PHI` to `(0,0)` return the pair `(n-1, n)`. Which leads to the definition of `PRED` as

`PRED = n => FIRST(n(PHI)(PAIR(ZERO)(ZERO)))`

There are other ways to construct the PRED function, but this is probably the more natural to follow.

#### Acknowledgments

This article takes inspiration from 2 great talks from Gabriel Lebec (@glebec) “Lambda Calculus” and “A flock of functions”. I really recommend anybody interested in the argument to watch them carefully.