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 …
-
-
Replying to @SusanPotter
It is pretty silly that an untyped backend can run faster than the old C backend. Does Chez Scheme perform its own type inference to ensure a sane value representation?
2 replies 0 retweets 0 likes -
Replying to @sigkill_dk @SusanPotter
I think its mostly that decades of engineering by specialists beats my effort! The GC is much better, and turning off runtime checks helps quite a bit too.
1 reply 0 retweets 9 likes -
Are benchmarks with full program optimisation, or is idris2 faster even without?
1 reply 0 retweets 0 likes -
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 reply 1 retweet 5 likes
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!
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.