mgechev/typed-calc

Interpreter for simply typed lambda calculus implemented in JavaScript λ

Simply Typed Lambda Calculus

A type checker and interpreter for simply typed lambda calculus written in JavaScript.

Example

The following program:

(λ a: Int → a) if (λ a: Int → iszero a) pred 0 then succ 0 else 0

Is correct and evaluates to 0.

How to use?

Interpreter

$ node index.js demo/correct1.lambda

0

Compiler

$ node index.js compile demo/correct1.lambda

(function(a) {
  return a;
})(
  (function(a) {
    return a === 0;
  })(0 - 1)
    ? 0 + 1
    : 0
);

License

MIT

typed-calc's Issues

Transpile lazy evaluation properly

The transpilation to JavaScript of the following construct will fail at the moment.

(λ a: Nat → a)
  (if
    (λ a: Nat → iszero a) pred 0
  then
    (λ a: Nat → succ a)
  else
    (λ a: Nat → pred a))
  0

Termination

Hi,

Does the interpreter has any support to guarantee program termination ? Thanks.

Improve error reporting

Use PegUtil to get column and line of a symbol.