Skip to content

Instantly share code, notes, and snippets.

@tjjfvi
Last active February 17, 2024 21:03
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save tjjfvi/4fe9a244ad6b776a0015cad86b36860b to your computer and use it in GitHub Desktop.
Save tjjfvi/4fe9a244ad6b776a0015cad86b36860b to your computer and use it in GitHub Desktop.
Lambda Calculus in TypeScript Types: https://tsplay.dev/wE5nZw
type _I = Reduce<[S, K, K]>
// ^?
type One = I
type Zero = Reduce<[K, I]>
// ^?
type Add = { a: { b: { i: { z: ["a", "i", ["b", "i", "z"]] } } } }
type Mul = { a: { b: { i: ["a", ["b", "i"]] } } }
type Two = [Add, One, One]
type Three = [Add, Two, One]
type Six = [Add, Three, Two]
type Inc = [Add, One]
type Dec = { n: { i: { z: ["n", { v: { j: ["j", ["v", "i"]] } }, { _: "z" }, { x: "x" }] } } }
type Y = { f: [{ x: ["x", "x"] }, { g: ["f", ["g", "g"]] }] }
type If = { n: ["n", { _: { t: { f: "t" } } }, { t: { f: "f" } }] }
type Factorial = [Y, { f: { x: [If, "x", [Mul, "x", ["f", [Dec, "x"]]], One] } }]
// Church numeral representing 6 (as there are 6 calls to "i").
type a = Reduce<[Mul, Two, Three]>
// ^?
/*
// Errors in playground; works locally, but very slow.
type b = Reduce<[Factorial, Two]>
// ^?
/**/
/*
// Errors in playground; potentially works locally, but extremely slow
// (I haven't ever been patient enough to see it finish)
type c = Reduce<[Factorial, Three]>
// ^?
/**/
/* Implementations */
type Reduce<T> = TailRec.Reduce<T>
// type Reduce<T> = Plain.Reduce<T>
// type Reduce<T> = WithHkt.Reduce<T>
// type Reduce<T> = Combinators.Reduce<T>
// Plain, non-tail-recursive implementation
namespace Plain {
export type Reduce<T> = ToCompact<_Reduce<FromCompact<T>, []>>
type _Reduce<T, C extends unknown[]> =
T extends Lambda<infer I, infer U>
? C extends [infer A, ...infer D]
? _Reduce<_Replace<U, [I, A]>, D>
: Lambda<I, _Reduce<U, []>>
: T extends Call<infer U, infer V>
? _Reduce<U, [V, ...C]>
: _WrapCalls<T, C>
type _WrapCalls<T, C extends unknown[]> =
C extends [infer A, ...infer D]
? _WrapCalls<Call<T, _Reduce<A, []>>, D>
: T
type _Replace<T, R extends [string, unknown]> =
T extends R[0]
? Extract<R, [T, unknown]>[1]
: T extends Lambda<infer I, infer U>
? I extends R[0]
? R[0] extends I
? T
: Lambda<I, _Replace<U, Exclude<R, [I, unknown]>>>
: I extends AllFreeVars<R[1]>
? Lambda<Prime2<I, AllFreeVars<R[1]>>, _Replace<U, [I, Prime2<I, AllFreeVars<R[1]>>] | R>>
: Lambda<I, _Replace<U, R>>
: T extends Call<infer U, infer V>
? Call<_Replace<U, R>, _Replace<V, R>>
: T
}
// Tail-recursive implementation
// This isn't necessarily ideal, as it loses some potential caching of types
// However, this implementation has gotten the farthest before failing due to recursion limits
// Because this procedure is not conducive to usual tail-recursion, this essentially implements a call stack
namespace TailRec {
export type Reduce<T> = ToCompact<Run<FromCompact<T>, [["reduce", []]]>>
type _Run<U, A extends unknown[], B extends unknown[]> = Run<U, [...A, ...B]>
type Extends<T, U extends T> = U
type Run<T, Stack> =
| Stack extends [["reduce", [...infer C]], ...infer Stack]
? T extends Lambda<infer I, infer U>
? C extends [infer A, ...infer C]
? _Run<U, [["replace", [I, A]], ["reduce", C]], Stack>
: _Run<U, [["reduce", C], ["lambda", I]], Stack>
: T extends Call<infer U, infer V>
? _Run<U, [["reduce", [V, ...C]]], Stack>
: _Run<T, { [K in keyof C]: ["call", C[K]] }, Stack>
: Stack extends [["replace", Extends<[string, unknown], infer R>], ...infer Stack]
? T extends R[0]
? _Run<Extract<R, [T, unknown]>[1], [], Stack>
: T extends Lambda<infer I, infer U>
? I extends R[0]
? R[0] extends I
? _Run<T, [], Stack>
: _Run<U, [["replace", Exclude<R, [I, unknown]>], ["lambda", I]], Stack>
: I extends AllFreeVars<R[1]>
? _Run<U, [["replace", R | [I, Prime2<I, AllFreeVars<R[1]>>]], ["lambda", Prime2<I, AllFreeVars<R[1]>>]], Stack>
: _Run<U, [["replace", R], ["lambda", I]], Stack>
: T extends Call<infer U, infer V>
? _Run<U, [["replace", R], ["replace2", R, V]], Stack>
: _Run<T, [], Stack>
: Stack extends [["replace2", infer R, infer U], ...infer Stack]
? _Run<U, [["replace", R], ["pass", T]], Stack>
: Stack extends [["call", infer A], ...infer Stack]
? _Run<A, [["reduce", []], ["pass", T]], Stack>
: Stack extends [["pass", infer A], ...infer Stack]
? _Run<Call<A, T>, [], Stack>
: Stack extends [["lambda", infer I], ...infer Stack]
? _Run<Lambda<I & string, T>, [], Stack>
: T
}
/* Shared utils */
interface Call<F, A> { type: "call", f: F, a: A }
interface Lambda<I extends string, T> { type: "lambda", i: I, t: T }
type Prime<T extends string> = `${T}'`
type Prime2<T extends string, U, N extends 0[] = [0]> = `${T}_${N["length"]}` extends U ? Prime2<T, U, [...N, 0]> : `${T}_${N["length"]}`
// Converts e.g. { a: ["a", "a"] } to Lambda<"a", Call<"a", "a">>
type FromCompact<T> =
T extends string
? T
: T extends Lambda<infer A, infer B>
? Lambda<FromCompact<A>, FromCompact<B>>
: T extends Call<infer A, infer B>
? Call<FromCompact<A>, FromCompact<B>>
: T extends [infer A, infer B, ...infer C]
? FromCompact<[Call<A, B>, ...C]>
: T extends [infer A]
? FromCompact<A>
: Lambda<keyof T & string, FromCompact<T[keyof T]>>
// Converts e.g. Lambda<"a", Call<"a", "a">> to { a: ["a", "a"] }
type ToCompact<T> =
T extends string
? T
: T extends Lambda<infer A, infer B>
? { [_ in A]: ToCompact<B> }
: T extends Call<infer A, infer B>
? ToCompact<A> extends unknown[]
? [...ToCompact<A>, ToCompact<B>]
: [ToCompact<A>, ToCompact<B>]
: T
// e.g. Lambda<"a", Call<"a", Call<"b", "c">>> -> "b" | "c"
type AllFreeVars<T, E = never> =
T extends string
? T extends E
? never
: T
: T extends Lambda<infer I, infer U>
? AllFreeVars<U, E | I>
: T extends Call<infer U, infer V>
? AllFreeVars<U | V, E>
: never
// Uses HKTs to represent lambdas
// Doesn't seem to work for recursive things
namespace WithHkt {
interface _TransformBreak<T> { type: "transformBreak", value: T }
interface _Lambda<I extends string, T> {
type: "_lambda",
input: unknown,
output: Value<_FromData<_Replace<T, I, _TransformBreak<this["input"]>>>>
}
interface Value<T> {
value: T
}
export type Reduce<T> = ToCompact<_ToData<_FromData<FromCompact<T>>>>
type _Call<T, U> =
T extends string
? Call<T, U>
: T extends Value<infer V>
? _Call<V, U>
: (T & { input: U })["output" & keyof T]
type _ToData<T, X extends string = "x"> =
T extends { type: "_lambda" }
? Lambda<X, _ToData<_Call<T, X>, Prime<X>>>
: T extends Call<infer A, infer B>
? Call<_ToData<A, X>, _ToData<B, X>>
: T extends Value<infer V>
? _ToData<V, X>
: T
type _FromData<T> =
T extends _TransformBreak<infer U>
? U
: T extends Lambda<infer I, infer T>
? _Lambda<I, T>
: T extends Call<infer T, infer U>
? _Call<_FromData<T>, _FromData<U>>
: T
type _Replace<T, A extends string, B> =
T extends A
? B
: T extends Lambda<infer I, infer U>
? I extends A
? T
: I extends AllFreeVars<B>
? _Replace<Lambda<Prime<I>, _Replace<U, I, Prime<I>>>, A, B>
: Lambda<I, _Replace<U, A, B>>
: T extends Call<infer U, infer V>
? Call<_Replace<U, A, B>, _Replace<V, A, B>>
: T
}
// Converts the lambda expression to the SKI basis, reduces that, and then
// converts it to a lambda expression, avoiding the need for alpha-reduction
namespace Combinators {
type _ToCombinators<T> =
T extends Call<infer A, infer B>
? Call<_ToCombinators<A>, _ToCombinators<B>>
: T extends Lambda<infer A, infer U>
? A extends AllFreeVars<U>
? U extends A
? I
: U extends Lambda<infer B, infer V>
? _ToCombinators<Lambda<A, _ToCombinators<U>>>
: U extends Call<infer X, infer Y>
? Call<Call<S, _ToCombinators<Lambda<A, X>>>, _ToCombinators<Lambda<A, Y>>>
: never
: Call<K, _ToCombinators<U>>
: T
type _ReduceCombinators<T, C extends unknown[] = [], N extends string = "x"> =
T extends [infer A, ...infer B]
? _ReduceCombinators<A, [...B, ...C], N>
: T extends S | K | I
? [T, C] extends [S, [infer X, infer Y, infer Z, ...infer D]]
? _ReduceCombinators<X, [Z, [Y, Z], ...D], N>
: [T, C] extends [K, [infer X, infer Y, ...infer D]]
? _ReduceCombinators<X, D, N>
: [T, C] extends [I, [infer X, ...infer D]]
? _ReduceCombinators<X, D, N>
: { [_ in N]: _ReduceCombinators<T, [...C, N], Prime<N>> }
: C extends []
? T
: [T, ...{ [K in keyof C]: _ReduceCombinators<C[K]> }]
export type Reduce<T> = _ReduceCombinators<ToCompact<_ToCombinators<FromCompact<T>>>>
}
// Combinators
interface S { a: { b: { c: ["a", "c", ["b", "c"]] } } }
interface K { a: { b: "a" } }
interface I { a: "a" }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment