31

所以我最近一直在阅读关于共归纳法的文章，现在我想知道：Haskell 列表是归纳法还是归纳法？我也听说 Haskell 不区分这两者，但如果是这样，他们是如何正式区分的？

列表是归纳定义的，data [a] = [] | a : [a]，但可以互归纳地使用，ones = a:ones。我们可以创建无限列表。然而，我们可以创建有限列表。那么它们是什么？

相关是在 Idris 中，其中类型List a是严格的归纳类型，因此只是有限列表。它的定义类似于它在 Haskell 中的定义。但是，Stream a是一种互感类型，建模一个无限列表。它被定义为（或者更确切地说，定义等同于）codata Stream a = a :: (Stream a)。创建无限列表或有限流是不可能的。但是，当我写定义

codata HList : Type -> Type where
    Nil : HList a
    Cons : a -> HList a -> HList a

我从 Haskell 列表中得到了我期望的行为，即我可以制作有限和无限的结构。

所以让我把它们归结为几个核心问题：

  1. Haskell 不区分归纳类型和共归纳类型吗？如果是这样，那它的形式化是什么？如果不是，那么哪个是[a]？

  2. HList 是互感的吗？如果是这样，协约类型如何包含有限值？

  3. 如果我们定义了data HList' a = L (List a) | R (Stream a)呢？会考虑什么和/或它会比 just 有用HList吗？

4

3 回答 3

25

  1. 由于懒惰，Haskell 类型既是归纳的又是共归纳的，或者说，数据和余数据之间没有正式的区别。所有递归类型都可以包含无限嵌套的构造函数。在 Idris、Coq、Agda 等语言中，类似的定义ones = 1 : ones会被终止检查器拒绝。懒惰意味着ones可以一步计算到1 : ones，而其他语言仅计算为范式，并且ones没有范式。

  2. “共归纳”并不意味着“必然无限”，它意味着“由解构方式定义”，而归纳意味着“由其构建方式定义”。我认为这是对细微差别的一个很好的解释。你肯定会同意这种类型

    codata A : Type where MkA : A

    不可能是无限的。

  3. 这是一个有趣的问题 - 与 相比HList，您永远无法“知道”它是有限的还是无限的（具体来说，如果列表是有限的，您可以在有限的时间内发现，但您无法计算它是无限的），HList'为您提供了一种简单的方法来确定您的列表是有限的还是无限的。

于 2016-10-04T16:49:03.490 回答
19

在像 Coq 或 Agda 这样的整体语言中，归纳类型是那些值可以在有限时间内被拆除的类型。感应功能必须终止。另一方面，感应类型是那些值可以在有限时间内建立起来的类型。感应功能必须是生产性的。

旨在用作证明助手的系统（如 Coq 和 Agda）必须是完全的，因为不终止会导致系统在逻辑上不一致。但是要求所有函数都是全集的和归纳的，使得不可能处理无限的结构，因此，发明了共归纳法。

所以归纳和共归纳类型的目的是拒绝可能的非终止程序。这是 Agda 中的一个示例，该示例由于生产力条件而被拒绝。（您传递给的函数filter可能会拒绝每个元素，因此您可能会永远等待结果流的下一个元素。）

filter : {A : Set} -> (A -> Bool) -> Stream A -> Stream A
filter f xs with f (head xs)
... | true = head xs :: filter f (tail xs)
... | false = filter f (tail xs)  -- unguarded recursion

现在，Haskell 没有归纳或共归纳类型的概念。问题“这种类型是归纳的还是共归纳的？” 不是一个有意义的。Haskell 如何在不区分的情况下逃脱？好吧，Haskell 从一开始就从未打算将其作为一种逻辑保持一致。它是一种部分语言，这意味着您可以编写非终止和非生产性函数 - 没有终止检查器和生产力检查器。人们可以辩论这一设计决策的智慧，但它肯定会使归纳和共归纳变得多余。

相反，Haskell 程序员习惯于非正式地推理程序的终止/生产力。懒惰让我们可以使用无限的数据结构，但我们没有从机器那里得到任何帮助来确保我们的功能是完整的。

于 2016-10-04T17:04:35.437 回答
5

要解释类型级递归，需要为 CPO 值列表函子找到一个“固定点”

F X = (1 + A_bot * X)_bot

如果我们进行归纳推理，我们希望不动点是“最小的”。如果是共归纳的，“最大”。

从技术上讲，这是通过在 CPO_bot 的嵌入投影子类别中工作来完成的，例如，将嵌入图的 colimit 视为“最小”

0_bot |-> F 0_bot |-> F (F 0_bot) |-> ...

推广 Kleene 不动点定理。对于“最大”，我们将采用投影图的限制

0_bot <-| F 0_bot <-| F (F 0_bot) <-| ...

然而事实证明，对于任何F. 这是“bilimit”定理（参见例如 Abramsky 的“Domain Theory”调查论文）。

也许令人惊讶的是，归纳或共归纳的味道来自于应用的提升，F而不是最小/最大固定点。例如，如果x是粉碎产品并且#是粉碎总和，

F X = 1_bot # (A_bot x X)

将有限列表集（直到iso）作为bilimit。

[我希望我做对了——这些很棘手；-)]

于 2016-10-04T17:05:58.227 回答