Edwin BradyJul 24, 2021
The main goal of my research is to find the most contrived way of calculating 2+2. Latest effort: https://gist.github.com/edwinb/00319dfe5aebcedc3849fffd428e4123#file-eval-idr-L143-L225
Eval.idr

GitHub Gist: instantly share code, notes, and snippets.

Show threadEdwin BradyJul 24, 2021

This is a toy language that compiles to Scheme so it can use the Scheme evaluator on open terms, then read back from Scheme to its syntax.

That last example runs instantly. In contrast, the Idris evaluator takes 15 seconds on the equivalent. I might have some fun with this...

Show threadEdwin Brady
I suppose if your runtime just happens to include a compiler for the lambda calculus, you might as well see what you can do with it...
Jul 24, 2021 at 11:44pmMoa
Show threadEdwin BradyJul 29, 2021
Turns out this does adapt to Idris, yay! Although this fork of Idris is currently like a golf course, in that it has 18 holes and involves someone shouting FOUR a lot.
Show threadEdwin BradyJul 29, 2021

Okay, so I've actually got a bit further, it's just that I didn't think of that joke (if that's what it is) until now. #lightningwit

The scheme based evaluator seems to be just the teensiest bit faster...

Show threadEdwin BradyJul 29, 2021
There are now 9 holes. so it's still like a golf course, albeit a smaller one.
Show threadEdwin BradyJul 29, 2021

This is important because type checking interesting dependently typed programs fundamentally relies on this evaluator. As it stands now, if Idris is slow to type check something, it's almost always the evaluator.

So I hope I can fill in those remaining holes! Place Your Bets...

Show threadCsepp 🌢Jul 30, 2021
@edwinb A possibly (definitely) naive idea: would JiT techniques help? Or is the complexity / compilation overhead too much?
Show threadEdwin BradyJul 30, 2021
@csepp In some sense that's what this is doing, but leaving all the hard work to the scheme runtime