[xuejie]

The author first goes with:

> Idris 1 is implemented in Haskell, but that has little (if anything) to do with the difference.

But latter they also go on to say:

> Idris 2 benefits from a robust, well-engineered and optimised run time system, by compiling to Chez Scheme.

I must say I'm slightly confused here. Yes a rewrite might also enable to avoid all the legacy part that might slow down the code, but what is also possible, is that a new language and a new runtime could enable new optimizations that are not possible before. The author did mention Chez's profiling tools help a lot in the rewrite. So I was curious: is it really true, that we cannot attribute some part of the speedup to language differences?

Also I was interested in the rationale behind using Scheme to replace Haskell, but I failed to find some reasoning behind this, anyone can shed some light on this?

[kccqzy]

That's not relevant at all. I think you have misunderstood the situation here. In Idris 1 the compiler and code generator is in Haskell, but the runtime is in C. So Scheme isn't exactly replacing Haskell but replacing C, for the runtime. (What replaced Haskell was Idris itself, by virtue of being self-hosting.)

The author even says that it's difficult to write C that deals well with the functional style of lots of little functions, and this is a problem Scheme also has and has solved. That's enough rationale to switch to Scheme:

> Generating good C code corresponding to a functional program which might have lots of small (and higher order) definitions is extremely challenging, so it is better to take advantage of someone else's work here.

[kryptiskt]

Scheme isn't used to replace Haskell. Idris 1 is written in Haskell and compiled by default to C (it comes with a Javascript backend too and it has an API for making others). Idris 2 is written in Idris 2 and compiles to Scheme so far (Chez by default, there is also support for Racket and Gambit), it's not tied to scheme but there is no pluggable backend functionality yet.

So Scheme is replacing C, and Idris is replacing Haskell. The goal was self-hosting by writing the compiler in Idris. Chez Scheme is a nice compilation target because it's performant and Scheme is a sugared lambda calculus that goes well together with FP languages.

[xuejie]

Thanks guys for the explanation! I truly have misunderstood this post.