我开始深入研究依赖类型编程，发现 Agda 和 Idris 语言最接近 Haskell，所以我从那里开始。
我的问题是：它们之间的主要区别是什么？类型系统在它们中是否同样具有表现力？对收益进行全面的比较和讨论会很棒。
我已经能够发现一些：
编辑：这个问题的 Reddit 页面中有更多答案：http ://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/
我可能不是回答这个问题的最佳人选，因为实施了 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如果您觉得这太严格并且不介意您的证明可能不可靠，您可以同时拥有这两者）。
Idris 和 Agda 之间的另一个区别是 Idris 的命题等式是异质的，而 Agda 的命题等式是同质的。
换句话说，Idris 中对平等的假定定义是：
data (=) : {a, b : Type} -> a -> b -> Type where
refl : x = x
在阿格达，它是
data _≡_ {l} {A : Set l} (x : A) : A → Set a where
refl : x ≡ x
Agda 定义中的 l 可以忽略，因为它与 Edwin 在他的回答中提到的宇宙多态性有关。
重要的区别在于 Agda 中的相等类型将 A 的两个元素作为参数，而在 Idris 中，它可以采用两个可能具有不同类型的值。
换句话说，在 Idris 中，人们可以声称具有不同类型的两个事物是相等的（即使它最终成为无法证明的主张），而在 Agda 中，这种陈述本身就是无稽之谈。
这对类型理论具有重要而广泛的影响，特别是在使用同伦类型理论的可行性方面。为此，异构相等是行不通的，因为它需要一个与 HoTT 不一致的公理。另一方面，可以用异质等式陈述有用的定理，而这些定理不能用齐次等式直接陈述。
也许最简单的例子是向量连接的结合性。给定这样定义的称为向量的长度索引列表：
data Vect : Nat -> Type -> Type where
Nil : Vect 0 a
(::) : a -> Vect n a -> Vect (S n) a
并与以下类型连接：
(++) : Vect n a -> Vect m a -> Vect (n + m) a
我们可能想证明：
concatAssoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) ->
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
这句话在齐次等式下是无稽之谈，因为等式的左边有类型Vect (n + (m + o)) a，右边有类型Vect ((n + m) + o) a。这是一个具有异质性平等的完全明智的陈述。