Haskell中的列表是归纳还是诱导？

Question

所以我最近一直在阅读有关coinduction的内容,现在我想知道:Haskell列出了归纳还是共同？我也听说Haskell没有区分这两者,但如果是这样的话,他们怎么这样做呢？

列表是归纳定义的data [a] = [] | a : [a],但可以共同使用,ones = a:ones.我们可以创建无限列表.然而,我们可以创建有限列表.他们是哪一个？

相关的是Idris,其中类型List a严格地是归纳类型,因此仅是有限列表.它的定义类似于Haskell中的方式.然而,Stream a是一种共同类型,建模无限列表.它被定义为(或者更确切地说,定义相当于)codata Stream a = a :: (Stream a).创建无限List或有限Stream是不可能的.但是,当我写出定义时

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

我得到了我对Haskell列表的期望,即我可以创建有限和无限结构.

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

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

2. HList是coinductive吗？如果是这样,coinductive类型如何包含有限值？

3. 如果我们定义data HList' a = L (List a) | R (Stream a)怎么办？会考虑什么和/或仅对它有用HList？

Answer 1

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

2. "共同"并不意味着"必然是无限的",它意味着"由它如何被解构所定义",而"诱导意味着"由它如何构建来定义'.我认为这是对细微差别的一个很好的解释.当然你会同意这种类型

   codata A : Type where MkA : A

   不能无限.

3. 这是一个有趣的 - 相反HList,你可以永远'知道',如果它是有限的或无限的(具体来说,你可以在有限的时间发现一个列表是有限的,但你无法计算它是无限的),HList'为您提供一种简单的方法来确定您的列表是有限的还是无限的.

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程序员习惯于非正式地推理程序的终止/生产力.懒惰让我们可以使用无限的数据结构,但是我们没有得到机器的任何帮助来确保我们的功能是完整的.

Answer 3

要解释类型级递归,需要为CPO值列表仿函数找到"固定点"

F X = (1 + A_bot * X)_bot

如果我们以归纳的方式推理,我们希望固定点是"最小的".如果是coinductive,"最伟大".

从技术上讲,这是通过在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的"领域理论"调查论文).

也许令人惊讶的是,事实证明,归纳或共同引导的风味来自于应用F而不是最小/最大固定点.例如,如果x是破碎的产品并且#是破碎的总和,

F X = 1_bot # (A_bot x X)

将有限列表(最多为iso)作为一个bilimit.

[我希望我得到了正确的解决 - 这些都很棘手;-)]