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.
First, a recap - a pairing between two functors
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
gcan be paired)
Product f1 g1with
Coproduct f2 g2(assuming
Pairings are non-unique, since if I have a pairing between
g, and a natural transformation
h ~> f, then I can construct a pairing of
There is a trivial pairing between any
boring :: forall f. Pairing f (Const Void) boring _ (Const v) = absurd v
Pairings in terms of
It can be convenient to think of pairings in terms of
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
A category of pairings
Let's fix a functor
f and construct a category of functors which pair with
An object in this category will be a functor
g along with a natural transformation
g ~> Co f (i.e. a pairing of
A morphism between
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
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.