Edwin Brady spoke at the Scheme Workshop last week about making Chez Scheme the backend for Idris 2. But just now on Twitter he said that Racket-on-Chez outperforms Chez for this purpose and he may make it the default.

whoa, nifty

That’s surprising.

Did he know why that was?

Oh, I see this: https://github.com/edwinb/Idris2/pull/90#issuecomment-526119964

So the claim isn’t that the code runs faster but that it’s about the same and the infrastructure is better. Which sounds about right.

My first guess (expressed to Edwin at ICFP): extra inlining by schemify. My newer guess, which is probably better: Idris is compiled to a let wrapping definitions, and Racket’s semantics for internal definitions is more optimizer-friendly.

Oh, so he does get better performance from Racket. Nice!