haskell - 在编程环境中什么构成协同数据？

Question

这是一种核心递归算法，因为在每次迭代时，它都会调用比以前更大的数据:

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

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

后续问题:值(value)递归仅仅是corecursion的同义词吗？

Answer 1

我认为回答您的问题需要大量解释，因此这是一个很长的答案，最后附有您问题的具体答案。

数据和协数据在类别理论方面具有形式化的数学定义，因此，这不仅关乎它们在程序中的使用方式(即，不仅是您在注释中提到的“应用程序上下文”)。在Haskell中似乎是这种方式，因为该语言的功能(特别是非终止性和惰性)最终使两者之间的区别变得模糊，因此在Haskell中，所有数据也是codata，反之亦然，但这不是必须的，并且有一些语言使区别更加清晰。

数据和协数据在编程领域都具有有用的表示形式，这些表示形式与递归和corecursion形成了自然的关系。

在不迅速掌握技术的情况下，很难解释这些形式化的定义和表示形式，但是大致来说，用于整数列表的数据类型是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

来“构造”一个​​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

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

类似地，整数列表的协数据类型将是L类型以及析构函数:

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

从某种意义上讲，它可以表示任何可能的破坏，因此在某种程度上是“通用的”。

同样，从一个反例开始，对(Int, Int)不是我们要查找的codata类型。例如，使用析构函数:

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的惰性列表，包括有限破坏或无限破坏)。

(作为证明，这并非全部都是挥手的，并且如果您想将其与形式数学联系起来，用技术范畴理论的术语来说，以上等同于说出类似列表的endofunctor:

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

产生一个类别，其对象是构造函数(AKA F-代数)1 + Int*A -> A。与F相关的数据类型是该类别中的初始F代数。 F还引起了另一类对象，该类的对象是析构函数(AKA F-coalgebras)A -> 1 + Int*A。与F相关联的协同数据类型是此类别中的最终F-coalgebra。)

用@DanielWagner的直觉来讲，数据类型是表示列表对象的任何构造的一种方式，而codata类型是表示列表对象的任何破坏的一种方式。在数据和共数据不同的语言中，存在一个基本的不对称性-终止程序只能构造一个有限列表，但它可以破坏无限列表(的第一部分)，因此数据必须是有限的，但协数据可以是有限的或无限。

这导致了另一种复杂性。在Haskell中，我们可以使用makeL构造一个无限列表，如下所示:

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

请注意，如果Haskell不允许对非终止程序进行延迟评估，则这将是不可能的。因为我们可以做到这一点，所以通过“数据”的正式定义，Haskell整数列表数据类型还必须包括无限列表!也就是说，Haskell的“数据”可以是无限的。

这可能与您在其他地方阅读的内容(甚至与@DanielWagner提供的直觉)相冲突，其中“数据”仅用于表示有限的数据结构。好吧，因为Haskell有点怪异，并且因为在其他数据和协数据不同的语言中不允许无限数据，所以当人们谈论“数据”和“codata”时(甚至在Haskell中)并且对区分有兴趣，他们可以使用“数据”仅指有限的结构。

递归和核心递归适用于此的方式是，通用性自然使我们可以使用“递归”来消耗数据，而使用“corecursion”来产生协数据。如果L是具有构造函数的整数列表数据类型:

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

然后，使用列表L生成Result的一种方法是定义一个(非递归)函数:

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

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

通过通用性(即makeL是初始F代数的事实)，存在一个独特的process :: L -> Result函数，可以“实现” makeResult。实际上，它将以递归方式实现:

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

相反，如果L是具有析构函数的整数协数据类型:

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

那么从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中，生成[a]类型的codata的corecursion依赖于惰性。但是，严格的协同数据表示是可能的。例如，以下协同数据表示形式在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列表数据类型也是协数据类型的实现级别的原因。