There's something oddly satisfying about making slow code run faster. This thing (some code with lots of type level computation) took 14 minutes to typecheck in Idris2 two days ago...pic.twitter.com/nNpNonUZOx
You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
Also worth adding: I'm fairly confident I haven't broken anything while doing this, because whatever I do has to get past a separate checker for the core language (~500 LOC) Your language with fancy types *does* have a separately checkable core, doesn't it? :)
It always comes down to the "just", doesn't it? I would be more than happy to help with Idris 2 codegen, but I don't really know where to start.
Indeed! Fortunately we're now in the position Idris 1 was a couple of years ago when first trying to get Idris 2 to run fast enough, so the problems are familiar by now. The key to it is getting the Inliner to work hard enough.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.