Lambda calculus at type-level with TypeScript.
The project includes:
- a parser which transforms raw strings representing lambda expressions into an ASTs
- an evaluator which reduces ASTs
- a stringifyier which transforms an AST back into a string
Try it out in the TypeScript Playground!
When parsing the string (λx.x) y,
- the parser produces
App<Func<Var<"x">, "x">, Var<"y">> - the evaluator derives
Var<"y"> - the stringifier produces
y:
import { Parse } from "./Parser"
import { Eval, Stringify } from "./Semantics"
type raw = `(λx.x) y`
type parsed = Parse<raw> // App<Func<Var<"x">, "x">, Var<"y">>
type evaluated = Eval<parsed> // Var<"y">
type stringified = Stringify<evaluated> // yThe following example shows simple arithmetic operations with Church Encoding:
type ZERO = "(λf.(λx.x))"
type SUCC = "(λa.(λf.(λx.(a f) (f x))))"
type ADD = `(λa.(λb.(b ${SUCC} a)))`
type zero = Parse<ZERO> // Func<Func<Var<"x">, "x">, "f">
type succ = Parse<SUCC> // Func<Func<Func<App<App<Var<"a">, Var<"f">>, App<Var<"f">, Var<"x">>>, "x">, "f">, "a">
type one = Parse<`${SUCC} ${ZERO}`> // App<Func<Func<Func<App<App<Var<"a">, Var<"f">>, App<Var<"f">, Var<"x">>>, "x">, "f">, "a">, Func<Func<Var<"x">, "x">, "f">>
type two = Parse<`${SUCC} (${SUCC} ${ZERO})`> // App<Func<Func<Func<App<App<Var<"a">, Var<"f">>, App<Var<"f">, Var<"x">>>, "x">, "f">, "a">, App<Func<Func<Func<App<App<Var<"a">, Var<"f">>, App<Var<"f">, Var<"x">>>, "x">, "f">, "a">, Func<Func<Var<"x">, "x">, "f">>>
type rawOne = Stringify<one> // ((λa.(λf.(λx.((a f) (f x))))) (λf.(λx.x)))
type rawTwo = Stringify<two> // (
// (λa.(λf.(λx.((a f) (f x)))))
// ((λa.(λf.(λx.((a f) (f x))))) (λf.(λx.x)))
// )
type evalZero = Stringify<Eval<zero>> // (λf.(λx.x))
type evalOne = Stringify<Eval<one>> // (λf.(λx.(f x)))
type evalTwo = Stringify<Eval<two>> // (λf.(λx.(f (f x))))
// 3 + 2 = 5
type parsed = Parse<`${ADD} (${SUCC} (${SUCC} (${SUCC} ${ZERO}))) (${SUCC} (${SUCC} ${ZERO}))`>
type rawParsed = Stringify<parsed> // (((λa.(λb.((b (λa.(λf.(λx.((a f) (f x)))))) a)))
// ((λa.(λf.(λx.((a f) (f x)))))
// ((λa.(λf.(λx.((a f) (f x)))))
// ((λa.(λf.(λx.((a f) (f x)))))
// (λf.(λx.x))))))
// ((λa.(λf.(λx.((a f) (f x)))))
// ((λa.(λf.(λx.((a f) (f x)))))
// (λf.(λx.x)))))
type evaluated = Stringify<Eval<parsed>> // (λf.(λxx.(f (f (f (f (f xx)))))))There is an implementation of factorial in Fact.ts, but unfortunately the compiler has hardcoded type-instantiation depth limits and fails with Type instantiation is excessively deep and possibly infinite.
MIT