Comonads and Day Convolution

Day Convolution

The Day convolution of two functors is another functor, defined as follows:

data Day f g a where
  Day :: (x -> y -> a) -> f x -> g y -> Day f g a

There is an implementation of Day in Edward Kmett's kan-extensions package on Hackage.

Day Convolution of Comonads

While writing my last post, I was looking for a way to combine comonads, and found out some interesting things about Day convolution in the process.

It turns out that there is a valid Comonad instance for Day f g whenever f and g are themselves Comonads:

instance Functor (Day f g) where
  fmap g (Day f x y) = Day (\a b -> g (f a b)) x y

instance (Comonad f, Comonad g) => Comonad (Day f g) where
  extract (Day f x y) = f (extract x) (extract y)
  duplicate (Day f x y) = Day (Day f) (duplicate x) (duplicate y)

That's interesting, but what's more interesting is that Day f is even a comonad transformer:

instance Comonad f => ComonadTrans (Day f) where
  lower (Day f x y) = fmap (f (extract x)) y

So for every comonad, we have a (symmetric) comonad transformer, for free!

These instances are now available in the kan-extensions package.

A Free Theorem

In order to prove the comonad laws, we'll need to apply a certain free theorem.

Consider how we might observe the state of a comonadic value of type Day f g. We would need a function f of type Day f g a -> r for some result type r. Now, this is isomorphic to:

f :: Day f g a -> r
   ~ (exists x y. (x -> y -> a, f x, g y) -> r
   ~ forall x y. (x -> y -> a) -> f x -> g y -> r

If we plug the type of f into the online free theorem generator, then we find out that its free theorem is (after some tidying):

f (\a b -> g (f1 a) (f2 b)) x y = f g (fmap f1 x) (fmap f2 y)

This theorem tells us that we can either apply a function in one of the functorial structures x or y, or defer it until the extraction function g. We won't be able to observe the difference, so we should consider these two values to be equal:

Day (\a b -> g (f1 a) (f2 b)) x y = Day g (fmap f1 x) (fmap f2 y)

This theorem will come in very useful soon.

Proving the Comonad Laws

The first comonad law states that

extract . duplicate = id

This one is simple to prove:

extract (duplicate (Day f x y))
  = extract (Day (Day f) (duplicate x) (duplicate y))
  = Day f (extract (duplicate x)) (extract (duplicate y))
  = Day f x y

The second comonad law states that

fmap extract . duplicate = id

This is slightly trickier, relying on the free theorem above:

fmap extract (duplicate (Day f x y))
  = fmap extract (Day (Day f) (duplicate x) (duplicate y))
  = Day (\a b -> extract (Day f a b)) (duplicate x) (duplicate y)
  = Day (\a b -> f (extract a) (extract b)) (duplicate x) (duplicate y)
  = Day f (fmap extract (duplicate x)) (fmap extract (duplicate y))
  = Day f x y

Notice how we use the free theorem in the fifth line, to move the extract from the first argument to the second and third arguments.

The final law states that

fmap duplicate . duplicate = duplicate . duplicate

Again, we'll need the free theorem:

duplicate (duplicate (Day f x y))
  = duplicate (Day (Day f) (duplicate x) (duplicate y))
  = Day (Day (Day f)) (duplicate (duplicate x)) (duplicate (duplicate y))
  = Day (Day (Day f)) (fmap duplicate (duplicate x)) (fmap duplicate (duplicate y))
  = Day (\a b -> duplicate (Day (Day f) a b)) (duplicate x) (duplicate y)
  = fmap duplicate (Day (Day f) (duplicate x) (duplicate y))
  = fmap duplicate (duplicate (Day f x y))

Success!

Now let's check the two ComonadTrans laws. The first says that

extract . lower = extract

This one is straightforward:

extract (lower (Day f x y))
= extract (fmap (f (extract x)) y)
= f (extract x) (extract y)
= extract (Day f x y)

The second ComonadTrans law states that

duplicate . lower = lower . fmap lower . duplicate

This one is a more involved application of the comonad laws of the base monad:

lower (fmap lower (duplicate (Day f x y)))
  = lower (fmap lower (Day (Day f) (duplicate x) (duplicate y)))
  = lower (Day (\a b -> lower (Day f a b)) (duplicate x) (duplicate y))
  = lower (Day (\a b -> fmap (f (extract a)) b) (duplicate x) (duplicate y))
  = fmap ((\a b -> fmap (f (extract a)) b) (extract (duplicate x)) (duplicate y)
  = fmap ((\a b -> fmap (f (extract a)) b) x) (duplicate y)
  = fmap (fmap (f (extract x))) (duplicate y)
  = duplicate (fmap (f (extract x)) y)
  = duplicate (lower (Day f x y))

That's it! Day f is a law-abiding comonad transformer for any Comonad f.

Comonad Optics

In fact, Day provides a symmetric monoidal product over the category of Haskell comonads. The unit of this product is the Identity functor.

kan-extensions defines the functions which provide this structure, but I won't cover the proof here.

In his video on monad transformer lenses, Edward Kmett makes a case for generalized profunctor lenses whenever we have a monoidal category. In the case of monads, the monoidal product was Compose. However, Compose is not symmetric, so we needed to separate left lenses from right lenses. However, in the case of comonads, we can use Day as our monoidal product, and Day is symmetric, making things a little simpler.

If we form the class of "strong" profunctors in the comonad category, we can derive a sensible notion of an optic which can focus on a component in a larger comonad which is isomorphic to a Day convolution of smaller comonads:

type (~>) f g = forall a. f a -> g a

class Profunctor p where
  dimap :: (f ~> g)
        -> (h ~> i)
        -> p i f
        -> p h g

class Convoluted p where
  convoluted :: (Comonad f, Comonad g, Comonad w)
             => p f g
             -> p (Day f w) (Day g w)

type Optic s t a b = Convoluted p => p a b -> p s t

Now for the interesting part: it turns out that many standard comonad transformers are already isomorphic to Day f for some f, so we can use these optics to easily operate inside comonad transformer stacks.

For example, consider StoreT:

data StoreT s w a = StoreT (s, w (s -> a))

Now, it turns out this is isomorphic to Day (Store s) as follows:

Day (Store s) w a
  ~ exists x y. (x -> y -> a, Store s x, w y)
  ~ exists x y. (x -> y -> a, s, s -> x, w y)
  ~ exists y. (s, s -> y -> a, w y)
  ~ exists y. (s, y -> s -> a, w y)
  ~ (s, w (s -> a))
  ~ StoreT s w a

Similarly, for EnvT:

Day (Env e) w a
  ~ exists x y. (x -> y -> a, Env e x, w y)
  ~ exists x y. (x -> y -> a, e, x, w y)
  ~ exists y. (y -> a, e, w y)
  ~ (e, w a)
  ~ EnvT e w a

And TracedT:

Day (Traced m) w a
  ~ exists x y. (x -> y -> a, Traced m x, w y)
  ~ exists x y. (x -> y -> a, m -> x, w y)
  ~ exists y. (m -> y -> a, w y)
  ~ w (m -> a)
  ~ TracedT m w a

So now we can write optics which focus on a Store inside a StoreT, or on the comonad transformed by StoreT, and similar optics for EnvT and TracedT.

I have a sketch of an implementation of these optics in PureScript.

It's not entirely clear to me what we can do with these optics just yet, but it seems like it should at least be possible to lift actions for the corresponding monads whenever we have a comonad optic which identifies one comonad as a Day convolution of a smaller comonad. I'm hoping this can be useful when using comonads to describe user interfaces.