sixty
A type checker for a dependent type theory using normalisation by evaluation, with an eye on performance. Might go into Sixten one day.
Roadmap
- Surface syntax
- Core syntax
- Safe and fast phantom typed De Bruijn indices
- Evaluation
- Inlining of globals
- Readback
- Parsing
- Indentation-sensitivity
- Pretty printing
- Scope-aware name printing
- Unification and meta variables
- Pruning
- The "same meta variable" intersection rule
- Solution inlining
- Elaboration of meta variable solutions to local definitions
- Case expression inversion
- Basic type checking
- Elaboration postponement ("impredicative polymorphism" inference)
- Lazily written solutions
- Approximate polymorphic variable inference
- Query architecture
- Parallel type checking
- Simple modules
- Top-level definitions
- Name resolution
- Imports
- Tests
- Error tests
- Multi-module tests
- Position-independent implicit arguments
- Errors
- Source location tracking
- Meta variable locations
- Error recovery during
- Parsing
- Elaboration
- Unification
- Print the context and let-bound variables (including metas)
- Source location tracking
- Data
- Elaboration of data definitions
- Constructors
- Type-based overloading
- ADT-style data definitions
- Pattern matching elaboration
- Case expressions
- Exhaustiveness check
- Redundant pattern check
- Clause elaboration
- Pattern lambdas
- Inductive families
- Glued evaluation
- Let definitions by clauses
- Mutually recursive lets
- Command-line parser
- Language server
- Diagnostics
- Hover
- Print the context and let-bound variables (including metas)
- Jump to definition
- Multi file projects
- Reverse dependency tracking
- Completion
- Type-based refinement completion snippets
- Find references
- Renaming
- Code lenses
- Language server tests
- File watcher
- Cached builds
- Per-module caches
- Backend
- Typed lambda lifting
- Recursive let bindings
- Typed closure conversion
- Code generation
- Basics
- Closures
- Precise, moving garbage collector
- Cheney's two-space algorithm
- Generational GC
- Extern code
- Typed lambda lifting
- Prevent CBV-incompatible circular values
- Literals
- Numbers
- Strings
- Records
- Binary/mixfix operators
- REPL
- Integrate into Sixten
Inspiration
- András Kovács' smalltt and work on Dhall
- Thierry Coquand's semantic type checking
- Danny Gratzer's nbe-for-mltt