Haskell 中的双函子与范畴论中的双函子

Question

在Haskell中，类

Bifunctor

定义如下：

class Bifunctor p where
  bimap :: (a -> b) -> (c -> d) -> p a c -> p b d

在范畴论中，根据 ncatlab，双函子是“一个定义域为产品类别的函子：对于 C1、C2 和 D 类别，函子 F:C1×C2⟶D 被称为来自 C1 的双函子，并且C2 到 D。”

现在，如果我必须实现分类定义，我会写以下内容：

class MyBifunctor p where
  myBimap :: ((a,c) -> (b,d)) -> p a c -> p b d

特别是，

myBimap

看起来很像

fmap

，我想这就是我们想要的，因为双函子是函子。

现在要进一步推动这一点，因为

base 4.18.0

，添加了量化约束：

class (forall a. Functor (p a)) => Bifunctor p where
    bimap :: (a -> b) -> (c -> d) -> p a c -> p b d

这个量化约束告诉我们，双函子是一个函子其第二个参数，这绝对与分类定义不匹配。

我知道，从

Bifunctor

类中，我们可以得到some双函子，即第一个和第二个参数的类型不相互作用的双函子，但不是所有。实际上，我什至会说类 Bifunctor

 实现了两个函子的 

product，而不是双函子。

所以我的问题如下：我是否误解了什么？或者 Haskell 中的双函子并不是真正的双函子？课程

MyBifunctor

有意义吗？

Answer 1

您的

MyBifunctor

不正确。产品类别中的态射不是对象对之间的态射（在广义分类环境中这意味着什么？），而是对象之间的态射对。比较：

((a,c) -> (b,d)) -> p a c -> p b d -- incorrect
(a -> b, c -> d) -> p a c -> p b d -- correct

正确的版本与基础库中的版本在道德上是同构的：

(a -> b) -> (c -> d) -> p a c -> p b d -- base, also correct

这个量化约束告诉我们，双函子是其第二个参数中的函子，这绝对与分类定义不匹配。

它实际上确实符合分类定义。给定一个双函子

B

 和第一个源类别 

c

 的对象 

C

，可以定义诱导操作 

F = B(c, -)

，它将对象 

d

 映射到 

B(c, d)

，将箭头 

f : d1 -> d2

 映射到 

B(id_c, f)

 。很容易验证 

F

 满足函子定律：

F(id_d) = B(id_c, id_d) = id_B(c,d) = id_F(d)
F(f) . F(g) = B(id_c, f) . B(id_c, g) = B(id_c . id_c, f . g) = B(id_c, f . g) = F(f . g)

在每种情况下，第二个等式都由双函子法则（或者如果您愿意的话，以产品类别作为源类别的函子法则）证明是合理的。几乎相同的论证表明

B(-,d)

 也是一个函子，但在 Haskell 中没有简单的方法来表达该约束。