In Haskell, the class Bifunctor
is 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 ?
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.