4 ms·

Well minor including the switch to use of so called “quantitative type theory” where you can include use counts for variables that inform the compiler how long

Well minor including the switch to use of so called “quantitative type theory” where you can include use counts for variables that inform the compiler how long variables will stick around. Also the compiler switch to Chez Scheme yields a pretty big performance boost.

zelphirkalt 6y ago
The Idris 2 compiler is build with Chez Scheme? That's pretty cool in my opinion, didn't know that.
- mjepronk 6y ago
  It compiles to Chez Scheme. It's written in Idris 2 (self-hosted).
- rq1 6y ago
  It is written with Idris2 as the article mentions. It produces/translates to Chez Scheme code.
mx00s 6y ago
You're right, there are several notable improvements in Idris2. I was mainly referring to the amount of code from the book that must be adapted. The QTT features, as you say, are opt-in; by default no new constraints are imposed.