I bought the book "Type Driven Development in Idris" and got several chapters in before getting distracted by whatever else. It was enough that I'm now annoyed relatively often that I can't pass types as parameters to be altered during execution. I really think they're onto something brilliant. I need to pick it back up and finish the book.
Chez Scheme has an interesting compiler [1] and has also been adopted by Racket [2].<p>It really cool to see a little used lisp have such a great impact.<p>[1] <a href="https://news.ycombinator.com/item?id=15156027" rel="nofollow">https://news.ycombinator.com/item?id=15156027</a><p>[2] <a href="https://blog.racket-lang.org/2020/02/racket-on-chez-status.html" rel="nofollow">https://blog.racket-lang.org/2020/02/racket-on-chez-status.h...</a>
How practical is Idris (or Idris 2) for real-world production programming right now? It seems to be a pretty natural evolution of Haskell with dependent types built in from the ground up instead of being sort of achievable with a patchwork of language extensions. Moreover, making laziness optional is a big deal for real-world industrial applications. (Note that even the author of this post indicates at the end significant difficulty with space leaks in the original Haskell compiler for Idris.)<p>Or, said differently, what's missing in the language or ecosystem to make it more immediately practical? Could Idris be the successor to Haskell with appropriate support?
I find this slightly depressing that using global mutable state had such a significant performance given the functional programming (encompassing Idris) is very much in favor of immutable data structures and purity. I know it's best to explicitly switch to mutability iff a bottleneck is found (like how `mut` is explicit and not default in Rust), but I want to <i>believe</i> that Idris can live in a purity. This makes me think my opinions are not far off from religion.
The usual answer for such a question about X2 and X1 is that X1 was really slow. It is usually correct, with the proviso that X2 might <i>still</i> be really slow, only less so.<p>With most computer artifacts, it is hard to tell, <i>prima facie</i>, that they are slow, until somebody makes a faster one. Then the original comes to be recognized as slow (although somebody will still insist it's not <i>that</i> slow). The faster one might still be slow, but that fact remains unknown.<p>The fact is that almost everything is slow, in the sense that somebody smarter, more experienced, and more diligent could make it faster, often by doing things that the person who wrote the slow version would have found distasteful.
The author first goes with:<p>> Idris 1 is implemented in Haskell, but that has little (if anything) to do with the difference.<p>But latter they also go on to say:<p>> Idris 2 benefits from a robust, well-engineered and optimised run time system, by compiling to Chez Scheme.<p>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?<p>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?