我开始深入研究依赖类型编程，发现 Agda 和 Idris 语言最接近 Haskell，所以我从那里开始。
我的问题是：它们之间的主要区别是什么？类型系统在它们中是否同样具有表现力？如果能对收益进行全面的比较和讨论，那就太好了。
我已经发现了一些：
编辑：这个问题的Reddit页面有更多答案：http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/
【问题讨论】：
标签： agda type-theory idris
我可能不是回答这个问题的最佳人选，因为实施了 Idris 我可能有点偏颇！常见问题解答 - 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 具有 cumulativity（如果您觉得这太严格并且不介意您的证明可能不可靠，您可以同时使用 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。这是一个具有异质性平等的完全明智的陈述。
【讨论】：
(n + (m + o)) 和 ((n + m) + o) 在 ℕ 上的关联性判断上是相等的（源自归纳原理）。因此，等式的每一边确实具有相同的类型。相等类型之间的区别很重要，但我不明白这是一个例子。