haskell - Haskell 中 Zap Functor 和 zap 函数的目的是什么？

Question

我遇到了this construction在 haskell 。我找不到有关如何使用 zap 的任何示例或解释/zapWith和 bizap/bizapWith在实际代码中。它们是否与标准 zip 有某种关联？/zipWith职能？我如何使用 Zap/Bizap Haskell 代码中的仿函数？它们有什么好处？

Answer 1

这篇精彩的 Kmett 博客文章涵盖了这一点，Cofree Comonad and the Expression Problem .不幸的是，那篇博文中有很多术语，我自己也不太了解所有内容，但我们可以尝试勾勒出细节。

皮亚诺号码

让我们以一种非常奇怪的方式定义自然数。我们将首先定义 Peano 零和后继函数:

zero :: ()
zero = ()

incr :: a -> Identity a
incr = Identity

然后我们可以定义一些数字:

one :: Identity ()
one = incr zero

two :: Identity (Identity ())
two = incr . incr $ zero

three :: Identity (Identity (Identity ()))
three = incr . incr . incr $ zero

奇怪，但它似乎有效。您可以转换 3 :: Int至 three然后回来。 (试试看。)我们可以写一个函数 f吗？将任意数字转换为我们奇怪的表示并返回？抱歉不行。 Haskell 类型系统不会让我们构造无限类型，而这正是我们想要的类型 f .

一个更大的问题是，作为一个懒惰的函数式程序员，我希望停止输入 Identity很多次。按照这个速度，我将被迫输入 O(n^2) 次来定义 n 个数字。这是 2016 年，我觉得这是 Not Acceptable 。

我们可以求助于 Free 数据类型来解决我们的两个问题。 (有些人称其为 Free monad，但是当我们只能说“type”时，我们没有理由说“monad”。)

newtype Free f a = Free (Either a (f (Free f a)))

zero :: a -> Free Identity a
zero x = Free (Left x)

incr :: Free Identity a -> Free Identity a
incr = Free . Right . Identity

one :: a -> Free Identity a
one x = incr (zero x)

two :: a -> Free Identity a
two x = incr (incr (zero x))

three :: a -> Free Identity a
three = incr . incr . incr . zero

漂亮。这(可能令人惊讶)与我们不寻常的 Identity 相同- 上面的包装表示。

流

现在让我们尝试构建一个流。比如说，从 2000 年(2000 年、2400 年、2800 年)开始的世纪闰年流。但以一种奇怪的方式。

unfold :: (a -> a) -> a -> (a, (a, (a, ...)))
unfold a2a a = (a, unfold a2a (a2a a))

centurials :: (Int, (Int, (Int, ...)))
centurials = unfold (+ 400) 2000

假设编译器允许我们写下无限类型，这将是数字流的合适表示。 Cofree 来救援，它是 Free 的“双重”类型。在范畴理论意义上是双重的，如果你花时间拿出一本范畴论教科书，煮了很多咖啡，画出范畴图，然后翻转所有的箭头，你会从一个到另一个(或另一个)。这个糟糕的解释将足以作为关于二元性的手波段落。

newtype Cofree f a = Cofree (a, f (Cofree f a))

unfold :: Functor f => (a -> f a) -> a -> Cofree f a
unfold a2fa a = Cofree (a, fmap (unfold a2fa) (a2fa a))

centurials :: Cofree Identity Int
centurials = unfold (Identity . (+ 400)) 2000

这(可能再次令人惊讶)相当于我们上面无限的俄罗斯嵌套娃娃表示。

使用 Peano 数字索引流

但是如何寻找流中的特定元素呢？通过利用 Free 和 Cofree 之间的二元性，我们实际上可以使用我们的 Peano 数表示来索引我们的流表示。

事实证明，在 Haskell 中，如果 f和 g在数学意义上是对偶的，那么以下性质成立:

class Zap f g | f -> g, g -> f where
  zap :: (a -> b -> r) -> f a -> g b -> r

我们将不得不省略关于对偶性以及为什么这个性质适用于对偶仿函数的讨论。

我们可以实现最简单的实例:恒等仿函数(在 Haskell 中表示为 newtype Identity a = Identity a)与其自身之间的数学对偶性。

instance Zap Identity Identity where
  zap ab2r (Identity a) (Identity b) = ab2r a b

此属性也可以扩展到双仿函数:

class Bizap f g | f -> g, g -> f where
  bizap :: (a -> c -> r) -> (b -> d -> r) -> f a b -> g c d -> r

我们可以为 Haskell 的 sum 和 product 编码实例化这个类，它们在范畴论中是(非平凡的!)对偶的:

instance Bizap Either (,) where
  bizap ac2r bd2r (Left a) (c, d) = ac2r a c
  bizap ac2r bd2r (Right b) (c, d) = bd2r b d

instance Bizap (,) Either where
  bizap ac2r bd2r (a, b) (Left c) = ac2r a c
  bizap ac2r bd2r (a, b) (Right d) = bd2r b d

我们现在有足够的机制来展示 Haskell 中 Free 和 Cofree 之间相同的二元性。

instance Zap f g => Zap (Cofree f) (Free g) where
  zap ab2r (Cofree as) (Free bs) = bizap ab2r (zap (zap ab2r)) as bs

instance Zap f g => Zap (Free f) (Cofree g) where
  zap ab2r (Free as) (Cofree bs) = bizap ab2r (zap (zap ab2r)) as bs

这些实例利用了Either 和(,) 的双重二元仿函数性质以及继承的 zap来自 f的对偶性和 g ，在我们的例子中总是 Identity和 Identity为了“剥离”一层 Free和 Cofree并递归调用 zap在那个下层。

最后，让我们看看它的实际效果:

year2800 :: Int
year2800 = zap id (two id) centurials

正是通过利用这种 zap 或“湮灭”属性，我们能够使用 Free 构建的自然数索引从 Cofree 构建的流中检索值。尽管与真实世界的示例相去甚远，但该代码作为练习存在，用于说明我们如何在 Haskell 类型和类型类中编码来自类别理论的高度错误的想法。我们能够做到这一点可以作为一个脑筋急转弯，也是对我们选择的 Free 和 Cofree 类型的理智检查。

您可能会发现这些实例对单行代码很有用，或者当您的数据结构恰好对齐时，如 Gurkenglas 的回答中所述。如果您发现对偶性是一个有用的属性，请务必使用 category-extras 包的这一部分。但是，即使我们找不到它的用法，我们当然也可以欣赏到一切巧妙地组合在一起的美。

至于 zipper

You are correct in thinking that there is a connection between Zap and Zip .它们以文字游戏驱动开发的 Kmett 风格命名。编码可压缩的仿函数会导致非常相似的类型类 Zip :

class Functor f => Zip f where
  fzipWith :: (a -> b -> c) -> f a -> f b -> f c

您可以通过遵循此构造为树和流派生通用压缩函数(再次使用 Cofree)。有关更多详细信息，请参阅博客文章。