To answer a question people sometimes ask: https://www.type-driven.org.uk/edwinb/why-is-idris-2-so-much-faster-than-idris-1.html … In which I explain several bad design decisions I made several years ago...
-
Show this thread
-
Replying to @edwinbrady
FYI,
@ollfredo has come up with a much simpler version of smalltt's evaluator, which I've microbenchmarked to be roughly as fast. Minimal demo: https://gist.github.com/AndrasKovacs/a0e0938113b193d6b9c1c0620d853784 … It also allows some super slick approximate conversion/scope checking which was not possible before.3 replies 3 retweets 17 likes -
Replying to @andrasKovacs6 @ollfredo
Interesting, I'll take a closer look, thanks! I don't have a particularly clever evaluator yet, and I think there's going to be some things that suffer as a result.
2 replies 0 retweets 1 like -
Replying to @edwinbrady @ollfredo
I briefly looked at Idris2 and I noted this as well. I don't think I'd actually recommend the original smalltt evaluator, because it duplicates a lot of code. The new version though is very simple and I definitely recommend it.
1 reply 0 retweets 5 likes
Hmm, actually I'd thought about a strategy a bit like the one you describe there at one point, but not enough to try it out. I might consider saving that as an exercise for an incoming PhD student, especially if you say it works well :).
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.