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 …
-
-
Oh, a useful point of comparison is the ghc optimised equivalent, which is about 0.7s. To be honest, for such a simple hack I'm quite pleased the gap isn't bigger!
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.