Agda和Idris之间的差异

Question

我开始深入研究依赖类型的编程,并发现Agda和Idris语言最接近Haskell,所以我从那里开始.

我的问题是:它们之间的主要区别是什么？类型系统在两者中是否同样具有表现力？能够进行全面的比较和关于利益的讨论会很棒.

我已经能够发现一些:

• Idris有类型类la Haskell,而Agda有实例参数
• 伊德里斯包括monadic和applicative符号
• 它们似乎都有某种可重新绑定的语法,虽然不确定它们是否相同.

---

编辑:此问题的Reddit页面中有更多答案:http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

Answer 1

我可能不是回答这个问题的最佳人选,因为实施伊德里斯我可能有点偏颇!常见问题解答 - http://docs.idris-lang.org/en/latest/faq/faq.html - 有话要说,但要稍微扩展一下:

Idris的设计是为了在定理证明之前支持通用编程,因此具有高级功能,如类型类,符号,成语括号,列表推导,重载等.Idris将高级编程放在交互式证明之前,尽管因为Idris建立在基于策略的阐述者之上,因此有一个基于策略的交互式定理证明器的接口(有点像Coq,但不是那么先进,至少还没有).

Idris旨在支持的另一件事是嵌入式DSL实现.使用Haskell,您可以通过符号获得很长的路径,并且您也可以使用Idris,但是如果需要,您还可以重新绑定其他构造,例如应用程序和变量绑定.您可以在教程中找到更多详细信息,或者在本文中找到完整的详细信息:http://www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf

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

Agda和Idris中的类型系统在许多重要方面非常相似.我认为主要区别在于宇宙的处理.阿格达具有宇宙多态性,伊德里斯具有累积性(Set : Set如果您发现这种限制性过于严重并且不介意您的证据可能不健全,那么您可以使用它们).

Answer 2

Idris和Agda之间的另一个区别是Idris的命题平等是异质的,而Agda是同质的.

换句话说,伊德里斯的平等假定定义是:

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

阿格达定义中的l可以被忽略,因为它与埃德温在他的答案中提到的宇宙多态性有关.

重要的区别在于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.这是异质平等的完美明智的陈述.