Lambda Calculus Through JavaScript, Part 1

This article was originally published at 47deg.com on December 22, 2020.

Lambda calculus is one of the pinnacles of Computer Science, lying in the intersection between Logic, Programming, and Foundations of Mathematics. In our case, we will look at it as the minimal (functional) programming language; and see how we can build the rest of a “proper” language on top of it.

Most descriptions of lambda calculus present it as detached from any “real” programming experience, with a level of formality close to mathematical practice. Fortunately, this is far from true! You likely have an interpreter of lambda calculus on your computer: any interpreter of JavaScript. You can either open the Developer Tools in your favorite browser, or start the Node.js REPL using node in a terminal.

> const id = a => a
undefined
> id
[Function: id]
> id(3)
3

Here are the rules that you and I are going to follow in order to use JavaScript as lambda calculus mandates:

1. Our definitions may only use anonymous functions, function calls, and references to function arguments;
2. Every function must take one single argument at a time, variable => body;
3. Functions may be composed of just one single expression; in practice we can_not_ use blocks of statements with curly braces, just expression-like bodies.

We can actually relax those hard requirements at the beginning. For example, until we introduce numerals – the way we encode numbers in lambda calculus – we’ll use the built-in numbers in code blocks, as we have done above.

The second requirement may look constraining, but it’s really not. Suppose we want to define a function that adds two numbers; our first impulse may be to define it as follows:

const add = (x, y) => x + y

This contradicts the aforementioned rule. The trick here, known as currying, is to create a sequence of nested functions, each one taking a single argument at a time:

const add = x => y => x + y

This is just the first of many tricks – in the good sense of the word – that we’ll use to reach our goal of building every single piece of programming from this very small and strict set of elements.

The many forms of lambda calculus

Lambda calculus is like ice cream: it comes in different flavors (the best of course being turrón). In this case, each flavor refers to a different type system superimposed on the functions themselves. In this post, we talk about untyped lambda calculus, the one in which there is no restriction! JavaScript is dynamically typed, so that choice is a natural one. Untyped lambda calculus was the first one being studied by Alonzo Church, its creator, because it focuses on the fundamental aspects of computation: defining and calling functions.

The simplest way to add types to the untyped lambda calculus is known as simply typed lambda calculus (or STLC). Each element in the language has one single type associated to it.

const add = (x : number) => (y : number) => x + y

STLC falls short because you cannot talk about polymorphic functions – in other words, you would need to define different id functions for each type. If you have used generics in Java, Kotlin, TypeScript, etc., you’ll surely know how to do it once and for all:

const id: <U>(x: U) => U = x => x

In academic circles, the extension of lambda calculus with polymorphic types is known as System F. However, it’s not the simple version we see here; in actual System F, you need to explicitly introduce or provide types as you do for other parameters:

// fake syntax for introducing types
const id = (type U) => (x: U) => x
// fake syntax for applying types
const isStillTrue = id(type bool)(true)

Several languages, the most popular being Haskell, use System F as logical core. GHC – the main Haskell compiler – in fact translates all the code written by the programmer to this very explicit syntax as one of the steps in the compilation pipeline.

Given that System F requires too many annotations, Hindley, Damas, and Milner invented a more restricted yet practical system; this was the basis for the surface language of Haskell and ML (the programming language, not Machine Learning or the car) until a few decades ago. In HM (as it is usually abbreviated), every type can be inferred and will get the best possible type.

Nowadays, people are looking at dependent types, which allow types that have values inside them. In dependently-typed languages, types are first-class, in the sense that they can be arguments and returned from functions. There are even more subtleties and distinctions: most of them are summarized in the so-called Lambda Cube.

Binding with consts

After the short digression, let’s move back to playing with lambda calculus. Well, “playing” may not be the right word, given the onerous constraints we have. Couldn’t we turn it into a proper programming language? Like one with variables (immutable, of course), conditionals, and loops?

Sure we can! As done previously with functions of multiple arguments, the trick is to encode what we want in lambda calculus form. Whenever we want to express something of the form:

const x = something
rest

we are going to translate it as follows:

(x => rest) something

We create a function that gives with an argument of the right name, so that using it in the rest is OK. The computation for something is then executed, and passed as the value of that x.

Let’s look at an example to make things clearer. The following function computes the norm (or squared length) of a vector (x, y). We have split the computation of each square into its own variable:

const norm = x => y => {
  const sqX = x * x
  const sqY = y * y
  return sqX + sqY
}

The “trick” then translates such code into one that fulfills all the constraints of lambda calculus.

const norm = x => y => ( sqX => ( sqY => sqX + sqY ) (y * y) ) (x * x)

If you open the Node.js REPL and type that function, everything works as expected:

> norm(3)(2)
13
> norm(0)(0)
0

Enough for today

We’ve worked a lot, but unfortunately we are still far from a “proper” language: we are still missing a way to take different branches (conditionals) and to repeat computations (with loops or recursion). Stay tuned for the upcoming posts!