- Self-hosted
- Compiles to javascript
- Bidirectional typechecking with NbE (based on elaboration zoo)
- Dependent type checking
- type classes
- ADTs with dependent pattern matching
- TCO (trampoline for mutually tail recursive functions)
- Erasure of compile-time only values (0, ω quantities, but not linear)
- Web playground
- LSP (added this month)
- Syntax is similar to Agda / Idris / Haskell
EDIT: Actually, it's not quite "ML-family" enough for this post. But it is a remarkably cool project! :)
And here is a set of single file lambda calculus implementations with a variety of extensions: https://github.com/solomon-b/lambda-calculus-hs
`polytt` is kind of an ended experiment but that lambda calculus repo i plan to extend in the near future.