Haskell中的列表是归纳的还是归纳的？
Haskell中的列表是归纳的还是归纳的？
提问于 2016-10-04 14:09:10
所以我最近读了一些关于共归纳的文章，现在我想知道: 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没有区分归纳和共归纳类型吗？如果是的话，它的形式化是什么？如果不是，那么哪一个是
- HList是共诱导的吗？如果是这样的话，协归纳类型怎么能包含有限值呢？
- 那么如果我们定义了
data HList' a = L (List a) | R (Stream a)呢？那会考虑什么和/或它对HList有用吗？
Stack Overflow用户
回答已采纳
发布于 2016-10-04 16:49:03
- 由于懒惰，Haskell类型分为归纳型和共归纳型，或者，数据和协数据之间没有正式的区别。所有递归类型都可以包含无限嵌套的构造函数。在诸如Idris、Coq、Agda等语言中，终止检查器拒绝像
ones = 1 : ones这样的定义。懒惰意味着ones可以在一个步骤中被计算到1 : ones，而其他语言只能计算为正常形式，而ones没有正常形式。 - “共归纳”并不意味着“必然是无限的”，它意味着“通过如何解构来定义它”，而作为归纳的意思是“由它的构造方式定义的”。我认为this是对细微差别的一个极好的解释。你肯定会同意那种
codata A : Type where MkA : A不可能是无限的。 - 这是一个有趣的问题--与
HList相反，你永远不可能“知道”它是有限的还是无限的(具体来说，如果列表是有限的，你可以在有限的时间内发现，但不能计算它是无限的)，HList'给出了一种简单的方法，可以在常数时间内确定列表是有限的还是无限的。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/39854514
复制相关文章
相似问题
腾讯云开发者
