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

科技回声

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

GitHubTwitter

首页

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

资源链接

HackerNews API原版 HackerNewsNext.js

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

Towards Idris Version 1.0

236 点作者 yomritoyj超过 8 年前

10 条评论

chriswarbo超过 8 年前
Any ideas why the effect system may be deprecated in favour of the state machine&#x2F;indexed monads system? To me, they seem to be fulfilling two different requirements: algebraic effects let us call &#x27;operations&#x27; in an expression by writing placeholder values, track the usage of such operations in the type, and plug in the implementation afterwards. For example, we can write &quot;print&quot; as a placeholder, give it a &quot;StdOut&quot; effect type, and provide a production implementation which writes to the program&#x27;s stdout, a test implementation which produces a normal String value for us to check, a remote implementation which writes to a WebSocket, etc.<p>The state machine stuff seems to mostly be concerned with using types to keep track of state, in terms of which actions are available or unavailable, e.g. you can&#x27;t close a file unless it&#x27;s open, you can&#x27;t read from a file unless it&#x27;s open, you can&#x27;t run an expression unless it closes all of its files, etc.<p>There&#x27;s certainly overlap, but I&#x27;m not sure whether one subsumes the other.
评论 #13075710 未加载
评论 #13078657 未加载
评论 #13075027 未加载
tupshin超过 8 年前
Is anybody still thinking about Idris and HoTT? <a href="https:&#x2F;&#x2F;github.com&#x2F;fmota&#x2F;HoTT-Idris&#x2F;blob&#x2F;master&#x2F;README.md" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;fmota&#x2F;HoTT-Idris&#x2F;blob&#x2F;master&#x2F;README.md</a> I don&#x27;t see anything more recent than the 2014 discussions.
chriswarbo超过 8 年前
Sounds good!<p>I played with Idris quite a bit in the early days. I started spending more time in Coq around the time Idris gained its proof search mechanisms (I&#x27;m still not sure how they work!), but Idris has always been a more &#x27;realistic&#x27; language for development (as opposed to proof engineering).<p>I think I spoiled myself with dependent types, as all of my Haskell projects seem to hit a wall which dependent types can trivially solve (e.g. calculating a type or a TypeRep based on incoming JSON data)
评论 #13072790 未加载
评论 #13074498 未加载
alphanumeric0超过 8 年前
I&#x27;ve been learning Haskell and Idris off and on now for a few years. I have a few friends who happen to be computer science majors and they tend to be very dismissive of Haskell, they mostly focus on the performance tweaking of a Haskell program, which seems to be a &#x27;black art&#x27;.<p>Does anyone know if Idris improves on this aspect of Haskell?
评论 #13075062 未加载
评论 #13075037 未加载
评论 #13074974 未加载
评论 #13075003 未加载
amckinlay超过 8 年前
Would be nice to see a dependently-typed strict functional programming language that didn&#x27;t require a GC or a C runtime. Are there any plans for this with Idris?
评论 #13075582 未加载
评论 #13077453 未加载
评论 #13075055 未加载
评论 #13085347 未加载
weavie超过 8 年前
This is pretty exciting. I&#x27;m still only about halfway through the book, but I am really enjoying the language. Learning it has been a real brain melter (in a good way) so far. Am looking forward to finishing the book.<p>I do appreciate how you can use dependant types as much or as little as you like, so in some ways it can actually be considered a simpler and easier to learn Haskell due to having strict evaluation.
hood_syntax超过 8 年前
Great to see. Idris is pretty much the final frontier for what I see value in becoming comfortable with as far as functional programming goes. Hopefully it gets more momentum moving forward.
评论 #13074468 未加载
gcanti超过 8 年前
what&#x27;s the state of the JavaScript backend? I do frontend and I&#x27;d really love to write some code in idris
评论 #13079218 未加载
vesak超过 8 年前
How are packages handled in Idris? Do they have a cargo&#x2F;composer&#x2F;npm analogue?
posterboy超过 8 年前
Quick question, does design by contract, ie. invariants and so on, warrant calling dependent typing? I&#x27;m currently learning OCL, and Haskell next, hence the question.