我开始深入研究依赖类型编程，发现 Agda 和 Idris 语言最接近 Haskell，所以我从那里开始。
我的问题是:它们之间的主要区别是什么？它们中的类型系统是否具有同样的表现力？对好处进行全面的比较和讨论会很棒。
我已经能够发现一些:
编辑:这个问题的 Reddit 页面中有更多答案:http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/
最佳答案
我可能不是回答这个问题的最佳人选，因为实现了 Idris 我可能有点偏见!常见问题解答 - http://docs.idris-lang.org/en/latest/faq/faq.html - 有话要说，但要稍微扩展一下:
Idris 从头开始设计，以支持定理证明之前的通用编程，因此具有高级功能，例如类型类、do 表示法、习语括号、列表理解、重载等。 Idris 将高级编程置于交互式证明之前，尽管因为 Idris 建立在基于策略的阐述器上，所以有一个基于策略的交互式定理证明器的接口(interface)(有点像 Coq，但没有那么先进，至少现在还没有)。
Idris 旨在支持的另一件事是嵌入式 DSL 实现。使用 Haskell，您可以使用 do 表示法，您也可以使用 Idris，但如果需要，您还可以重新绑定(bind)其他构造，例如应用程序和变量绑定(bind)。你可以在教程中找到更多细节，或者在这篇论文中找到完整的细节:http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf
另一个区别在于编译。 Agda 主要通过 Haskell，Idris 通过 C。Agda 有一个实验性后端，它使用与 Idris 相同的后端，通过 C。我不知道它的维护情况如何。 Idris 的主要目标始终是生成高效的代码——我们可以做得比目前做得更好，但我们正在努力。
Agda 和 Idris 中的类型系统在许多重要方面非常相似。我认为主要区别在于对宇宙的处理。 Agda 有全域多态性，Idris 有 cumulativity(如果你觉得这太严格并且不介意你的证明可能不可靠，你可以在两者中都有 Set : Set)。
关于agda - Agda 和 Idris 之间的差异，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/9472488/