TE
科技回声
首页24小时热榜最新最佳问答展示工作
GitHubTwitter
首页

科技回声

基于 Next.js 构建的科技新闻平台,提供全球科技新闻和讨论内容。

GitHubTwitter

首页

首页最新最佳问答展示工作

资源链接

HackerNews API原版 HackerNewsNext.js

© 2025 科技回声. 版权所有。

Why is Idris 2 so much faster than Idris 1?

282 点作者 culturedsystems将近 5 年前

8 条评论

ngngngng将近 5 年前
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.
评论 #23306926 未加载
评论 #23306092 未加载
评论 #23308599 未加载
papaf将近 5 年前
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:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=15156027" rel="nofollow">https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=15156027</a><p>[2] <a href="https:&#x2F;&#x2F;blog.racket-lang.org&#x2F;2020&#x2F;02&#x2F;racket-on-chez-status.html" rel="nofollow">https:&#x2F;&#x2F;blog.racket-lang.org&#x2F;2020&#x2F;02&#x2F;racket-on-chez-status.h...</a>
评论 #23304800 未加载
评论 #23304646 未加载
nilkn将近 5 年前
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&#x27;s missing in the language or ecosystem to make it more immediately practical? Could Idris be the successor to Haskell with appropriate support?
评论 #23308684 未加载
toastal将近 5 年前
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&#x27;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.
评论 #23308488 未加载
评论 #23308232 未加载
评论 #23307684 未加载
评论 #23320272 未加载
nikivi将近 5 年前
What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
评论 #23304663 未加载
评论 #23304671 未加载
评论 #23304705 未加载
评论 #23304415 未加载
评论 #23304528 未加载
评论 #23309054 未加载
评论 #23305925 未加载
评论 #23309375 未加载
评论 #23304417 未加载
ncmncm将近 5 年前
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&#x27;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.
评论 #23307651 未加载
xuejie将近 5 年前
The author first goes with:<p>&gt; 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>&gt; Idris 2 benefits from a robust, well-engineered and optimised run time system, by compiling to Chez Scheme.<p>I must say I&#x27;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&#x27;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?
评论 #23306590 未加载
评论 #23306681 未加载
评论 #23307233 未加载
评论 #23307393 未加载
PunksATawnyFill将近 5 年前
What is Idris?<p>Critical info missing.
评论 #23306872 未加载