haskellcategory-theorybifunctor

Bifunctors in Haskell vs in category theory


In Haskell, the class Bifunctoris defined as follow :

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

In category theory, a bifunctor is, according to ncatlab, "simply a functor whose domain is a product category : for C1, C2 and D categories, a functor F:C1×C2⟶D is called a bifunctor from C1 and C2 to D."

Now if I had to implement the categorical definition, I would write the following :

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

In particular, myBimap looks a lot like fmap, which is what I suppose we want since, again, a bifunctor is a functor.

Now to push this even further, since base 4.18.0, a quantified constraint has been added :

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

This quantified constraint tells us that a bifunctor is a functor in its second argument, which definitely doesn't match with the categorical definition.

I understand that from the class Bifunctor, one can get some bifunctors, the ones where the types of the first and second arguments do not interact, but not all of them. Actually, I'd even say that the class Bifunctor implements a product of two functors, and not a bifunctor at all.

So my question is the following : Did I misunderstood something ? Or are bifunctors in Haskell not really bifunctors ? Does the class MyBifunctor makes sense ?


Solution

  • Your MyBifunctor is incorrect. Morphisms in the product category are not morphisms between pairs of objects (what would that even mean, in the generalized categorical setting?), but rather pairs of morphisms between objects. Compare:

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

    The correct version is morally isomorphic to the version in the base library:

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

    This quantified constraint tells us that a bifunctor is a functor in its second argument, which definitely doesn't match with the categorical definition.

    It actually does match the categorical definition. Given a bifunctor B and an object c of the first source category C, the induced operation F = B(c, -) can be defined, which maps objects d to B(c, d) and arrows f : d1 -> d2 to B(id_c, f). It's pretty easy to verify that F satisfies the functor laws:

    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)
    

    In each case, the second equality is justified by the bifunctor laws (or the functor laws with the product category as the source category, if you prefer). An almost identical argument shows that B(-,d) is also a functor, but there's no easy way to express that constraint in Haskell.