Agda和Idris的区别

我开始深入依赖types编程,并发现Agda和Idris语言是最接近Haskell,所以我开始在那里。

我的问题是:他们之间的主要区别是什么? 这两种types的系统是否同样expression? 对收益进行全面的比较和讨论是非常好的。

我已经能够发现一些:

  • Idris的Haskelltypes类,而Agda带有实例参数
  • 伊德里斯包括一元和适用的符号
  • 他们两个似乎都有某种可重新expression的语法,虽然不太确定它们是否相同。

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

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

伊德里斯从头开始被devise为在定理certificate之前支持通用编程,因此具有types类,符号,成语括号,列表parsing,重载等高级特征。 伊德里斯把高层次的编程放在交互式certificate之前,尽pipe因为伊德里斯是build立在基于策略的阐释者之上的,所以存在一个基于策略的交互式定理certificate者(有点像Coq,但不像先进的,至less还没有)的接口。

embedded式DSL实现还有另一件事Idris的目标是支持。 有了Haskell,你可以用符号表示很长的路,而且你也可以用Idris,但是如果需要的话,你也可以重新绑定其他的结构,比如应用程序和variables绑定。 你可以在本教程中find更多的细节,或者在本文中查看完整的细节: http : //www.cs.st-andrews.ac.uk/~eb/drafts/dsl-idris.pdf

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

Agda和Idris的types系统在许多重要方面都非常相似。 我认为主要的区别在于宇宙的处理。 Agda拥有宇宙多态性,Idris具有累积性(如果你觉得这个限制太大,你可以Set : Set ,不要介意你的certificate可能不合适)。

伊德里斯和阿格达之间的另一个区别是,伊德里斯的命题平等是异质的,而阿格达是同质的。

换句话说,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中的相等types将A的两个元素作为参数,而在Idris中它可以取两个具有不同types的值。

换句话说,在伊德里斯,人们可以说,两种不同types的东西是平等的(即使它最终是一个无法certificate的主张),而在阿格达,这种说法是无稽之谈。

这对types理论具有重要而广泛的影响,特别是关于同伦types理论的可行性。 为此,异类平等不会起作用,因为它需要一个与HoTT不一致的公理。 另一方面,有可能陈述有用的定理,不可能用均匀的平等直接表示。

也许最简单的例子是vector连接的关联性。 给定由此定义的长度索引列表:

 data Vect : Nat -> Type -> Type where Nil : Vect 0 a (::) : a -> Vect na -> Vect (S n) a 

并与以下types连接:

 (++) : Vect na -> Vect ma -> Vect (n + m) a 

我们可能想要certificate:

 concatAssoc : (xs : Vect na) -> (ys : Vect ma) -> (zs : Vect oa) -> xs ++ (ys ++ zs) = (xs ++ ys) ++ zs 

因为等式的左边有Vect (n + (m + o)) atypes,右边的types为Vect ((n + m) + o) a ,所以这种说法在同质平等下是无意义Vect ((n + m) + o) a 。 这是一个非常明智的声明与异质平等。

Interesting Posts