ts-lambda-calc

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!

Examples

Intro

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> // y

Arithmetics

The 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)))))))

Factorial and limitations

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.

License

MIT