Co Finds a Pairing

This is a quick note to explain something which I've hinted at in some of my previous posts, namely that the Co construction from Edward Kmett's kan-extensions package can be used to construct a pairing "for free" for a given functor. In fact, it constructs the most specific pairing in a certain sense, as we'll see.

Pairings

First, a recap - a pairing between two functors f and g is a function which combines two functors full of values to return a single result:

type Pairing f g = forall a b. f (a -> b) -> g a -> b

Several functors can be usefully paired, such as

• Identity with Identity
• Tuple a with (->) a
• State s with Store s
• Writer w with Traced w
• Free f with Cofree g (assuming f and g can be paired)
• Product f1 g1 with Coproduct f2 g2 (assuming f1 and f1 pair, and g1 and g2 pair also)

Pairings are non-unique, since if I have a pairing between f and g, and a natural transformation h ~> f, then I can construct a pairing of h and g.

There is a trivial pairing between any f and Const Void:

boring :: forall f. Pairing f (Const Void)
boring _ (Const v) = absurd v

Pairings in terms of Day

It can be convenient to think of pairings in terms of Day convolution:

Pairing f g
= forall a b. f (a -> b) -> g a -> b
~ (exists a. (f (a -> b), g a)) -> b
~ Day f g b -> b
~ Day f g ~> Identity

So a pairing is simply a natural transformation from Day f g to the identity functor.

Day f has a right adjoint (f ⊸ -) which acts as the internal hom functor in the symmetric monoidal category with Day as its tensor.

So we also have:

Pairing f g
~ g ~> (f ⊸ Identity)
~ g ~> Co f

Thus, a pairing is a natural transformation from g to the functor f ⊸ Identity (which we might think of as "annihilating" f in the internal language of this symmetric monoidal category), which is isomorphic to Co f.

A category of pairings

Let's fix a functor f and construct a category of functors which pair with f.

An object in this category will be a functor g along with a natural transformation g ~> Co f (i.e. a pairing of f and g).

A morphism between g and h will be a natural transformation g ~> h such that the obvious diagram commutes. This captures the idea above that h is more specific than g, since they differ by a natural transformation.

It is hopefully obvious that id :: Co f ~> Co f is the terminal object in this category, so in this sense, Co f is the most specific functor which pairs with f.

You might ask - what about functors such as Maybe which have no obvious pairing? Well in this case, we recover the boring pairing above, so every "other" pairing factors through the boring one.

Putting this to use

How is this useful?

Well, for one, it can save us a step when working with pairings of free monads and cofree comonads, for example. Since Co has a lot of useful instances already, it is often not necessary to work with the paired functor explicitly.

I've also put this to use in my recent paper which summarizes the "comonads as spaces" work. In this case, it was convenient to frame user interfaces in terms of only a comonad, and to derive the corrsponding monad, instead of working with both.