- 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
[type Shape
[Circle Float]
[Rect Float Float]]
[fn area [s]
[match s
[Circle r] => [* 3.14 r r]
[Rect w h] => [* w h]]]
[area [Circle 5.0]]