Lambda Calculus in TypeScript Types

Implementing lambda calculus ONLY in TypeScript types.

After watching this video from Truttle1 about things you can do in TypeScript’s type system, I’ve decided to do my own by implementing the basic lambda calculus interpreter.

Numbers

In the video, a basic system was used to define numbers with succession (just like in in lambda calculus, if we use Church numerals). We say that a number can have a “previous,” except zero.

1type Num = {
2  prev?: Num;
3};
4
5type Zero = Num & {
6  prev: undefined;
7};

These are actual “types.” This means that they are their own things, just like booleans or normal number types in TS/JS, they don’t need parameters, as we shall see.

Functions

If we’re only using types, we can’t really define functions or use them. To get ahead of this problem, we use type parameters as function arguments. For example, the Next and Prev functions could be defined as such:

1type Next<N extends Num> = Num & {
2  prev: N;
3};
4
5type NonZero = Num & {
6  prev: Num;
7};
8
9type Prev<N extends NonZero> = N["prev"];

Here, we defined NonZero as a helper type for us to remove the possibilty of accessing the “previous” of zero. As you can see, numbers are defined as recursive objects.

1type One = Next<Zero>;
2type Two = Next<One>;
3type Three = Next<Two>;
4type Four = Next<Three>;
5type Five = Next<Four>;
6type Six = Next<Five>;
7type Seven = Next<Six>;
8type Eight = Next<Seven>;
9type Nine = Next<Eight>;
10//   ^? Nine = Next<Next<Next<Next<Next<Next<Next<Next<Next<Zero>>>>>>>>>

Operations

Now that we have numbers properly defined and that we know how to define functions, it’s pretty easy to get addition, subtraction, multiplication, and division working. They all can be defined in recursive ways.

1type Add<A extends Num, B extends Num> = A extends Zero
2  ? B
3  : A extends NonZero
4    ? Add<Prev<A>, Next<B>> // remove from one, add to another
5    : B;
6    
7type Sub<A extends Num, B extends Num> = B extends Zero
8  ? A
9  : A extends NonZero
10    ? B extends NonZero
11      ? Sub<Prev<A>, Prev<B>> // remove from both
12      : never
13    : Zero;

Multiplication and addition are a bit more annoying but can still be recursively defined; multiplication with an accumulator and division by separating it into integer division and modular, of which both use addition and subtraction.

Instead of recursive objects, one could’ve also achieved this with a const array of some length symbolising a number or even possibly with a binary tree, but that would be pretty complicated.

Turing Completeness

The video proved that types in TS is turing complete by implementing Fractran with our previous definition of a number, which is fair enough. And in the end, it does look really cool (do check the video out to see it!). However, what’s interesting is that TS can’t handle the highly recursive nature of the specification, so you need to remove the following if statement from the source code of TS.

1if (tailCount === 1e3) {
2  error(currentNode, Diagnostics.Type_instantiation_is_excessively_deep_and_possibly_infinite);
3  return errorType;
4}

Lambda Calculus

Instead of implementing Fractran (or even Brainfuck, which would’ve been really cool too!), I’ve decided to implement a very simple interpreter for lambda calculus. First, I’ve tried the following definitions, but soon realised that it’s not as simple as the above definitions.

1type Lambda<X, M> = (x: X) => M;
2type Lambda = (x: Lambda) => Lambda;
3type Apply<F extends Lambda, N extends Parameters<F>[0]> = ReturnType<F>;

There’s two basic issues:

Even though lambda calculus is only made up of “functions,” it also has applications, or so-called beta reductions. And, you can’t do that only with types as you’re only just “defining” functions, just like in JavaScript, and it is really difficult to define the argumants and return types specifically as well, as TS needs to infer them for us to get a good result.
Even if we had functions working in types, we wouldn’t be able to have currying in place, since that’s a fully JavaScript runtime dependent thing. If you’ve done lambda calculus before, you’ll understand how important currying actually is — it needs memory.

Therefore, instead of relying on TS types, we should define our own with an abstract syntax tree (AST). In lambda calculus, there are variables, lambdas, and we use them both with applications.¹

1type Term = Var<string> | Lam<string, any> | App<any, any>;
2
3type Var<Name extends string> = {
4  readonly kind: "var";
5  readonly name: Name;
6};
7
8type Lam<Name extends string, Body extends Term> = {
9  readonly kind: "lam";
10  readonly name: Name;
11  readonly body: Body;
12};
13
14type App<F extends Term, A extends Term> = {
15  readonly kind: "app";
16  readonly f: F;
17  readonly a: A;
18};

Thus, a Term is a combination of a variable, lambda, or an application, defined recursively. Note that we need to define a kind for these types as otherwise TS would not be able to properly infer what kind of term it is otherwise. We also need to define our closure.

1type Env = Record<string, any>;
2
3type Closure<Name extends string, Body extends Term, E extends Env> = {
4  readonly kind: "closure";
5  readonly name: Name;
6  readonly body: Body;
7  readonly env: E;
8};
9
10type Lookup<E extends Env, Name extends string> = Name extends keyof E
11  ? E[Name]
12  : never;

Here, our environment is just a simple object keyed off of the variable names and lookup is a simple helper for us to get the value using the variable. Now, we define the evaluations. They are separated into three different evaluations:

1type EvalVar<Name extends string, E extends Env> = Lookup<E, Name>;
2
3type EvalLam<Name extends string, Body extends Term, E extends Env> = Closure<
4  Name,
5  Body,
6  E
7>;
8
9type EvalApp<F extends Term, A extends Term, E extends Env> =
10  Eval<F, E> extends Closure<
11    infer Name extends string,
12    infer Body extends Term,
13    infer CEnv extends Env
14  >
15    ? Eval<Body, CEnv & Record<Name, Eval<A, E>>>
16    : never;
17
18type Eval<T extends Term, E extends Env = {}> =
19  T extends Var<infer Name extends string>
20    ? EvalVar<Name, E>
21    : T extends Lam<infer Name extends string, infer Body extends Term>
22      ? EvalLam<Name, Body, E>
23      : T extends App<infer F extends Term, infer A extends Term>
24        ? EvalApp<F, A, E>
25        : never;

And that’s it! This is our entire lambda calculus logic. Let’s use them now!

Some Usage

As we’ve defined in KCPC Workshops, let’s do boolean arithmetic. We define True and False as such:

1type True = Lam<"x", Lam<"y", Var<"x">>>;
2type False = Lam<"x", Lam<"y", Var<"y">>>;

Thus, the and operator is defined, using applications, like (λp.λq.p q p):

1type And = Lam<"p", Lam<"q", App<App<Var<"p">, Var<"q">>, Var<"p">>>>;

And, we can evaluate them with the Eval type:

1type T1 = Eval<App<App<And, True>, True>>;
2//   ^? T1 = Closure<"p", Lam<"q", App<App<Var<"p">, Var<"q">>, Var<"p">>, {}>>

Discussion

As you can see, one thing that my implementation is missing is the simplification into just Lam and Vars, as Eval just outputs a Closure. Things that might be added could be a de Bruijn-index version, a full beta-normaliser, Church numerals (like actual numbers), and arithmetic. Also, of course, a prettifier/simplifier for the resulting types.²

Check out my full implementation at lambda-calculus-typescript.

Footnotes

Subscribe!

Follow Next!

Contents

Numbers
Functions
Operations
Turing Completeness
Lambda Calculus
Some Usage
Discussion
Footnotes