A Simple Counter Example of Joint Functoriality

      2 mins

A bifunctor is a functor whose source is a product category. In Haskell, bifunctors have the bimap operation:

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

The laws for bimap are:

bimap id id = id
bimap (f . f') (g . g') = bimap f f' . bimap g g'

which are nothing but a reiteration of functoriality.

Bartosz Milewski, in one of his blog posts, mentioned that functoriality in each argument does not imply joint functoriality (i.e., the above bimap laws). However, he didn’t provide an example. Here I’m going to show a simple example that proves

  bimap (f . f') (g . g') = bimap f f' . bimap g g'
⤂
  bimap f (g . g') = bimap f g . bimap f g'  Λ
  bimap (f . f') g = bimap f g . bimap f' g

In words, bimap jointly preserving composition does not follow from preserving composition in each argument. Note that variables in all three equations above are universally quantified.

The Example

The example is in a category with a single object: a set of two elements {A, B}, and two arrows: the function id, and the function const A. Arrows are composed via regular function composition. Define bimap as

bimap f g = if f == id || g == id then id else const A

now, let f = g' = id and f' = g = const A. Then we have

bimap (f . f') (g . g') = bimap (const A) (const A) = const A
bimap f g . bimap f' g' = id . id = id

Therefore bimap does not jointly preserve composition, and so is not a bifunctor. However, bimap does preserve composition in each argument. Suppose we fix f:

  • If f = id: 
    bimap f (g . g') = id = bimap f g . bimap f g'
  • If f = const A, and at least one of g and g' is id (without loss of generality, suppose g = id): 
    bimap f (g . g') = bimap f g' = bimap f g . bimap f g'
  • If f = g = g' = const A: 
    bimap f (g . g') = bimap (const A) (const A) = const A = bimap f g . bimap f g'

This shows that bimap preserves composition in the second argument. By symmetry, it also preserves composition in the first argument.

Conclusion

A mapping from a product category to another category is not necessarily a bifunctor if it only preserves composition in each argument, since this does not imply preserving composition jointly.