Lambda calculus in the TS type system

Lambda.ts

// Copyright 2021 Simon Meskens
// Licensed under the MIT License
//
// Permission to use, copy, modify, and/or distribute this software for any
// purpose with or without fee is hereby granted, provided this license is
// preserved. This software is offered as-is, without any warranty.

type Test1 = λ<Not, [True]>;        // False
type Test2 = λ<And, [True, False]>; // False
type Test3 = λ<And, [True, True]>;  // True

// Boolean
interface True extends Func { expression: Var<this, 0>; }
interface False extends Func { expression: Var<this, 1>; }
interface Not extends Func { expression: λ<Var<this, 0>, [False, True]> }
interface And extends Func { expression: λ<Var<this, 0>, [Var<this, 1>, Var<this, 0>]> }

// Plumbing
type Func = {
    variables: Func[];
    expression: unknown;
}

type Var<F extends Func, X extends number> = F["variables"][X];

type λ<Exp extends Func, Vars extends unknown[]> = (Exp & {
    variables: Vars;
})["expression"];