Emulating the Lambda Calculus in TypeScript's Type System

• Lambda calculus syntax
• $\beta$-reduction
• Free variables
• $\alpha$-conversion
• Substitution
  • Contexts
• Evaluation: $\beta$ normal form
• Extension: Program Equivalence
  • $\alpha$-equivalence
  • Type-level numbers
  • $\alpha\beta$-equivalence
  • Proving arithmetic equivalences
• Notes

It's been half year since I last wrote about exploiting the TypeScript type system to solve non-trivial problems. Those problems were relatively simple as far as computational complexity goes - we weren't trying to do everything a Turing machine can do.

This time, we'll solve the computationally-harder problem of emulating the lambda calculus. The (untyped) lambda calculus is a model of computation equivalent to the Turing machine model, which means that the lambda calculus can compute anything a Turing machine canThe typed lambda calculus, which only admits terms that are "well-typed", is not computationally equivalent to the Turing machine. It turns out that all well-typed terms in the typed lambda calculus halt. But there are programs for which a Turing machine does not halt.. In other words, the lambda calculus can simulate any computer algorithm. So, if we can emulate the lambda calculus in the TypeScript type system, we will have a proof that the type system is Turing-completeIt has been well-known for several years that TypeScript's type system is Turing-complete. However, I am not aware of any prior implementations of the lambda calculus in the type system. Perhaps this because it is straightforward (as we will see), or Turing machine emulators are more appealing as proofs.! Furthermore, our construction will not be esoteric; in fact, it will read similarly to typical functional implementations of the lambda calculus.

The lambda calculus is one of the most well-studied topics in computer science, fundamental in computational theory. Almost all functional languages, type systems, and type-based theorem provers are built on an extension of the lambda calculus with types, known as the simply typed lambda calculus. The simply typed lambda calculus is part of a beautiful trilogy known as the Curry-Howard-Lambek correspondence that says that computation in the model of typed lambda calculi, mathematical logic, and category theory are equivalent.

I mention these consequences not because they're particularly important to know, but to say that applications of the lambda calculus across mathematics and computer science are well known. Our construction of the lambda calculus will not be anything new, so if you are already familiar with it, perhaps only the type-level implementation in TypeScript will be interesting. Nevertheless, I will not assume existing knowledge of the lambda calculus. I will, however, assume familiarity with TypeScript's syntax and type system. For a refresher of the latter and an introduction to computation with the TS type system, see my last post on this topic.

Lambda calculus syntax

The untyped lambda calculus is a language consisting of three forms:

An abstraction $(\lam x. {\tt e})$ binds the variable $x$ in the $expr$ ${\tt e}$; that is, it's a one-parameter function. We can't do anything with an abstraction until we have something to apply to it, which is what the application form does. As a consequence of the untyped calculus, the left ${\tt e}$ in the application form can be an arbitrary $expr$, not necessarily an abstraction.

A program in the untyped lambda calculus is just an expression composed from these three forms. Here's one:

"Intuitively", we might reduce this as

but there's one other reduction procedure to $z$ (what is it?). This reduction process is exactly evaluation of the lambda calculus. Sequences of reductions are also called normalization, for reasons that will be made apparent later.

This program doesn't communicate anything useful, but as we mentioned before, the lambda calculus is equivalent to a Turing machine! It's crazy to imagine, but it might suggest we have our work set out for us if we want to implement it in the TypeScript type system.

We'll start off with something easy and fun: the syntax, a pretty-printer, and parser. First, the basic definitions:

ts
type Expr = Var<string>|Abs<string, any>|App<any, any>;
type Var<X extends string> = {x: X};
type Abs<S extends string, B extends Expr> = {s: S, b: B};
type App<E1 extends Expr, E2 extends Expr> = {e1: E1, e2: E2};

Notice the use of any in the definition of Expr. Writing Expr in place of any would cause Expr to be a self-referential type, which TypeScript no longer permits. Fortunately, the use of any here does not detriment our implementation.

Since TypeScript added template literal string types, we can provide a type-level pretty-printer for expressions:

ts
type StringOfExpr<T extends Expr>
    = T extends Var<string> ? `${T['x']}`
    : T extends Abs<string, any> ?
        StringOfExpr<T['b']> extends infer B ? B extends string ?
        `(λ${T['s']}. ${B})` : never : never
    : T extends App<any, any> ?
        StringOfExpr<T['e1']> extends infer E1 ? E1 extends string ?
        StringOfExpr<T['e2']> extends infer E2 ? E2 extends string ?
        `(${E1} ${E2})` : never : never : never : never
    : never;

We will see patterns of the form StringOfExpr<T['b']> extends infer B ? B extends string, as above, often in our implementation. This unravelling of an type to an intermediate inference variable B aids the typechecker by instructing it to solve for one unconstrained variable at a time. Without this guidance, the type instantiation space may balloon exponentially, causing the checker to give up. Usually this ballooning isn't too bad, but StringOfExpr is a pretty complex type, so nested references can grow quite large.

Template literal types can be pattern-matched by the typechecker, so we can also provide a type-level parser for lambda calculus expressions.

ts
type ParseVar<T> = T extends `${infer X}` ? Var<X> : never;
type ParseAbs<T> = T extends `(λ${infer S}. ${infer B})` ? Abs<S, ParseExpr<B>> : never;
type ParseApp<T> = T extends `(${infer E1} ${infer E2})` ? App<ParseExpr<E1>, ParseExpr<E2>> : never;
type ParseExpr<T> =
    ParseAbs<T> extends never
    ? ( ParseApp<T> extends never
        ? ( ParseVar<T> extends never
            ? never
            : ParseVar<T> )
        : ParseApp<T> )
    : ParseAbs<T>;

Since our parser is top-down and pattern-based, it is even weaker than a regex-based parser. Indeed, it fails to properly parse nested applications or abstractions on the left. For example,

ts
type BadParse = ParseExpr<"((λx. x) y)">;
        
type BadParse = {
    e1: Var<"(λx.">;
    e2: Var<"x) y">;
}

But this is not a post about parsing. We'll live with this solution, and write out expressions in the internal syntax when parsing does a bad job.

$\beta$-reduction

The only place where something can get evaluated in an expression is at an application to an abstraction. The process of evaluating of an abstraction body with an applied argument is called $\beta$-reduction. Explicitly, $\beta$-reduction is the rule

where the substitution $[a/x]b$ replaces free occurrences of the variable $x$ in $b$ with $a$. Expressions to which reductions can be applied are called redexes (reducible expressions); in particular, expressions to which $\beta$-reductions can be applied are called $\beta$-redexes.

Performing substitution is a bit tricky, so before we give a type-level algorithm to do so, we should talk about some subtle cases.

Free variables

What do we mean by free occurrences of a variable? Consider $((\lam x. (x\ (\lam x. x)))\ (y\ z))$. If we were to perform the substitution $[(y\ z)/x]\hspace{0pt}(x\ (\lam x. x))$ by replacing all occurrences of $x$ we wouldn't even get a syntactically-valid expression! If we replaced all variables named $x$ we would get $((y\ z)\ (\lam x. (y\ z)))$, which is incorrect because the innermost abstraction is no longer the identity function. Rather, we only want to replace the first variable $x$, as it is free of binding by any enclosing abstraction. The second variable $x$ is bound to an enclosing abstraction, so we should not touch it during substitution. Distinguishing between free and bound variables this way, we see that the correct reduction is $((y\ z)\ (\lam x. x))$.

Discovery of free variables in an expression will be important in for our evaluator. We can construct a recursive predicate Free that collects all variables into a union of literals by traversing a type bottom-up. The only variables we need to exclude from this collection are those bound by an abstraction.

ts
type Free<T extends Expr>
    = T extends Var<infer X> ? X
    : T extends Abs<infer S, infer B> ? Exclude<Free<B>, S>
    : T extends App<infer E1, infer E2> ? Free<E1>|Free<E2> : never;
type FreeTest1 = Free<ParseExpr<"(x z)">>;
        
type FreeTest1 = "x" | "z"
type FreeTest2 = Free<ParseExpr<"(λy. (x (y z)))">>;
        
type FreeTest2 = "x" | "z"

$\alpha$-conversion

There's another tricky case in substitution. Consider $[x/y]\hspace{0pt}(\lam x. y)$. This time, a literal replacement yields the identity function $(\lam x. x)$ rather than a constant function to $x$ in the outer scope. If only the bound $x$ had been named something else, say $x'$, we would end up with the constant function $(\lam x'. x)$ we expect.

Indeed, there is no reason we can't arbitrarily rename bound variables in such cases. For example, $(\lam x. (\lam y. (x\ y)))$ and $(\lam x. (\lam z. (x\ z)))$ differ in the name of their second bound variables, but are computationally equivalent. Renaming bound variables to computationally equivalent expressions is called $\alpha$-conversion. We say that two expressions are $\alpha$-equivalent if they are syntactically equivalent, up to $\alpha$-conversion. You may be familiar with $\alpha$-conversion and $\alpha$-equivalence if you've ever renamed a variable in a codebase; hopefully it didn't cause a failure!

We'll return to $\alpha$-equivalence later on when talking about program equivalence. Regarding our present issue, it is enough to stipulate that when we have a $\beta$-redex $((\lambda x. b)\ a)$ where $x\in\text{Free}(a)$, we should choose a fresh variable name for $x$ and perform $\alpha$-conversion on the abstraction before proceeding. The only requirement is that we choose a variable name that is not already free in $a$ or $b$, otherwise we end up with the same problem again (in the former case) or accidentally binding a free variable (in the latter case). The popular strategy is to tack on single quotes until these requirements are met.

Here's a type constructor to find a fresh variable name given a collection (union) of reserved names.

ts
type Freshen<X extends string, Used> = X extends Used ? Freshen<`${X}'`, Used> : X;
const freshen_test1: Freshen<"x", "x"|"y"|"x'"> = `x''`;

Substitution

We now use our notes from the two sections above to come up with a proper algorithm for the right hand side of $\beta$-reduction, via a type constructor Subst<X, A, E> that performs the substitution [A/X]E.

In the interest of a performant type-level algorithm that the typechecker will be willing to compute, we make some adjustments to the high-level ideas previously discussed.

Rather than explicitly performing alpha conversion on an abstraction body every time its binder (say $x$) interferes with a free variable in the replacement expression, we generate a fresh binder name (say $x'$) and store the mapping $x\to x'$ in a "substitution context" we pass on to substitution of the abstraction body. Then, whenever we see a variable, if it is in the substitution context (either because it is the original substitution target, or needs to undergo $\alpha$-conversion), we replace it with its mapping. Otherwise, the variable is untouched. This implicit $\alpha$-conversion as we go requires only one pass of the expression, whereas explicit $\alpha$-conversion everytime it is needed would result in a quadratic substitution algorithm.

To avoid having to compute the free variables of the expression we wish to substitute everytime we need to check a binder for $\alpha$-conversion, we compute the collection of free variables once and pass it down to nested expressions as neededAt an abstraction, why don't we need to check if the binder is free in the right-hand mappings of all variables in our context? Hint: Recall that other than the substitution $[X\to A]$, there is only one other kind of mapping in the context..

ts
type Subst<X extends string, A extends Expr, E extends Expr>
    = Subst_<X, E, [[X, A]], Free<A>>;
type Subst_<X extends string, E extends Expr, Subs extends Ctx<Expr>, FreeInA>
    = E extends Var<infer U> ?
        (Find<Expr, U, Subs> extends infer R ? R extends Expr ? R : E : never)
    : E extends App<infer E1, infer E2> ?
        Subst_<X, E1, Subs, FreeInA> extends infer E11 ? E11 extends Expr ?
        Subst_<X, E2, Subs, FreeInA> extends infer E21 ? E21 extends Expr ?
        App<E11, E21> : never : never : never : never
    : E extends Abs<infer S, infer B> ? (
        // Case 1: S = X, shadowing X, so no need to substitute at all.
        S extends X ? E :
        // Case 2: S \in Free(A), so naively substituting A in the body will
        // change what S in A refers to. For example, [x->s](λs. x) => λs. s,
        // which is incorrect. Instead, come up with a fresh name S->S1.
        S extends FreeInA ?
            (FreeInA|Free<B> extends infer FreeXB ?
            Freshen<S, FreeXB> extends infer S1 ? S1 extends string ?
            Subst_<X, B, [[S, Var<S1>], ...Subs], FreeInA> extends infer B1 ? B1 extends Expr ?
            Abs<S1, B1> : never : never : never : never : never) :
        // Case 3: A doesn't conflict with the introduced binder S, so direct
        // substitution is fine.
        Subst_<X, B, Subs, FreeInA> extends infer B1 ?
            B1 extends Expr ? Abs<S, B1> : never : never
    )
    : never

Let's write some tests to check our work.

ts
type SubstTest<X extends string, E extends string, B extends string> =
    Subst<X, ParseExpr<E>, ParseExpr<B>> extends infer R ? R extends Expr ?
    StringOfExpr<R> : never : never;
const subst_test1: SubstTest<"x", "y", "(λz. x)"> = "(λz. y)";
const subst_test2: SubstTest<"x", "y", "(λy. x)"> = "(λy'. y)";
const subst_test3: SubstTest<"x", "y", "(λx. x)"> = "(λx. x)";

Contexts

Hopefully, the completist side of you is nagging at this Ctx type constructor - we mentioned contexts, but how exactly are they implemented? And how does Find work?

As case 2 of substitution in abstractions hints, we implement contexts as associative lists backed by type tuples. If you know associative lists from OCaml or Lisp, this should be familiar. Each element of the type tuple is a "mapping" represented by a two-element tuple. For our purposes contexts only need to map from strings to something else, so we parameterize Ctxs by only the value type.

ts
type Ctx<T> = [string, T][];

Find is pretty straightforward, finding the first mapping from the front of the context. This is why we add new mappings to the front of a context. Since we can't throw type-level errors, we report failures to find a mapping for a key with a special NotFound type.

ts
type NotFound = {__brand: 'Not found'}
type Find<T, X extends string, L extends Ctx<T>> =
    L extends [[infer Y, infer N], ...infer B] ?
    (Y extends X ? N : B extends Ctx<T> ? Find<T, X, B> : never)
    : NotFound;
    
const find_test: Find<number, "a", [["b", 10], ["a", 7], ["c", 15]]> = 7;

Evaluation: $\beta$ normal form

As we've seen, $\beta$-reduction is the only meaningful computation to make in an expression. This leads naturally to a notion of the $\beta$ normal form of an expression, in which there no $\beta$-reductions are possible anywhere in the term - not in either side of applications, nor inside abstractionsThere are weaker notions of normal form, for example an expression is in weak head normal form (whnf) if there are no $\beta$-reductions possible in the head position (i.e. top-level applications), but there may be $\beta$-reductions possible inside arguments to applications or in the bodies of abstractions. Whnf is the reduction strategy of Haskell's evaluation semantics; this is part of what is necessary for lazy evaluation and sharing of computational results..

Let's look at some examples.

• As we saw before, the expression $((\lam x. x)\ ((\lam y. y)\ z))$ has a $\beta$-redex in head position. If we apply this reduction we get $((\lam y. y)\ z)$, which has another $\beta$-redex in head position. After we apply it, we get $z$, which has no further $\beta$-reduction, and so $z$ is the $\beta$ normal form of these expressions.
• The expression $(x\ ((\lam y. y)\ z))$ does not have a $\beta$-redex in head position, but there is one in the argument to the top-level application. We apply the reduction to get $(x\ z)$, which is in $\beta$ normal form.
• The expression $(\lam x. ((\lam y. y)\ z))$ has no $\beta$-redex in head or argument position, but there is one inside the top-level abstraction. Applying the reduction yields $(\lam x. z)$, which is in $\beta$ normal form.

An important decision to make is what order we should apply $\beta$-reductions in. As we mentioned when first introducing the $\beta$-reduction, $((\lam x. x)\ ((\lam y. y)\ z))$ has multiple normalization sequences - either by applying the reduction in head position first, or the one in argument position first. Either way we go we, normalization to $\beta$ normal form ends up at the expression $z$. Unfortunately, in general we may not be so lucky. One example (taken from Wikipedia) is

If we try to apply the $\beta$-redex in argument position first, we step to the expression

with a larger redex in argument position. Indeed, if we keep trying to reduce in argument position, our normalization sequence will never halt. But there is a $\beta$ normal form for this expression - if only we had reduced the $\beta$-redex in head position first, we would wind up with just $z$, since $x$ is never referenced in the left-hand abstraction body.

It turns out that applying $\beta$-reductions in the leftmost, outermost position before considering arguments to the right or abstraction bodies one level down is the "best" normalization strategy in the sense that if a $\beta$ normal form for an expression exists, this strategy always finds it. This evaluation strategy is appropriately named normal order; the seminal result is known as the Standardization Theorem, proven by Curry and Feys in 1958.

With a strategy in our hands, we can now describe an algorithm for evaluating to $\beta$ normal form explicitly. Given an expression, we first check if the top-level is a $\beta$-redex. If it is, we perform the $\beta$-reduction and compute the $\beta$ normal form of the resulting expression. Otherwise, the top-level expression must be a variable, an abstraction, or an application with a non-abstraction on the left-hand side, or an abstraction. In the first case there is nothing more to do. In the second case, we compute the $\beta$ normal form of the abstraction body and re-package the abstraction. In the third case, we compute the $\beta$ normal form of the application argument and re-package the application.

ts
type BetaNF<E extends Expr>
    = E extends App<infer F, infer A> ?
        (BetaNF<F> extends infer F ? F extends Expr ?
            (F extends Abs<infer S, infer B>
            ? (Subst<S, A, B> extends infer B1 ? B1 extends Expr ? BetaNF<B1> : never : never)
            : BetaNF<A> extends infer A1 ? A1 extends Expr ? App<F, A1> : never : never) : never : never)
    : E extends Abs<infer S, infer B> ?
        BetaNF<B> extends infer B1 ? B1 extends Expr ? Abs<S, B1> : never : never
    : E;

As always, we write some tests to check our implementation:

ts
type BetaNFTest<E extends Expr> =
    BetaNF<E> extends infer PE ? PE extends Expr ?  StringOfExpr<PE> extends infer R ? R extends string ?
    StringOfExpr<E> extends infer E ? E extends string ?
    `${E} => ${R}` : never : never : never : never : never : never;
const nf_test1: BetaNFTest<ParseExpr<"(x y)">>
    = "(x y) => (x y)";
const nf_test2: BetaNFTest<App<Var<"x">, App<Abs<"y", Var<"y">>, Var<"z">>>>
    = "(x ((λy. y) z)) => (x z)";
const nf_test3: BetaNFTest<Abs<"x", App<Abs<"y", Var<"y">>, Var<"z">>>>
    = "(λx. ((λy. y) z)) => (λx. z)";
const nf_test4: BetaNFTest<App<Abs<"x", Var<"z">>, App<Abs<"w", App<App<Var<"w">, Var<"w">>, Var<"w">>>,
                                                   Abs<"w", App<App<Var<"w">, Var<"w">>, Var<"w">>>>>>
    = "((λx. z) ((λw. ((w w) w)) (λw. ((w w) w)))) => z";

That's it! We now have a type-level evaluator for the lambda calculus to $\beta$ normal form. This is enough to show that TypeScript's type system is Turing-complete.

Extension: Program Equivalence

One way of viewing an evaluator to $\beta$ normal form is as a checker of equivalence between expressions, up to $\beta$-reduction. In general, evaluators of programs in any language never introduce anything "new"; they simply yield equivalent, (hopefully) simpler forms of their inputs under some set of evaluation rules.

This is one reason normal forms need to be described formally and evaluation strategies need to be chosen carefully. After all, $((\lam x. z)\ ((\lam w. (w\ w)\ w)\ (\lam w. (w\ w)\ w)))$ and $((\lam y. z) a)$ reduce to the same $\beta$ normal form if we use a normal order evaluation strategy, but are certainly not equivalent if we apply $\beta$-reductions in argument position first!

As a more familiar example, the TypeScript functions

ts
function strip_impl1(what: string) {
  return function(from: string) {
    return from.split(what).join('');
  }
}
 
function strip_impl2(what: string) {
  return function(target: string) {
    while (target.indexOf(what) >= 0) {
      target = target.replace(what, '');
    }
    return target;
  }
}

are equivalent for all string inputs what, up to $\alpha$-conversion of their returned closure parameters and reduction of the expressions in the closure bodies. But if we don't reduce the closure bodies, it is very hard to prove that they produce the same output for all inputs without enumerating and reducing all string inputs, an impossible task.

It is for this reason we chose to evaluate to $\beta$-normal form, which looks inside abstraction bodies and unapplied arguments. Furthermore, our normal order evaluation strategy for the lambda calculus yields a normal form whenever one exists, so two expressions are always comparable whenever there is some route for their termination.

Can we be confident that two lambda calculus expressions are equivalent when their $\beta$-normal forms are equal? Only if by equality we mean equivalence up to $\alpha$-conversion! After all, we don't want to say two programs are semantically different just because we changed a variable name. Since we already have a $\beta$-normal form evaluator, we just need to complete an algorithm for calculating $\alpha$-equivalence, as promised earlier.

$\alpha$-equivalence

Since $\alpha$-equivalence measures syntactic equality of two terms up to the renaming of bound variables, we only have to concern ourselves with some way of normalizing bound variables at abstraction sites. The typical approach, which we will employ, is to recurse on the structure of expressions being compared in parallel. If the structures differ (for example a variable vs an application), the expressions cannot possibly be $\alpha$-equivalent. Otherwise, there are three remaining cases of parallel forms.

For applications, we simply check $\alpha$-equivalence of corresponding subexpressions.

For abstractions, we normalize introduced bound variables in each expression by creating a fresh id and mapping each bound variable to that id in a context carried alongside each respective expression. The fresh id we create can be of any form; in our implementation, we use type-level integers.

When comparing two variables, we check if both have mappings to some id in their respective contexts. If they do, and the mapped ids are equal, then the variables are equivalent up to $\alpha$-conversion of some enclosing abstraction. If neither variable has a mapping in its respective context, then both variables are free in all enclosing abstractions; for them to be $\alpha$-equivalent, they must have the same name. Otherwise, one variable is free and the other is bound in some enclosing abstraction, so they cannot be $\alpha$-equivalent.

ts
type AlphaEq<E1 extends Expr, E2 extends Expr,
            L1 extends Ctx<number> = [], L2 extends Ctx<number> = [], Fr extends number = 0>
    = E1 extends Var<infer X1> ? (E2 extends Var<infer X2>
        ? (Find<number, X1, L1> extends number
            ? (Find<number, X2, L2> extends number
                ? Find<number, X1, L1> extends Find<number, X2, L2> ? true : false
                : false)
            : (Find<number, X2, L2> extends number
                ? false
                : X1 extends X2 ? true : false))
        : false)
    : E1 extends App<infer E11, infer E12> ? (E2 extends App<infer E21, infer E22> ?
        AlphaEq<E11, E21, L1, L2, Fr> extends true ?
        AlphaEq<E12, E22, L1, L2, Fr> extends true ?
        true : false : false : false)
    : E1 extends Abs<infer S1, infer B1> ? (E2 extends Abs<infer S2, infer B2> ?
        Incr<Fr> extends infer Fr1 ?
        Fr1 extends number ?
        AlphaEq<B1, B2, [[S1, Fr1], ...L1], [[S2, Fr1], ...L2], Fr1> : never : never : false)
    : never

Here are some tests:

ts
type AlphaEqTest<E1 extends string, E2 extends string> = AlphaEq<ParseExpr<E1>, ParseExpr<E2>>;
const alpha_eq_test1: AlphaEqTest<"(λx. x)", "(λy. y)"> = true;
const alpha_eq_test2: AlphaEqTest<"(λx. z)", "(λy. z)"> = true;
const alpha_eq_test3: AlphaEqTest<"(λz. (λx. (z x)))", "(λx. (λw. (x w)))"> = true;
const alpha_eq_test4: AlphaEqTest<"(y (λx. (λz. (z x))))", "(y (λx. (λw. (w x))))"> = true;
const alpha_eq_test5: AlphaEqTest<"(u (λx. (λz. (z x))))", "(y (λx. (λw. (w x))))"> = false;

Type-level numbers

Our implementation of type-level numbers is backed by tuples for arithmetic. To perform addition, we deserialize a number type n to an n-length tuple type, add m entries to the tuple type, and serialize it back to an n+m number type.

ts
type TupToNum<T extends unknown[]> = T extends {length: infer N} ? N : never;
type NumToTup<N extends number, Tup extends unknown[] = []> =
    Tup extends {length: N} ? Tup : NumToTup<N, [...Tup, unknown]>;
 
type Incr<N extends number> = TupToNum<[...NumToTup<N>, unknown]>;
const incr_test: Incr<11> = 12;

$\alpha\beta$-equivalence

With implementations of evaluation to $\beta$ normal form and $\alpha$-equivalence in place, checking for program equivalence under $\beta$-reduction and $\alpha$-conversion is trivial. Since $\alpha$-conversion cannot introduce new $\beta$-redexes, comparing two expressions consists of normalization followed by a check for $\alpha$-equivalence.

ts
type ABEq<E1 extends Expr, E2 extends Expr> =
    BetaNF<E1> extends infer E1 ? E1 extends Expr ?
    BetaNF<E2> extends infer E2 ? E2 extends Expr ?
    AlphaEq<E1, E2> : never : never : never : never;

Proving arithmetic equivalences

As a comprehensive application of all we've built up, let's show off what all introductions to the lambda calculus show off - simple arithmetic.

There's no syntax for the natural numbers in the lambda calculus language we've worked on, but there is a classic encoding of the naturals known as the Church numerals. Wikipedia gives a very good overview of the encoding and its presentation of various arithmetic operations.

In short, the idea is to encode the Peano axioms for natural numbers as abstractions. The Peano axioms define a symbol $0$ and a 1-parameter function $\S$ called the successor. We take as axioms that $0$ is a natural number, and that if $n$ is a natural number, $\S(n)$ is a natural numberThere are many other axioms, but they are not relevant here.. We can interpret $\S(0)$ as $1$, $\S(\S(\S(0)))$ as 3, and so on.

The church encoding represents the $n$th natural number as a second-order abstraction that takes a "successor function" and a "zero element" and yields an $n$-ary composition of the successor applied to the zero element, as in the Peano axioms. Taking $s$ to bind the "successor function" and $z$ to bind the "zero element", we can represent the first few natural numbers as follows.

It's important to note that, for example, $2$ is represented by the abstraction $(\lam s. (\lam z. (s\ (s\ z))))$, not by its application to some yet-unknown successor and zero arguments. Said another way, the $s$ and $z$ arguments here are only in name, axiomatized into existence.

However, applications to these numerals do come into play when we want to perform arithmetic operations, like addition. Take the church encoding of $m + n$, which is

If we apply a "reverse $\beta$-reduction", known as a $\beta$-abstraction, we can rewrite the above expression to the equivalent form

Now, we parameterize this expression on church numerals $m$ and $n$, where $m\sim(\lam s. (\lam z. (\underbrace{s\ (\ldots\ (s}_{m}\ (z))))))$. This yields an equation for the addition of $m$ and $n$.

Our evaluator can prove the equality of certain expressions under addition, if we take $\alpha\beta$-equivalence as equality. Below we demonstrate this for the proposed equivalence $1 + 1 \overset{\mbox{$\alpha\beta$}}{\equiv} 2$.

ts
type ABEqTest<E1 extends Expr, E2 extends Expr> =
    StringOfExpr<E1> extends infer SE1 ? SE1 extends string ?
    StringOfExpr<E2> extends infer SE2 ? SE2 extends string ?
    ABEq<E1, E2> extends true ?
    `${SE1} ≡ ${SE2}` : `${SE1} ≢ ${SE2}` : never : never : never : never;
type Zero = ParseExpr<"(λs. (λz. z))">;
type One = ParseExpr<"(λs. (λz. (s z)))">;
type Two = ParseExpr<"(λs. (λz. (s (s z))))">;
type Add = Abs<"m", Abs<"n", Abs<"s", Abs<"z",
                App<ParseExpr<"(m s)">, App<ParseExpr<"(n s)">, Var<"z">>>>>>>;
const abeq_test1: ABEqTest<App<App<Add, One>, One>, Two>
    = "(((λm. (λn. (λs. (λz. ((m s) ((n s) z)))))) (λs. (λz. (s z)))) (λs. (λz. (s z)))) ≡ (λs. (λz. (s (s z))))";

With the notion of program equivalence and this example, we can start to see glimmers of the Curry-Howard correspondenceBut whatever correspondence we might interpret here is really just a glimmer; we cannot get very far until we add types on top of the lambda calculus. Dependent type theories in particular provide a correspondence to all sorts of things in classical and intuitionist logic. With a bit of knowledge about Cartesian closed categories and adjunctions, we get even farther, to the trilogy we mentioned in the introduction.. Also, Peano arithmetic is Turing-complete, so if we wanted to, we could provide yet another proof that TypeScript's type system is Turing-complete by modeling the rest of Peano arithmetic in the lambda calculus (which is doable, if not tedious).

Notes

The trickiest and "ugliest" part of our evaluator is the procedure of substitution and $\alpha$-conversion. Indeed, it feels a bit unpleasant to have to deal with collisions between variable names, which are a syntactic concern, when performing substitution, which is a semantic concern. By using a nameless representation of bound variables, like de Bruijn indices, we trade off the inconveniences of $\alpha$-conversion for the semantically-more-appealing operation of "shifting" variable indices to account for changes in enclosing abstractions. de Bruijn indices are a bit tricky to internalize so we didn't use them here. For a good introduction on de Bruijn indices and various typed extensions of the lambda calculus see Pierce's classic Types and Programming Languages.

Besides $\alpha$ and $\beta$ reductions, there is a third common, fundamental operation in the lambda calculus known as $\eta$-equivalence. $\eta$-equivalence says that for all $f$, $(\lambda x. (f\ x)) \equiv f$. This leads to the rewrite rule $(\lambda x. (f\ x)) \Ra f$, known as $\eta$-reduction, and to the reverse rule $f \Ra (\lambda x. (f\ x))$, known as $\eta$-abstraction. $\eta$-reduction is useful for cleaning up code with lots of "unnecessary" abstractions and converting lazy (thunked) code into eagerly-evaluated code. Conversely, $\eta$-abstraction makes eager evaluation lazy. Importantly, $\eta$-equivalence communicates the extensional equivalence of functions, specifying that two functions are equivalent (more strictly, equal) iff they yield equivalent (more strictly, equal) outputs for all inputs. This equivalence is sometimes used for optimizations in compilers of functional languages. An expression is said to be in $\beta\eta$ normal form when no $\beta$ or $\eta$ reductions are possible. We did not explore $\eta$-reductions here because it does not impact our notion of program equivalence (why?).

Lastly, an unpleasant implementation detail is our constant unwrapping of recursive type constructors in the pattern of Rec<T> extends Infer1 ? Infer1 extends Target. As mentioned before, this verbose expansion is needed to help guide the typechecker in computing type instantiation efficiently. I could not find any way to get around this pattern except in a few places. If you find a better implementation, please let me know.