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.

Syntax

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

Testing

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:

Front-end

• [x] Lexing (regex)
• [x] Parsing (LALRPOP)
• [ ] Alpha conversion (De-Brujin Indices)
• [x] Bi-directional type inference (Hindley-Milner, Algorithm W)
• [ ] Type classes

Quality of life:

• [x] Pretty printing
• [x] Error recovery
• [ ] Language Server Protocol integration (LSP using codespan)

Middle-end

N/A

Back-end

N/A

Learning resources

• Ionut G. Stan: Let’s write a type checker @ I T.A.K.E. Unconference 2015
• A basic implementation of Hindley-Milner type inference via Algorithm W in Rust.
• f(by) 2019 - Christoph Hegemann, TYPE INFERENCE FROM SCRATCH