阿格达和伊德里斯之间的区别 [英] Differences between Agda and Idris
问题描述
我开始研究依赖类型的编程，并且发现Agda和Idris语言是最接近Haskell的语言，所以我从这里开始.
I'm starting to dive into dependently-typed programming and have found that the Agda and Idris languages are the closest to Haskell, so I started there.
我的问题是:它们之间的主要区别是什么?两种类型的系统都同样富有表现力吗?进行全面的比较并讨论收益将是很棒的.
My question is: which are the main differences between them? Are the type systems equally expresive in both of them? It would be great to have a comprehensive comparative and a discussion about benefits.
我已经发现了一些东西:
I've been able to spot some:
- Idris具有类型类àla Haskell，而Agda带有实例参数
- Idris包含一元和适用的符号
- 它们两者似乎都具有某种可重新绑定的语法，尽管不确定它们是否相同.
Edit: there are some more answers in the Reddit page of this question: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/
推荐答案
我可能不是回答这个问题的最佳人选，因为实施Idris可能会使我有些偏颇！常见问题解答- http://docs.idris-lang.org/en/最新的/faq/faq.html -上面有话要说，但要扩大一点:
I may not be the best person to answer this, as having implemented Idris I'm probably a bit biased! The FAQ - http://docs.idris-lang.org/en/latest/faq/faq.html - has something to say on it, but to expand on that a bit:
Idris是从头开始设计的，可以在定理证明之前支持通用编程，因此具有高级功能，例如类型类，符号表示法，成语括号，列表理解，重载等. Idris将高级编程置于交互式证明之前，尽管Idris基于基于战术的详细说明程序构建，所以存在基于接口的交互式定理证明器的接口(有点像Coq，但还不那么先进，至少现在还不行).
Idris has been designed from the ground up to support general purpose programming ahead of theorem proving, and as such has high level features such as type classes, do notation, idiom brackets, list comprehensions, overloading and so on. Idris puts high level programming ahead of interactive proof, although because Idris is built on a tactic-based elaborator, there is an interface to a tactic based interactive theorem prover (a bit like Coq, but not as advanced, at least not yet).
Idris旨在支持的另一件事是嵌入式DSL实现.使用Haskell，您可以在不使用符号的方式上走很长的路，也可以使用Idris，但是如果需要，还可以重新绑定其他结构，例如应用程序和变量绑定.您可以在本教程中找到更多详细信息，或者在本文中找到全部详细信息: http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf
Another thing Idris aims to support well is Embedded DSL implementation. With Haskell you can get a long way with do notation, and you can with Idris too, but you can also rebind other constructs such as application and variable binding if you need to. You can find more details on this in the tutorial, or full details in this paper: http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf
另一个区别是在编译上. Agda主要通过Haskell，Idris通过C.Agda有一个实验性后端，它通过C与Idris使用相同的后端.我不知道它的维护程度如何. Idris的主要目标始终是生成高效的代码-我们可以做得比现在好得多，但我们正在努力.
Another difference is in compilation. Agda goes primarily via Haskell, Idris via C. There is an experimental back end for Agda which uses the same back end as Idris, via C. I don't know how well maintained it is. A primary goal of Idris will always be to generate efficient code - we can do a lot better than we currently do, but we're working on it.
Agda和Idris中的类型系统在许多重要方面非常相似.我认为主要区别在于处理宇宙.阿格达(Agda)具有宇宙多态性，伊德里斯(Idris)具有累积率(如果您会发现此限制过于严格，不必介意您的证明可能不正确.
The type systems in Agda and Idris are pretty similar in many important respects. I think the main difference is in the handling of universes. Agda has universe polymorphism, Idris has cumulativity (and you can have Set : Set in both if you find this too restrictive and don't mind that your proofs might be unsound).
这篇关于阿格达和伊德里斯之间的区别的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
