在 Haskell 中，列表是归纳的还是余归纳的？

Question

最近我在阅读有关共归的内容，现在我想知道：Haskell中的列表是归纳的还是共归的？我也听说过Haskell不区分这两者，但如果是这样，他们如何在形式上区分呢？

列表是归纳定义的，data [a] = [] | a : [a]，但可以用于共归，ones = a:ones。我们可以创建无限的列表（coinductive reasoning）。然而，我们也可以创建有限的列表。那么它们是哪种呢？

类似的，在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是否不区分归纳类型和余归纳类型？如果是这样，那么它的正式化是什么？如果不是，那么哪一个是？

2. 是否有关于HList的余归纳性质？如果有，那么如何使余归纳类型包含有限值？

3. 如果我们定义了data HList' a = L (List a) | R (Stream a)，那会被认为是什么？相对于只有HList有什么用处？

- Crazycolorz5

---

Haskell没有归纳或余归纳类型的概念。（因为它是一种部分和惰性的语言，所以实际上并不需要这样的概念。）因此，询问给定的Haskell类型是否是归纳或余归纳类型并没有太多意义。 - Benjamin Hodgson

你的HList类型通常被称为共列表（co-list）。 - Cactus

Answer 1

由于Haskell的惰性特性，它的类型既具有归纳性也具有余归纳性，即数据与协作数据之间没有正式的区别。 所有递归类型都可以包含无限嵌套的构造函数。在诸如Idris，Coq，Agda等语言中，类似ones = 1：ones 的定义会被终止检查器拒绝。 惰性意味着ones可以在一步中计算出1：ones，而其他语言仅计算到正常形式，并且ones没有正常形式。

'余归纳'并不意味着'一定无限'，它意味着'根据如何分解来定义'，而归纳则意味着'根据如何构建来定义'。 我认为这篇文章很好地解释了微妙的差异。你肯定会同意以下类型： codata A : Type where MkA : A 不能是无限的。

与HList相反，您永远无法确定它是有限还是无限（具体而言，您可以在有限时间内发现列表是否有限，但无法计算其是否无限）。相比之下，HList'提供了一种简单的方法，在常数时间内判断列表是有限还是无限。

- user2407038

---

@gardenhead 在我看来，不是所有的 Haskell 类型都是“归纳和余归纳”的，而是 Haskell 既没有归纳类型也没有余归纳类型。你也不能像 Stream 那样表示余归纳类型。在我看来，这更多是部分性质而不是惰性导致的后果。 - Benjamin Hodgson

@BenjaminHodgson 部分性与 Stream 有什么关系？数据类型 type Stream = Nil | Cons nat * Stream 应该是惰性动态下无限流的类型。一个数据类型怎么可能是部分的？部分性只涉及函数。 - gardenhead

@gardenhead 请记住，对于 Haskell 作为逻辑系统的所有正式处理都依赖于假设，例如 undefined 不会发挥作用，也不会使用 seq。我说 [] 是归纳和余归纳列表，因为您可以编写与 Agda 或 Coq 中操作 both 归纳和余归纳列表的等效程序的 Haskell 列表。 - user2407038

如果您接受上述假设，您可以使用data Nat = Z | S !Nat（请注意严格性注释）来真正表示自然数，其中定义inf = S inf 不是生成的，更具体地说，它只相当于undefined。我想列表也是一样的：data FiniteList = Nil | Cons a !(FiniteList a) - 这使得像ones这样的东西非生成，并且您会得到有限的列表或底部。 - user2407038

你是在讨论一个真实存在的编程语言，还是一个具有神奇能力的理论语义，可以判断任意输入时函数是否停机？ - user2297560

Answer 2

在像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程序员习惯于非正式地推理程序的终止性/生产性。懒惰让我们可以处理无限的数据结构，但我们没有得到任何来自机器的帮助来确保我们的函数总是有结果的。

- Benjamin Hodgson

---

在Agda中，是否可以定义类似于HList的结构？如果是这样，是否仍然会施加生产力约束（因为它是codata），因此filter仍然无效？也就是说，Nil的引入不会影响其有效性吗？ - Crazycolorz5

没错。共归列表仍然可以是无限的（虽然不像流一样），因此 filter 仍将被拒绝，因为它对于所有输入都不会产生结果。 - Benjamin Hodgson

Answer 3

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

F X = (1 + A_bot * X)_bot

如果我们采用归纳推理，我们希望不动点是“最小的”。如果采用共归纳推理，“最大”的不动点会更合适。从技术上讲，这是通过在CPO_bot的嵌入-投影子范畴中工作来实现的，例如对于“最小”，取嵌入图的余极限。

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

将Kleene的不动点定理进行概括，对于“最大值”，我们会取投影图的极限。

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

然而，对于任何 F，“最小值”与“最大值”是同构的。这就是“双极限定理”（参见例如Abramsky的“域理论”调查论文）。

令人惊讶的是，归纳或余归纳的特点来自于F应用的升降操作，而不是最小/最大不动点。例如，如果x是粉碎积，#是粉碎和。

F X = 1_bot # (A_bot x X)

作为双重极限，其双极限集合为有限列表（直到同构为止）。

[我希望我理解了抬升 - 这些是棘手的 ;-)]

- chi