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.
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
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: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.
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:
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 VoidAs far as I know, in Haskell IO is defined something like:
which means from the type theory alone the corresponding covering is_ the unique canonical covering space indexed by all
State# RealWorld
s. Whether you can (or should) reject this is probably a philosophical, rather than a technical question.MonadPlus m => Dual m a
is VoidRight, 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 ;-)