MLTT - A Minimal Martin-Löf Type Theory Implementation

A pedagogical implementation of Martin-Löf Type Theory in Rust.

Features

• Pi Types (Π): Dependent function types
• Sigma Types (Σ): Dependent pair types
• Identity Types: Propositional equality with J eliminator
• Universe Hierarchy: Predicative universes to avoid paradoxes
• Inductive Types: User-defined data types
• Pattern Matching: Compiled to eliminators

Syntax Overview

-- Type annotations
id : (A : Type) -> A -> A
id = \A => \x => x

-- Dependent function types (Pi)
(x : A) -> B x        -- dependent
A -> B                -- non-dependent (sugar)

-- Dependent pair types (Sigma)
(x : A) * B x         -- dependent  
A * B                 -- non-dependent (sugar)

-- Pairs
p : Nat * Bool
p = (42, true)
fst p                 -- 42
snd p                 -- true

-- Identity types
refl : a == a
J : (P : (x y : A) -> x == y -> Type) -> 
    ((z : A) -> P z z refl) ->
    (a b : A) -> (p : a == b) -> P a b p

-- Inductive types
data Nat : Type where
  zero : Nat
  succ : Nat -> Nat

-- Pattern matching
add : Nat -> Nat -> Nat
add = \m => \n => case m of
  zero => n
  succ m' => succ (add m' n)

Building

cargo build --release

Usage

REPL

cargo run

File Execution

cargo run -- examples/nat.mltt

Project Structure

src/
├── syntax/        # AST definitions
├── parser/        # Lexer and recursive descent parser
├── elaborate/     # Surface -> Core elaboration
├── typing/        # Bidirectional type checking
├── nbe/           # Normalization by Evaluation
├── inductive/     # Inductive type handling
└── repl/          # Interactive environment

References

• Per Martin-Löf, "Intuitionistic Type Theory" (1984)
• Andras Kovacs, "Elaboration Zoo"
• David Christiansen, "Checking Dependent Types with Normalization by Evaluation"

License

MIT