在 Haskell 中，列表是归纳的还是余归纳的？
最近我在阅读有关共归的内容，现在我想知道：Haskell中的列表是归纳的还是共归的？我也听说过Haskell不区分这两者，但如果是这样，他们如何在形式上区分呢？ 列表是归纳定义的，data [a] = [] | a : [a]，但可以用于共归，ones = a:ones。我们可以创建无限的列...
如何高效地将归纳类型转换为非递归的余归纳类型？（无需使用递归）
> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-} 任何归纳类型的定义如下所示 > newtype Ind f = Ind {flipinduct :: forall r. (f r ...
编码数据类型真的是终端代数吗？
（免责声明：我不完全确定codatatype的工作原理，特别是当它不涉及终端代数时。） 考虑“类型范畴”，类似于Hask，但具有适合讨论的任何调整。在这样的范畴中，据说（1）初始代数定义数据类型，而（2）终端代数定义codatatype。 我正在努力说服自己（2）是正确的。 考虑函子T（...
如何在Haskell中定义常数异构流？
我了解如何在Haskell中定义同质和异质流。 -- Type-invariant streams. data InvStream a where (:::) :: a -> InvStream a -> InvStream a -- Heterogeneous Stre...
理解Agda的协同归纳有困难
我正在尝试为IMP语言编写功能语义，其中包括并行抢占调度，如以下论文第4节所述。 我正在使用Agda 2.5.2和标准库0.13。此外，整个代码可在以下gist中找到。 首先，我已定义了该语言的语法为归纳类型。 data Exp (n : ℕ) : Set where $_ ...
一个由无限个1组成的列表是否合理？
在Prolog中，将变量X与列表[1|X]统一是获取一个无限个1的列表的正常方法吗？SWI-Prolog没有任何问题，但GNU Prolog会导致程序挂起。 我知道在大多数情况下，我可以用以下代码替换列表： one(1). one(X) :- one(X). 但我的问题明确地是，是否可...