程序员从范畴论理解双函数-第8章

Question

我要背诵《程序员范畴论》第8章

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

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

这里，如果我对Haskell有一点了解的话，bf、fu和gu是类型构造函数，bf属于(* -> *) -> (* -> *) -> * -> * -> *类，fu和gu属于* -> *类(就像Maybe或[]一样)，而a和b是*类的一般类型;BiComp在=左边是一个类型构造函数，而右边的BiComp是一个值构造函数，所以它的类型是(bf (fu a) (gu b)) -> BiComp bf fu gu a b。

如果类型构造函数参数bf也是Bifunctor，并且类型构造函数fu和gu都是Functors，则将BiComp作为a和b的双分函数:

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:它被假设为在bf的Bifunctor实例中定义的类型，因此这个bimap具有类型(a -> a') -> (b -> b') -> bf a b -> bf a' b';我认为这没有下面的有趣，因为这毕竟只是8.1中Bifunctor类型class的bimap签名;
• 左边的bimap，是我们在第4和第5参数中定义的使BiComp成为Bifunctor的那个;参数f1和f2是作用于类型实体(即BiComp的第4和第5参数)的函数;因此，此bimap的类型为(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'

我们需要使用它来将类型为bf (fu a) (gu b)的输入值转换为类型为bf (fu a') (gu b')的输出值。我们可以这样做，只有当我们让c ~ fu a, c' ~ fu a', d ~ gu b, d' ~ gu b'。让我们看看这对我们的RHSbimap:

有什么影响

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得到我们需要的函数。同样，f2和fmap f2，一切都很顺利。