阿格达与伊德里斯的区别

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

我的问题是: 它们之间的主要区别是什么？类型系统在两者中是否具有同样的表现力？如果能进行一次全面的比较和关于收益的讨论就太好了。

我发现了一些:

Idris 有类型类 la Haskell，而 Agda 有实例参数
伊德里斯包括一元符号和应用符号
它们似乎都有某种可重新绑定的语法，尽管不确定它们是否相同。

编辑 : 在这个问题的 Reddit 页面上有更多的答案: < a href = “ http://www.Reddit.com/r/depent _ types/comments/q8n2q/agda _ vs _ idris/”rel = “ norefrer”> http://www.Reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

24978

小开

伊德里斯与阿格达的另一个区别是，伊德里斯的命题相等是异质的，而阿格达的命题相等是同质的。

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

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 中，它可以接受两个具有潜在 与众不同类型的值。

换句话说，在伊德里斯，人们可以声称两种不同类型的东西是相等的(即使这最终是一个无法证明的说法) ，而在 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类型。这是一个具有异构相等性的非常合理的声明。