Bifunctors in Haskell vs in category theory

Question

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 ?

Answer 1

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.

Answer 2

Haskell Bifunctors are curried unlike category theory, that means that rather than being functors from a product category (FunctorOf (Prod (->) (->)) (->)) they are functors into a functor category (FunctorOf (->) (Nat (->) (->))).

This mirrors how functions from tuples ((a, b) -> c) are curried into functions into functions (a -> (b -> c)).

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

A product category Prod (->) (->) '(a, b) '(a', b') is not the same as ((a, b) -> (a', b')): it is the same as a tuple of functions (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')

That means the "uncurried Bifunctor" is

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

which doesn't fit any standard Haskell datatypes, since they are all curried.