Typed λ-calculus in Rust
This project is both a playground for experimenting with type theory, and a reference for how one can implement a functional programming language compiler in Rust.
PROG ::= FUN* EXP # Program EXP ::= NAME # Variable | LIT # Literal | λ VAR . EXP # Abstraction | EXP EXP # Application | let NAME = EXP in EXP # Let-binding | ( EXP ) # Parenthesized LIT ::= INT # Integer | BOOL # Boolean | STR # String FUN ::= NAME :: ( ∀ NAME* . )? TYPE # Function TYPE ::= TYPE → TYPE # Function type | NAME # Nominal | ( TYPE ) # Parenthesized
You can run the examples as follows:
cargo run --example=end-to-end
- :: (int → int) + :: (int → (int → int)) 5 Inferred type: int "hello" Inferred type: str true Inferred type: bool ((+ 1) 2) Inferred type: int ((+ true) false) Error: Cannot unify `int` with `bool` let id = λx.(x x) in id Error: `'t0` and `('t0 → 't1)` are recursive ...
Planned/finished features are:
- Lexing (regex)
- Parsing (LALRPOP)
- Alpha conversion (De-Brujin Indices)
- Bi-directional type inference (Hindley-Milner, Algorithm W)
- Type classes
Quality of life: