Теперь Idris 2 написан на самом себе (Idris 1).
https://github.com/edwinb/Idris2
Из новых фич:
- A core language based on «Quantitative Type Theory» which allows explicit annotation of erased types, and linear types.
- let bindings are now more expressive, and can be used to define pattern matching functions locally.
- Names which are in scope in a type are also always in scope in the body of the corresponding definition.
- Better inference. Holes are global to a source file, rather than local to a definition, meaning that some holes can be left in function types to be inferred by the type checker. This also gives better inference for the types of case expressions, and means fewer annotations are needed in interface declarations.
- Better type checker implementation which minimises the need for compile time evaluation.
- New Chez Scheme based back end which both compiles and runs faster than the default Idris 1 back end. (Also, optionally, Chicken Scheme and Racket can be used as targets).
- Everything works faster :)
Сейчас это пока преальфа, но почти все примеры из книги Type-Driven Development with Idris работают с незначительными изменениями:
https://github.com/edwinb/Idris2/tree/master/tests/typedd-book
Патчи и доработки приветствуются:
https://github.com/edwinb/Idris2/blob/master/CONTRIBUTING.md
