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