我可能不是回答这个问题的最佳人选，因为实施了 Idris 我可能有点偏见！FAQ - http://docs.idris-
lang.org/en/latest/faq/faq.html - 有话要说，但要扩展一下：

Idris 从一开始就被设计为支持定理证明之前的通用编程，因此具有高级功能，例如类型类、do notation、成语方括号、列表推导、重载等。Idris
将高级编程置于交互式证明之前，尽管由于 Idris 建立在基于策略的详细说明器上，因此有一个基于策略的交互式定理证明器的接口（有点像 Coq，但不如 Coq
先进，至少目前还没有）。

Idris 旨在很好地支持的另一件事是嵌入式 DSL 实现。使用 Haskell，您可以使用 do 表示法，您也可以使用
Idris，但如果需要，您还可以重新绑定其他构造，例如应用程序和变量绑定。您可以在本教程中找到更多详细信息，或在本文中找到完整详细信息：http:
//eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf

另一个区别在于编译。Agda 主要通过 Haskell，Idris 通过 C。Agda 有一个实验性后端，它使用与 Idris 相同的后端，通过
C。我不知道它的维护情况如何。Idris 的主要目标始终是生成高效的代码——我们可以做得比现在更好，但我们正在努力。

Agda 和 Idris 中的类型系统在许多重要方面都非常相似。我认为主要区别在于对宇宙的处理。Agda 具有宇宙多态性，Idris
具有累积性（Set : Set如果您觉得这太严格并且不介意您的证明可能不可靠，您可以同时拥有这两者）。