3 ms·
Iirc Idris2 went straight to running on chez since Edwin was so impressed by chez scheme and it's runtime.
by bjoli 7y ago
Iirc Idris2 went straight to running on chez since Edwin was so impressed by chez scheme and it's runtime.
- kryptiskt 7y agoI made a chez scheme backend for Idris a couple of years ago: https://github.com/melted/idris-chez https://github.com/melted/idris-chez About the only notable thing with it (apart from inspiring the target for Idris 2) is that it implements the C FFI, so it will handle Idris programs made to target C.
- logicchains 7y agoThe result is super fast: if you use if after using Idris1 you'll be blown away by how much quicker it type-checks. I'd never have thought a Scheme could perform noticeably faster than Haskell, but maybe most of the improvements are just due to algorithmic improvements made during the rewrite.
- bjoli 7y agoI 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.