Highlights for those not following:
- Idris2 written in Idris
- core language based on "Quantitative Type Theory" which allows explicit annotation of erased types, and linear types
- Default Chez Scheme Idris2 backend runs faster than default C Idris1 backend. 
https://twitter.com/edwinbrady/status/1148349263761629185 …
-
-
Are benchmarks with full program optimisation, or is idris2 faster even without?
-
I don't have properly scientific benchmarks so I don't want to make any strong claims, but for https://github.com/edwinb/Idris2/blob/master/tests/chez/chez002/Pythag.idr … Idris takes 6.3s vs Idris2 1.5s to calculate the length of pythag 500.
- 1 more reply
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.