Agda 和 Idris 的区别

Posted 2023-02-25

【中文标题】Agda 和 Idris 的区别

【英文标题】：Differences between Agda and Idris

【发布时间】：2012-03-17 08:48:17

【问题描述】：

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

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

我已经发现了一些：

Idris 具有类似于 Haskell 的类型类，而 Agda 使用实例参数 Idris 包括一元符号和应用符号 它们似乎都有某种可重新绑定的语法，但不确定它们是否相同。

---

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

【问题讨论】：

你可能想看看 coq aswel，它的语法与 haskell 相差不到一百万英里，而且它有易于使用的类型类 :)

郑重声明：Agda 现在也有单子和应用符号。

【参考方案1】：

我可能不是回答这个问题的最佳人选，因为实施了 Idris 我可能有点偏颇！常见问题解答 - http://docs.idris-lang.org/en/latest/faq/faq.html - 有话要说，但要扩展一下：

Idris 的设计初衷就是在定理证明之前支持通用编程，因此具有高级功能，例如类型类、do notation、成语方括号、列表推导、重载等。 Idris 将高级编程置于交互式证明之前，尽管由于 Idris 建立在基于策略的详细说明器上，因此有一个基于策略的交互式定理证明器的接口（有点像 Coq，但不如 Coq 先进，至少目前还没有）。

Idris 旨在很好地支持的另一件事是嵌入式 DSL 实现。使用 Haskell，您可以使用 do 表示法，您也可以使用 Idris，但如果需要，您还可以重新绑定其他构造，例如应用程序和变量绑定。您可以在教程中找到更多详细信息，或在本文中找到完整详细信息：http://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf

另一个不同之处在于编译。 Agda 主要通过 Haskell，Idris 通过 C。Agda 有一个实验性后端，它使用与 Idris 相同的后端，通过 C。我不知道它的维护情况如何。 Idris 的主要目标始终是生成高效的代码 - 我们可以做得比目前更好，但我们正在努力。

Agda 和 Idris 中的类型系统在许多重要方面都非常相似。我认为主要区别在于对宇宙的处理。 Agda 具有全域多态性，Idris 具有 cumulativity（如果您觉得这太严格并且不介意您的证明可能不可靠，您可以同时使用 Set : Set）。

【讨论】：

你是什么意思，“......不是回答的最佳人......”？你是最适合回答的人之一，因为你非常了解伊德里斯。现在我们也只需要 NAD 来回复，我们已经掌握了全貌 :) 感谢您抽出宝贵时间回复。

有什么地方可以让我了解更多关于累积性的信息吗？我以前从未听说过...

Adam Chlipala's book 可能是最好的地方：

HoTT 书的第一章也描述得很清楚，如果简洁的话。

【参考方案2】：

Idris 和 Agda 的另一个区别是 Idris 的命题等式是异质的，而 Agda 的命题等式是同质的。

换句话说，Idris 中对平等的假定定义是：

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

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。这是一个具有异质性平等的完全明智的陈述。

【讨论】：

您对 Agda 标准库的评论似乎比 Agda 的基础理论更多，但即使是标准库也包含同构和异构相等 (cse.chalmers.se/~nad/listings/lib/…)。人们只是倾向于在可能的情况下更频繁地使用前者。后者相当于声明类型相等，然后是关于值的声明。在一个类型相等很奇怪（HoTT）的世界里，heteq 是一个更奇怪的声明。

我不明白这种说法在齐次平等下是多么无意义。除非我弄错了，(n + (m + o)) 和 ((n + m) + o) 在 ℕ 上的关联性判断上是相等的（源自归纳原理）。因此，等式的每一边确实具有相同的类型。相等类型之间的区别很重要，但我不明白这是一个例子。

@Abhishek 判断平等与定义平等不一样吗？我认为您的意思是说 (n + (m + o)) 和 ((n + m) + o) 在命题上相等，但在定义/判断上不相等。

正确。当我说判断平等时，我指的是命题平等。对不起。这是更正的评论： (n + (m + o)) 和 ((n + m) + o) 在命题上相等，但在定义上不相等。如果您有 a:A ，则 a:B 仅在 A 和 B 定义上相等的类型时才成立。对于类型检查的可判定性，定义相等性必须是可判定的。在外延类型理论中，定义相等与命题相等一致，因此类型检查是不可判定的。在 Coq 中，定义相等只包括计算、alpha 相等、定义展开。