haskell - Traversable 和拉链。必要性和充分性

Question

每个类型T重载Traversable都会产生一个Zipper T。即实例 Traversable T的存在是Zipper T的充分条件。

有证据证明这也是必要条件吗？（我想它一定很琐碎，但到目前为止我还没有找到拉链的正式通用定义。）

Answer 1

每个 Traversable 函子都是一个容器，其中元素的位置有限。为了结合每个元素的计算效果，必须只有有限多个。因此，例如，无限Stream函子是不可遍历的，因为没有办法提供一个可靠的函数来Maybe通过。我们需要

sequence :: Stream (Maybe x) -> Maybe (Stream x)

但如果您想检查流中的所有内容是否成功，您将等待很长时间。

拉链对应于识别特定元素位置的能力（这进一步产生了与衍生品的联系，但这是另一回事）。为了能够将元素塞回其孔中，您需要一种有效的方法来确定位置是否相等。如果您只有有限多个职位，那肯定是正确的（在没有信息隐藏的情况下）。因此，对于拥有 Zipper 来说，Traversable 无疑是足够的。

然而，这不是必需的。Stream有一个非常明智的拉链

type StreamContext x = ([x], Stream x)
type StreamZipper x = (StreamContext x, x)

它将上下文表示为选定元素之前的有限（好的，好的，添加一个或两个）列表和它之后的无限流。

无限中的位置Stream是自然数。自然数有一个可判定的等式，但其中有无穷多个。

tl; 博士有限意味着可数，但反之亦然。