Lambda

A simple lambda calculus evaluator. Its just a bunch of functions you define and use as data and pass into other functions. It uses System F for type checking.

What this evaluator can do:

• lambda terms and evaluation (simple normalization)
• define simple types
• polymorphism for lambda terms via forall
• relative importing of other files
• sugaring and desugaring certain typed terms (for example numeric literals)

How to install

git clone https://github.com/lisk77/lambda && cd lambda
mkdir build && cd build
cmake ..
make

How to use

Write your code into a file and pipe it into the binary

cat file | lambda

or just echo the code directly

echo "main = \\ x . x;" | lambda

Syntax

Lambda expression

\ param1: Type param2: Type ... . body

Type abstraction / application (System F)

forall A . term
term [Type]

Type syntax

forall A . Type  
A -> B -> C 
type Alias = Type;

(right associative)

Definitions

identifier = expression;

Imports

import path/to/file;

(relative to the importing file)

Literals / built-ins

• Numeric literals desugar to Church Nat.
• Bool is Church-encoded; see examples/booleans for true/false.

For a file to be able to be run, it needs to define a main function.

Future ideas

• types
• imports (at least simple)
• small standard library