从程序员的范畴论理解二元函子 - Ch。8

Question

我正在思考程序员类别理论的第 8 章。

在 8.3 节中，Bartosz 定义了这种类型

newtype BiComp bf fu gu a b = BiComp (bf (fu a) (gu b))

在这里，如果我对 Haskell 有一点了解，bf, fu, andgu是类型构造函数，bfof kind(* -> *) -> (* -> *) -> * -> * -> *和fuand guof kind * -> *（就像Maybeor一样[]），而a, andb是 kind 的一般类型*；BiComp 左边=是一个很长的类型构造器，而BiComp 右边是一个值构造器，所以它的类型是(bf (fu a) (gu b)) -> BiComp bf fu gu a b。

然后作者BiComp在aand 中做了一个双函子b，条件是类型构造函数参数bf也是 a Bifunctor，并且类型构造函数fuandgu是Functors：

instance (Bifunctor bf, Functor fu, Functor gu) => Bifunctor (BiComp bf fu gu) where
    bimap f1 f2 (BiComp x) = BiComp ((bimap (fmap f1) (fmap f2)) x)

到目前为止一切顺利，在这一点上对我来说一切似乎都是合理的。除了对类型构造函数和值构造函数使用相同的名称可能会让我迷失方向。

现在我很想做出以下观察：

• 在bimap上定义的右边是一个撬动的约束：它是bimap作为定义的假设Bifunctor的任何类型的构造器实例bf确实是，所以这个bimap有型(a -> a') -> (b -> b') -> bf a b -> bf a' b'; 我认为这没有以下有趣，因为它毕竟只是8.1中bimap提供的Bifunctor类型的签名class；
• 在bimap左侧，取而代之的，是我们定义使一个BiComp一个Bifunctor在第4和第5的参数; 以及必须作用于类型实体的参数f1和f2函数，这些实体是 的第 4 个和第 5 个参数BiComp；因此， thisbimap的类型是(a -> a') -> (b -> b') -> BiComp bf fu gu a b -> BiComp bf fu gu a' b'。

这样对吗？

如果是这样，那么我不明白以下内容

bimap :: (fu a -> fu a') -> (gu b -> gu b') -> bf (fu a) (gu b) -> bf (fu a') (gu b')

因为这是bimap右边的类型，就是我在上面的要点中写的，除了它是用a= fu a、a'=fu a'等等写的。

我是不是错过了什么（或想多了……）？

Answer 1

你很接近。

首先，你有那种bf错误。它实际上只是* -> * -> *，这正是预期的，因为它将是一个Bifunctor. 当然，那种BiComp是相当疯狂的：

BiComp :: (* -> * -> *) -> (* -> *) -> (* -> *) -> * -> * -> *

至于您的要点中的类型，从技术上讲，它们都是正确的，但是使用新的类型变量（特别是对于您的第一个要点中的类型！）可能有助于使这一切更加清晰。事实上，在bimap右手边有类型

bimap :: forall c c' d d'. (c -> c') -> (d -> d') -> bf c d -> bf c' d'

我们需要使用它来制作将我们的输入值转换为 typebf (fu a) (gu b)的输出值的东西bf (fu a') (gu b')。只有我们让c ~ fu a, c' ~ fu a', d ~ gu b, d' ~ gu b'. 让我们来看看这对我们的 RHS 做了什么bimap：

bimap :: (fu a -> fu a') -> (gu b -> gu b') -> bf (fu a) (gu b) -> bf (fu a') (gu b')

啊哈！这正是你在右手边发现的！而且，我们可以准确地提供我们需要的参数。首先，类型为 的函数fu a -> fu a'。好吧，我们有一个给定的函数f1 :: a -> a'，我们知道它fu是一个函子，所以我们可以用fmap f1. 同样使用f2and fmap f2，一切都很好。