• Stars
    star
    253
  • Rank 160,776 (Top 4 %)
  • Language
    Haskell
  • License
    Other
  • Created over 5 years ago
  • Updated 3 months ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Dependent type checker using normalisation by evaluation

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

  • 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
  • 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

More Repositories

1

sixten

Functional programming with fewer indirections
Haskell
757
star
2

Earley

Parsing all context-free grammars using Earley's algorithm in Haskell.
Haskell
360
star
3

Bidirectional

Haskell implementation of Dunfield and Krishnaswami's "Complete and easy bidirectional typechecking for higher-rank polymorphism"
Haskell
123
star
4

rock

Build system
Haskell
114
star
5

braces-be-gone

Get those pesky braces out of your face
Haskell
49
star
6

Generate-C

Embedded C code generation DSL for Haskell.
Haskell
27
star
7

dependent-hashmap

Dependent hash maps
Haskell
14
star
8

rope-utf16-splay

Thick strings optimised for indexing and updating using UTF-16 code units and row/column pairs
Haskell
14
star
9

parsix

Adventures in parser combinators
Haskell
10
star
10

region

Adventures in region inference
Haskell
8
star
11

mirrored-keyboard-layouts

Mirrored XKB layouts for one-handed typing
8
star
12

Grempa

Embedded grammar DSL and LALR parser generator
Haskell
8
star
13

navm-hs

Not a virtual machine
Haskell
6
star
14

navm

Not A Virtual Machine
Rust
6
star
15

environment-bench

Benchmarking compiler representations of variable environments
Haskell
5
star
16

incrementalism

Haskell
4
star
17

Fuse.JSON

Convert various things (JavaScript values, Objective-C objects) to and from JSON in Uno
Uno
4
star
18

oslo-haskell

Exercises
Haskell
4
star
19

packrat

Adventures in packrat parsing
Haskell
3
star
20

rope-utf16

Haskell
3
star
21

ibuild

Indexed build systems a la carte
Haskell
2
star
22

FunSharp

Learning F#, nothing to see here
F#
2
star
23

vim-svorsk

Vim for Swedes in Norway
Vim Script
2
star
24

paws

Utility for automatically pausing and resuming music at appropriate times.
C
2
star
25

fenwick

Self-balancing Fenwick trees with logarithmic time monoidal prefix sums
Haskell
2
star
26

by-value

Polymorphism without pointer indirections in C++, allowing you to store and pass subclass objects by value
C++
1
star
27

llvm-irbuilder

IRBuilder for LLVM Haskell Bindings ( Experimental )
Haskell
1
star
28

system-rea

Dad made me do it
Haskell
1
star
29

deriving-gcompare

Derive instances for GEq and GCompare from the dependent-sum package
Haskell
1
star
30

ollef.github.io

HTML
1
star
31

postgres-woobat

Haskell
1
star
32

rope-bench

Haskell
1
star
33

satire

Satisfaction
Rust
1
star