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 SUCCis 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 function
type 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.
<a href="https://medium.com/media/77261fbb7fdee1e7b8140a6d2b5228c7/href">https://medium.com/media/77261fbb7fdee1e7b8140a6d2b5228c7/href</a>
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 *.
<a href="https://medium.com/media/be5016fdea3f14b53596285aa0d9d0a0/href">https://medium.com/media/be5016fdea3f14b53596285aa0d9d0a0/href</a>
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 parameters
TRUE = x => y => x // TRUE returns the first parameter
FALSE = 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.
<a href="https://medium.com/media/4f39743032023adaed9b994a69d405f7/href">https://medium.com/media/4f39743032023adaed9b994a69d405f7/href</a>
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 mis 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
<a href="https://medium.com/media/c52c59a10d776a04b27899b0645cb532/href">https://medium.com/media/c52c59a10d776a04b27899b0645cb532/href</a>
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
<a href="https://medium.com/media/49b5b159cf0e2ecf35d0aaf9a7d8c394/href">https://medium.com/media/49b5b159cf0e2ecf35d0aaf9a7d8c394/href</a>
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
<a href="https://medium.com/media/6b0aa36f72609a05ded3a0f34699a2b8/href">https://medium.com/media/6b0aa36f72609a05ded3a0f34699a2b8/href</a>
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
<a href="https://medium.com/media/8c72c636ccd892a149316b185aad532d/href">https://medium.com/media/8c72c636ccd892a149316b185aad532d/href</a>
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.