Skip to content
<open-source>
Oeiuwq Faith Blog OpenSource Porfolio

ollef/sixty

Dependent type checker using normalisation by evaluation
Source code at GitHub null
ollef/sixty.json
{
  "createdAt": "2019-04-27T21:22:21Z",
  "defaultBranch": "main",
  "description": "Dependent type checker using normalisation by evaluation",
  "fullName": "ollef/sixty",
  "homepage": null,
  "language": "Haskell",
  "name": "sixty",
  "pushedAt": "2024-09-05T18:35:20Z",
  "stargazersCount": 269,
  "topics": [],
  "updatedAt": "2025-11-02T00:18:43Z",
  "url": "https://github.com/ollef/sixty"
}

sixty

Section titled “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

Section titled “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)
  • 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
    • Smart case
  • 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
  • Prevent CBV-incompatible circular values
  • Literals
    • Numbers
    • Strings
  • Records
  • Binary/mixfix operators
  • REPL
  • Integrate into Sixten

Inspiration

Section titled “Inspiration”