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

问题描述

我对 Chapter 8 from Category Theory for Programmers 有点神经质。

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

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

这里,如果我对 Haskell 有一些了解,bffugu 是类型构造函数bf 类型为 (* -> *) -> (* -> *) -> * -> * -> *,和 fugu * -> *(就像 Maybe[]),而 ab 是通用的种类*; BiComp = 的左边是一个类型构造器,很容易写,而 BiComp 右边是一个值构造器,所以它的类型是(bf (fu a) (gu b)) -> BiComp bf fu gu a b

然后作者在 BiCompa 中使 b 成为双函子,前提是类型构造函数参数 bf 也是 Bifunctor,并且类型构造函数 fuguFunctor

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 被假定为在任何类型构造函数 {{1} 的 Bifunctor 实例中定义} 确实如此,因此此 bf 的类型为 bimap;我认为这没有以下有趣,因为它毕竟只是 8.1 中呈现的 (a -> a') -> (b -> b') -> bf a b -> bf a' b' 类型bimapBifunctor 签名;
  • 左边的 class 是我们定义的,使 bimap 在其第 4 个和第 5 个参数中成为 BiComp;并且参数 Bifunctorf1 是必须作用于类型实体的函数,这些实体是 f2 的第 4 个和第 5 个参数;因此,此 BiComp 的类型为 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,{{1} } = fu a,依此类推。

我是否遗漏了什么(或想得太多了……)?

解决方法

你很接近。

首先,您的错误是 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' 才能做到这一点。让我们看看这对我们的 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 得到我们需要的函数。 f2fmap f2 也是如此,一切都很好。