Can you define `Comonads` based on `Monads`?

Question

Okay, so let's say you have the type

newtype Dual f a = Dual {dual :: forall r. f(a -> r)->r}

As it turns out, when f is a Comonad, Dual f is a Monad (fun exercise). Does it work the other way around?

You can define fmap ab (Dual da) = Dual $ \fb -> da $ fmap (. ab) fb and extract (Dual da) = da $ return id, but I do not know how to define duplicate or extend.

Is this even possible? If not, what the proof there is not (is there a particular Monad m for which you can prove Dual m is not a comonad)?

Some observations: Dual IO a is essentially Void (and Const Void is a valid Comonad). Dual m a for MonadPlus m is Void (just use dual mzero). Dual Reader is Env. Dual Writer is Traced. Dual State is Store, I think.

Answer 1

Yes, in fact any functor gives rise to a unique comonad in this way, unless f==0.

Let F be an endofunctor on Hask. Let

W(a) = ∀r.F(a->r)->r
W(f) = F(f∗)∗
       where g∗(h) = h∘g

The puzzle becomes geometric/combinatoric in nature once you realize the following isomorphism:

Theorem 1.

Suppose neither of the types (∀r.r->F(r)) (∀r.F(r)->r) is empty. Then there is an isomorphism of types W(a) ≃ (∀r.F(r)->r, a).

Proof:

class Functor f => Fibration f where
        projection   :: ∀r. f(r)->r
        some_section :: ∀r. r->f(r) -- _any_ section will work

to :: forall f a. Fibration f
      => (∀r.f(a->r) -> r)
      -> (∀r.f(r)->r, a)
to(f) = ( f . fmap const
        , f(some_section(id)))

from :: forall f a. Fibration f
        => (∀r.f(r)->r, a)
        -> (∀r.f(a->r) -> r)
from (π,η) = ev(η) . π

ev :: a -> (a->b) -> b
ev x f = f x

Filling up the details of this (which I can post on request) will require a bit of parametricity and Yoneda lemma. When F is not a Fibration (as I defined above), W is trivial as you observed.

Let us call a fibration a covering if the projection is unique (though I'm not sure if this usage is appropriate).

Admitting the theorem, you can see W(a) as the coproduct of a's indexed by _all possible fibrations ∀r.F(r)->r, i.e.

W(a) ≃ ∐a
       π::∀f.F(r)->r

In other words, the functor W (as a presheaf on Func(Hask)) takes a fibration and constructs a canonically trivialized covering space from it.

As an example, let F(a)=(Int,a,a,a). Then we have three evident natural fibrations F(a)->a. Writing the coproduct by +, the following diagram together with the above theorem should hopefully be enough to describe the comonads concretely:

           a
           ^
           | ε
           |
         a+a+a
        ^  |  ^
     Wε |  |δ | εW
        |  v  |
(a+a+a)+(a+a+a)+(a+a+a)

So the counit is unique. Using evident indices into the coproduct, Wε maps (i,j) to j, εW maps (i,j) to i. So δ must be the unique 'diagonal' map, namely δ(i) == (i,i)!

Theorem 2.

Let F be a Fibration and let ΩW be the set of all comonads with the underlying functor W. Then ΩW≃1.

(Sorry I have not formalized the proof.)

An analogous combinatorial argument for the set of monads ΜW would be interesting too, but in this case ΜW may not be a singleton. (Take some constant c and set η:1->c and μ(i,j)=i+j-c.)

Note that the monads/comonads so constructed are not the duals to the original comonads/monads in general. For instance let M be a monad (F(a)=(Int,a), η(x) = (0,x), μ(n,(m,x)) = (n+m,x)), i.e. a Writer. The natural projection is unique hence by the theorem W(a)≃a, and there is no way to respect the original algebra.

Note also that a comonad is trivially a Fibration (in possibly many different ways) unless Void, which is why you got a Monad from a Comonad (but that's not necessarily unique!).

A few comments about your observations:

• Dual IO a is essentially Void

  As far as I know, in Haskell IO is defined something like:

    -- ghc/libraries/ghc-prim/GHC/Types.hs
   newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
  

  which means from the type theory alone the corresponding covering is_ the unique canonical covering space indexed by all State# RealWorlds. Whether you can (or should) reject this is probably a philosophical, rather than a technical question.

• MonadPlus m => Dual m a is Void

  Right, but do note that if F(a)=0 then W(a)=1 and it's not a comonad (because otherwise the counit would imply the type W(0)->0 ≃ 1->0). This is the only case where W can not even be a trivial comonad given an arbitrary functor.

• Dual Reader is.. Those statements will sometimes be correct, sometimes not. Depends on whether the (co)algebra of interest agrees with the (bi)algebra of coverings.

So I'm surprised how interestingly geometric Haskell really is! I guess there may be very many geometric constructions similar to this. For example a natural generalization of this would be to consider the 'canonical trivialization' of F->G for some covariant functors F,G. Then the automorphism group for the base space would no longer be trivial, so a bit more theory would be required to properly understand this.

Finally, here's a proof of concept code. Thanks for a great refreshing puzzle, and have a very merry Christmas ;-)

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Control.Comonad

class Functor f => Fibration f where
        x0 :: f ()
        x0 = some_section ()

        some_section :: forall r. r -> f(r)
        some_section x = fmap (const x) x0

        projection :: forall r. f(r) -> r

newtype W f a = W { un_w :: forall r. f(a->r)->r }

instance Functor f =>  Functor (W f) where
        fmap f (W c) = W $ c . fmap (. f)

instance Fibration f => Comonad (W f) where
        extract = ε
        duplicate = δ

-- The counit is determined uniquely, independently of the choice of a particular section.
ε :: forall f a. Fibration f => W f a -> a
ε (W f) = f (some_section id)

-- The comultiplication is unique too.
δ :: forall f a. Fibration f => W f a -> W f (W f a)
δ f = W $ ev(f) . un_w f . fmap const

ev :: forall a b. a -> (a->b)->b
ev x f = f x

-- An Example
data Pair a = P {p1 ::a
                ,p2 :: a
                 }
               deriving (Eq,Show)

instance Functor Pair where
        fmap f (P x y) = P (f x)  (f y)

instance Fibration Pair where
        x0 = P () ()
        projection = p1

type PairCover a = W Pair a

-- How to construct a cover (you will need unsafePerformIO if you want W IO.)
cover :: a -> W Pair a
cover x = W $ ev(x) . p1