Haskell与范畴论中的双函子

dffbzjpn  于 2023-11-18  发布在  其他
关注(0)|答案(2)|浏览(114)

在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类中,可以得到 * 一些 * 双函子,即第一个和第二个参数的类型不相互作用的双函子,但不是所有双函子。实际上,我甚至可以说Bifunctor类实现了两个函子的 * 乘积 *,而不是双函子。
所以我的问题是:我误解了什么吗?或者Haskell中的双函子不是真正的双函子?类MyBifunctor有意义吗?

aydmsdu9

aydmsdu91#

你的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, -),它将对象dMap到B(c, d),将箭头f : d1 -> d2Map到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中没有简单的方法来表达这个约束。

niwlg2el

niwlg2el2#

与范畴论不同,Haskell双函子是curried的,这意味着它们不是来自乘积范畴(FunctorOf (Prod (->) (->)) (->))的函子,而是进入函子范畴(FunctorOf (->) (Nat (->) (->)))的函子。
这反映了元组((a, b) -> c)中的函数如何被curry到函数中(a -> (b -> c))。

Prod (->) (->)  (->)
                   |               |
                   vvvvvvvvvvvv    vvvv
UncurriedEither :: (Type, Type) -> Type
(Curried)Either :: Type -> Type -> Type
                   ^^^^    ^^^^^^^^^^^^
                   |       |
                   (->)    Nat (->) (->)

字符串
产品类别Prod (->) (->) '(a, b) '(a', b')((a, b) -> (a', b')) * 不 * 相同:它与函数(a -> a', b -> b')的元组相同。

type Prod :: Cat k -> Cat j -> Cat (k, j)
data Prod cat1 cat2 pair pair' where
  Prod :: cat1 a a'
       -> cat2 b b'
       -> Prod cat1 cat2 '(a, b) '(a', b')


这意味着“未加咖喱的双函子”是

type  UncurriedBifunctor :: ((Type, Type) -> Type) -> Constraint
class UncurriedBifunctor bi where
  bimap :: (a -> a', b -> b') -> bi '(a, b) -> bi '(a', b')


它不适合任何标准的Haskell数据库,因为它们都是curry的。

相关问题