haskell - 在编程的上下文中什么构成了 codata？

Question

这是一个核心递归算法，因为每次迭代它都会调用比之前更大的数据：

iterate f x =  x : iterate f (f x)

它类似于尾递归累加器样式，但它的累加器是隐式的，而不是作为参数传递。如果不是因为懒惰，它将是无限的。那么 codata 是否只是 WHNF 中的值构造函数的结果，有点像(a, thunk)？或者 codata 是范畴论中的一个数学术语，在编程领域没有有用的表示？

后续问题：值递归只是核心递归的同义词吗？

score 4 · Accepted Answer

我认为回答你的问题需要很多解释，所以这里有一个很长的答案，最后是你问题的具体答案。

数据和余数据在范畴论方面具有正式的数学定义，因此这不仅仅是它们在程序中的使用方式（即，不仅仅是您在评论中提到的“应用程序上下文”）。在 Haskell 中可能看起来是这样，因为语言的特性（特别是非终止和惰性）最终模糊了区别，所以在 Haskell 中，所有数据也是 codata ，反之亦然，但不一定是这样，并且有些语言可以使区分更加清晰。

data 和 codata在编程领域都有有用的表示，并且这些表示产生了与递归和核心递归的自然关系。

如果不快速掌握技术知识，很难解释这些正式的定义和表示，但粗略地说，一个数据类型，比如整数列表，是一个L带有构造函数的类型：

makeL :: Either () (Int, L) -> L

这在某种程度上是“普遍的”，因为它可以完全代表任何这样的结构。（在这里，您想将 LHS 类型解释Either () (Int, L)为表示一个列表L是空列表Left ()或Right (h, t)由头元素h :: Int和尾列表组成的对t :: L。）

从一个反例开始，L = Bool不是我们正在寻找的数据类型，因为即使您可以编写：

foo :: Either () (Int, Bool) -> Bool
foo (Left ()) = False
foo (Right (h, t)) = True

“构造” a Bool，这不能完全代表任何这样的构造。例如，两种结构：

foo (Right (1, foo (Left ()))) = True
foo (Right (2, foo (Left ()))) = True

给出相同的Bool值，即使它们使用不同的整数，所以这个Bool值不足以完全表示构造。

相反，该类型[Int] 是合适的数据类型，因为（几乎是微不足道的）构造函数：

makeL :: Either () (Int, [Int]) -> [Int]
makeL (Left ()) = []
makeL (Right (h, t)) = h : t

完全代表任何可能的构造，为每个构造创造独特的价值。因此，它在某种程度上是类型签名的“自然”构造Either () (Int, L) -> L。

类似地，整数列表的余数据类型将是一个L带有析构函数的类型：

eatL :: L -> Either () (Int, L)

这在某种程度上是“普遍的”，因为它可以代表任何可能的破坏。

同样，从一个反例开始，一对(Int, Int)不是我们正在寻找的余数据类型。例如，使用析构函数：

eatL :: (Int, Int) -> Either () (Int, (Int, Int))
eatL (a, b) = Right (a, (b, a))

我们可以表示破坏：

let p0 = (1, 2)
    Right (1, p1) = eatL p0
    Right (2, p2) = eatL p1
    Right (1, p3) = eatL p2
    Right (2, p4) = eatL p3
...continue indefinitely or stop whenever you want...

但我们不能代表破坏：

let p0 = (?, ?)
    Right (1, p1) = eatL p0
    Right (2, p2) = eatL p1
    Right (3, p3) = eatL p2
    Left () = eatL p3

另一方面，在 Haskell 中，列表类型[Int]是整数列表的合适余数据类型，因为析构函数：

eatL :: [Int] -> Either () (Int, [Int])
eatL (x:xs) = Right (x, xs)
eatL [] = Left ()

可以表示任何可能的破坏（包括有限或无限破坏，这要归功于 Haskell 的惰性列表）。

（作为证据表明这并不全是挥手，如果你想把它与形式数学联系起来，在技术范畴理论术语中，上面相当于说类似列表的内函子：

F(A) = 1 + Int*A   -- RHS equivalent to "Either () (Int,A)"

产生了一个类别，其对象是构造函数（AKA F-algebras）1 + Int*A -> A。与 F 相关的数据类型是该类别中的初始 F 代数。F 还产生了另一个类别，其对象是析构函数（AKA F-coalgebras）A -> 1 + Int*A。与 F 相关的余数据类型是该类别中的最终 F-余代数。）

直观地说，正如@DanielWagner 所建议的那样，数据类型是表示类列表对象的任何构造的一种方式，而余数据类型是表示类列表对象的任何破坏的一种方式。在 data 和 codata 不同的语言中，有一个基本的不对称性——终止程序只能构造一个有限列表，但它可以破坏（第一部分）一个无限列表，因此 data 必须是有限的，但 codata 可以是有限的或无限。

这导致了另一个并发症。在 Haskell 中，我们可以makeL像这样构造一个无限列表：

myInfiniteList = let t = makeL (Right (1, t)) in t

请注意，如果 Haskell 不允许对非终止程序进行惰性求值，则这是不可能的。因为我们可以做到这一点，根据“数据”的正式定义，Haskell 整数列表数据类型也必须包含无限列表！也就是说，Haskell“数据”可以是无限的。

这可能与您可能在其他地方读到的内容相冲突（甚至与@DanielWagner 提供的直觉相冲突），其中“数据”仅用于指代有限的数据结构。好吧，因为 Haskell 有点奇怪，而且因为在数据和余数据不同的其他语言中不允许无限数据，所以当人们谈论“数据”和“余数据”（即使在 Haskell 中）并有兴趣区分时，他们可能只使用“数据”来指代有限结构。

递归和核心递归适应这一点的方式是，普遍性属性自然地给了我们“递归”来消费数据和“核心递归”来产生 codata。IfL是具有构造函数的整数列表数据类型：

makeL :: Either () (Int, L) -> L

那么使用列表L生成 a 的一种方法Result是定义一个（非递归）函数：

makeResult :: Either () (Int, Result) -> Result

这里，makeResult (Left ())给出一个空列表的预期结果，而makeResult (Right (h, t_result))给出一个列表的预期结果，该列表的头元素是h :: Int并且其尾部将给出结果t_result :: Result。

通过普遍性（即，它是一个初始 F 代数的事实makeL），存在一个process :: L -> Result“实现”的独特函数makeResult。在实践中，它将递归地实现：

process :: [Int] -> Result
process [] = makeResult (Left ())
process (h:t) = makeResult (Right (h, process t))

相反，如果L是具有析构函数的整数列表余数据类型：

eatL :: L -> Either () (Int, L)

那么从 a 生成列表L的一种方法Seed是定义一个（非递归）函数：

unfoldSeed :: Seed -> Either () (Int, Seed)

在这里，unfoldSeed应该Right (x, nextSeed)为每个所需的整数产生一个，并产生Left ()终止列表。

通过普遍性（即，eatL最终的 F-coalebra 的事实），存在generate :: Seed -> L“实现”的独特功能unfoldSeed。在实践中，它将以核心递归方式实现：

generate :: Seed -> [Int]
generate s = case unfoldSeed s of
  Left () -> []
  Right (x, s') -> x : generate s'

因此，综上所述，以下是您最初问题的答案：

从技术上讲，iterate f它是核心递归的，因为它是实现以下功能的独特的生成代码的函数Int -> [Int]：
```
unfoldSeed :: Seed -> Either () (Int, Seed)
unfoldSeed x = Right (x, f x)
```
通过generate上述定义。
在 Haskell 中，产生类型 codata 的 corecursion[a]依赖于惰性。然而，严格的尾数据表示是可能的。例如，以下 codata 表示在 Strict Haskell 中可以正常工作，并且可以安全地进行全面评估。
```
data CoList = End | CoList Int (() -> CoList)
```
下面的 corecursive 函数产生一个CoList值（我把它设为有限只是为了好玩——它也很容易产生无限的 codata 值）：
```
countDown :: Int -> CoList
countDown n | n > 0 = CoList n (\() -> countDown (n-1))
            | otherwise = End
```
所以，不，codata 不仅仅是 WHNF 中具有形式(a, thunk)或类似形式的值的结果，并且 corecursion 不是值递归的同义词。但是，WHNF 和 thunk 提供了一种可能的实现，并且是实现级别的原因，即“标准”Haskell 列表数据类型也是余数据类型。

haskell - 在编程的上下文中什么构成了 codata？

1 回答 1

Related

Reference