Skip to content

Normalization by evaluation for Martin-Löf Type Theory with dependent records

License

Notifications You must be signed in to change notification settings

brendanzab/rust-nbe-for-mltt

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

rust-nbe-for-mltt

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)

TODO

  • Convert data types to Rust
  • Port NbE and bidirectional type checking
  • Add a parser for the concrete syntax
  • Desugaring of concrete syntax to core syntax
  • Resugaring of core syntax to concrete syntax
  • Pretty printing
    • Basic pretty printing
    • Preserve pretty names through type checking and normalization
    • Unfold metavariables when pretty printing values
    • Attempt to avoid unfolding variables when pretty printing values
  • Add a REPL
  • Add span information to ASTs to improve diagnostics
  • Pattern matching elaboration
    • Simple cases
    • Nested cases
    • Multiple scrutinees
    • Lambda case
  • Dependent record types
  • Primitive operations
  • Unification
  • Metavariable insertion
  • Integration tests
    • Parse (pass)
    • Parse (fail)
    • Elaboration (pass)
    • Elaboration (fail)
    • Normalization tests
    • Sample modules
  • Error recovery in:
    • Lexer
    • Parser
    • Elaborator
    • Validator