我开始深入研究依赖类型编程，并发现Agda和Idris语言最接近Haskell，所以我从那里开始。
我的问题是：它们之间的主要区别是什么？它们的类型系统是否同样具有表现力？很好地进行全面比较并讨论其优点。
我已经能够发现一些差异：
编辑: 在这个问题的Reddit页面上还有更多答案：http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/
Idris从一开始就被设计成支持通用编程而不是定理证明，因此具有高级特性，如类型类、do表示法、范畴括号、列表推导、重载等。Idris把高级编程放在交互式证明之前，尽管因为Idris建立在基于策略的展开器上，所以有一个与策略相关的交互式定理证明接口（有点像Coq，但不那么先进，至少目前还不是）。
Agda和Idris中的类型系统在许多重要方面非常相似。我认为主要区别在于宇宙的处理。Agda具有宇宙多态性，Idris具有cumulativity（如果您发现这太限制并且不介意证明可能不正确，则两者都可以使用Set:Set）。
Idris和Agda之间的另一个区别是，Idris的命题等式是异构的，而Agda的是同构的。
换句话说，在Idris中所谓的等式定义为：
data (=) : {a, b : Type} -> a -> b -> Type where
refl : x = x
当在Agda中时，它是
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)根据自然数上 + 的结合律（从归纳原理得出）在判断上是相等的。因此，等式两边的类型是相同的。虽然等式类型的差异很重要，但我看不出这是一个例子。 - user788472