3 ms·
I never played with Idris2, but I recall running some idris1 programs using the chez scheme backend instead of thebc one and got instant 5x speedups. Across the
by bjoli 7y ago
I never played with Idris2, but I recall running some idris1 programs using the chez scheme backend instead of thebc one and got instant 5x speedups. Across the board.
Not that it wouldn't be possible to make the C code fast. It is just that the chez backend was a one man job.
- kryptiskt 7y agoThank the Chez Scheme developers for an absolutely fantastic compiler, and also Idris for being designed so that it's possible to feed any of the IRs to the particular backend. There's not much of an impedance mismatch between Scheme and Idris lambda output, so the overhead is small. I could have made it a bit better if I had represented Idris lists and bools as the corresponding scheme types, instead of being mapped as all the other types by their structure.