haskell - Haskell 中的列表是归纳的还是归纳的？

Question

所以我最近一直在阅读关于共归纳的文章，现在我想知道: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 列表中得到了我期望的行为，即我可以制作有限和无限的结构。

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

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

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

如果我们定义data HList' a = L (List a) | R (Stream a)呢？ ?会考虑什么和/或仅对 HList 有用吗？ ?

Answer 1

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

“共归纳”并不意味着“必然无限”，它意味着“由解构方式定义”，而归纳意味着“由其构建方式定义”。我认为 this是对细微差别的极好解释。你肯定会同意这种类型
codata A : Type where MkA : A
不可能是无限的。

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