Need help with sixty?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

ollef
178 Stars 7 Forks BSD 3-Clause "New" or "Revised" License 1.1K Commits 2 Opened issues

Description

Dependent type checker using normalisation by evaluation

Services available

!
?

Need anything else?

Contributors list

# 214,433
Vim
Firefox
Haskell
agda
1046 commits
# 102,484
Haskell
Zsh
Git
idris
1 commit
# 261,846
Vim
Shell
proc-ma...
trait
1 commit

sixty Gitter chat

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] 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] 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
  • [ ] Prevent CBV-incompatible circular values
  • [ ] Literals
    • [x] Numbers
    • [ ] Strings
  • [ ] Records
  • [ ] Binary/mixfix operators
  • [ ] REPL
  • [ ] Integrate into Sixten

Inspiration

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.