Agda和Idris的区别
我开始深入依赖类型编程，并发现Agda和Idris语言最接近Haskell，所以我从那里开始。
我的问题是：它们之间的主要区别是什么？ 这两种类型的系统是否同等表达？ 对收益进行全面的比较和讨论是非常好的。
我已经能够发现一些：
编辑：在这个问题的Reddit页面有更多的答案：http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/
我可能不是最好的人来回答这个问题，因为实施了伊德里斯我可能有点偏见！ 常见问题解答 - http://docs.idris-lang.org/en/latest/faq/faq.html - 有话要说，但有一点扩展：
伊德里斯从头开始被设计为在定理证明之前支持通用编程，因此具有高级特性，如类型类，符号，成语括号，列表解析，重载等。 伊德里斯在交互式证明之前提出了高级程序设计，尽管因为伊德里斯是建立在基于策略的阐述者之上的，所以存在基于策略的交互式定理证明者的界面（有点像Coq，但不像先进的，至少还没有）。
嵌入式DSL实现还有另一件事Idris的目标是支持。 有了Haskell，你可以用符号表示很长的路，而且你也可以用Idris，但是如果需要的话，你也可以重新绑定其他结构，例如应用程序和变量绑定。 您可以在本教程中找到关于此的更多详细信息，或者在本文中查看完整详细信息：http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf
另一个区别在于汇编。 Agda主要通过Haskell，Idris通过C进行。Agda有一个实验性的后端，它使用与Idris相同的后端，通过C.我不知道维护得如何。 Idris的主要目标始终是生成高效的代码 - 我们可以做得比现在做得更好，但我们正在努力。
Agda和Idris的类型系统在很多重要方面都非常相似。 我认为主要区别在于处理宇宙。 Agda具有宇宙多态性，Idris具有累积性（如果发现这种限制太多，并且不介意证明可能不合适，则可以在Set : Set ）。
伊德里斯和阿格达之间的另一个区别是伊德里斯的命题平等是异质的，而阿格达是同质的。
换句话说，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中，它可以取两个具有不同类型的值。
换句话说，在伊德里斯，人们可以声称两种不同类型的东西是平等的（即使它最终是一个无法证明的主张），而在阿格达，这种说法是无稽之谈。
这对类型理论具有重要而广泛的影响，特别是关于使用同伦类型理论的可行性。 为此，异类平等不会起作用，因为它需要一个与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 ，所以这种说法在同质平等下是无意义Vect ((n + m) + o) a 。 这是一个非常明智的声明与异质平等。