Normalization by evaluation for Martin-Löf Type Theory with dependent records
MIT License
This originally started as a Rust port of Danny Gratzer's implementation of Normalization by Evaluation for Martin-Löf Type Theory, but it has a slightly different architecture and some additional language features. The algorithm for the insertion and unification of metavariables was partly taken from Andras Korvacs' Minimal TT Exampls and smalltt (although gluing is not yet implemented here). It will probably become the basis for a new front-end for Pikelet.
In traditional type checking and normalization that uses DeBruijn indices, you are required to shift variable indices whenever you open up binders. This is extremely expensive, and rules out future optimizations, like using visitors to reduce the number of intermediate allocations as the AST is traversed. This implementation avoids these problems by using a "semantic type checking" algorithm that uses DeBruijn indices for the core syntax, and DeBruijn levels in the syntax of the semantic domain.
Syntax | Binding method | Example |
---|---|---|
Concrete | Nominal | λz. (λy. y (λx. x)) (λx. z x) |
Core | Nameless (DeBruijn Indices) | λ . (λ . 0 (λ . 0)) (λ . 1 0) |
Domain | Nameless (DeBruijn Levels) | λ . (λ . 1 (λ . 2)) (λ . 0 1) |