从程序员的范畴论中理解双函子 - Ch。 8个
Understanding of bifunctor from Category Theory for Programmers - 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，bf、fu 和 gu 是类型构造函数，bf (* -> *) -> (* -> *) -> * -> * -> *、fu 和 gu 属于 * -> *（就像 Maybe 或 []），而 a 和 b 是 kind * 的一般类型； BiComp 在=的左边是一个类型构造函数，写起来很长，而BiComp 右边是一个值构造函数，所以是(bf (fu a) (gu b)) -> BiComp bf fu gu a b.
类型
然后作者在a和b中使BiComp成为双函子，前提是类型构造函数参数bf也是Bifunctor，并且类型构造函数 fu 和 gu 是 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'；我认为这不如以下有趣，因为它毕竟只是 bimap 的 Bifunctor 类型 class 的签名，出现在 8.1;
- 左边的
bimap，相反，是我们定义的那个BiComp在它的第4和第5个参数中成为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的类型，就是我在上面bullet point写的那个，只不过是用a = fu a, a' = 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 得到我们需要的函数。同样 f2 和 fmap f2，一切都很好。
我要和 Chapter 8 from Category Theory for Programmers 在一起了。
在 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 是 kind * 的一般类型； BiComp 在=的左边是一个类型构造函数，写起来很长，而BiComp 右边是一个值构造函数，所以是(bf (fu a) (gu b)) -> BiComp bf fu gu a b.
然后作者在a和b中使BiComp成为双函子，前提是类型构造函数参数bf也是Bifunctor，并且类型构造函数 fu 和 gu 是 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'；我认为这不如以下有趣，因为它毕竟只是bimap的Bifunctor类型class的签名，出现在 8.1; - 左边的
bimap，相反，是我们定义的那个BiComp在它的第4和第5个参数中成为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的类型，就是我在上面bullet point写的那个，只不过是用a = fu a, a' = 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 得到我们需要的函数。同样 f2 和 fmap f2，一切都很好。