3

The situation is as follows (I changed to more standard-ish Haskell notation):

class Functor f => MonoidallyCopointed f where
    copointAppend ::  (∀r.f(r)->r) -> (∀r.f(r)->r) -> (∀r.f(r)->r)
    copointEmpty  ::  ∀r.f(r)->r

such that for all instance F of MonoidallyCopointed and for all

x,y,z::∀r.F(r)->r

The following holds:

x `copointAppend` copointEmpty == copointEmpty `copointAppend` x == x
x `copointAppend` (y `copointAppend` z) == (x `copointAppend` y) `copointAppend` z

Then is it true that F has a natural Comonad instance defined from copointAppend and copointEmpty?

N.B. The converse holds (with copointEmpty = extract and copointAppend f g = f . g . duplicate.)

EDIT

As Bartosz pointed out in the comment, this is mostly the definition of comonads using the co-Kleisli adjunction. So the question is really about the constructivity of this notion. Accordingly, the following question is probably more interesting in terms of real-world applications:

Does there exist a constructive isomorphism between the set of possible Comonad instances of f and the set of possible MonoidallyCopointed instances of f?

This can be useful in practice because a direct definition of Comonad instance can involve a bit of technical, hard-to-read code that cannot be verified by the type checker. For example,

data W a = W (Maybe a) (Int -> a) (Either (String -> a) (a,a,a,a))

has a Comonad instance but the direct definition (with the proof that it's indeed a Comonad!) may not be so easy. On the other hand, providing a MonoidallyCopointed instance may be a little easier (but I'm not perfectly sure of this point).

mnish
  • 385
  • 2
  • 11
  • 1
    `e` seems to be a natural fit for the unit. Do you have an idea how you might define, uh, comultiplcation? `f(r) -> f(f(r))` – luqui Dec 28 '16 at 08:57
  • @luqui: I think so, e would serve as the counit. Actually I want to check if (forall r. f(r)->r, a) is a Monad, f must be a Comonad. This was motivated by revising an answer I wrote to another question about Comonads. – mnish Dec 28 '16 at 09:07
  • @luqui: I mean this [question](http://stackoverflow.com/questions/34302616/can-you-define-comonads-based-on-monads). – mnish Dec 28 '16 at 09:09
  • 1
    How about naming this something other but [`<*>`](http://hackage.haskell.org/package/base-4.9.0.0/docs/Control-Applicative.html#v:-60--42--62-)? – leftaroundabout Dec 28 '16 at 13:46
  • @leftaroundabout: What would be a good fit? I often use \otimes, but unicode characters often get in the way of correct indentation in Emacs. Any suggestion? – mnish Dec 29 '16 at 03:43
  • This is not strictly necessary, but I might better add the condition that f is additionally pointed (i.e. `forall r.r->f(r)` is inhabited). Then the question becomes about constructing suitable `extend` out of such 'points' of the functor. – mnish Dec 29 '16 at 03:50
  • 2
    This is almost the definition of a comonad using co-Kleisli arrows, except that co-Kleisli arrows can go between different objects (f a -> b). For this to be a comonad you'd have to extend <*> to the full-blown co-Kleisli composition operator =>=. I don't see how this could be done, unless you're working in a discrete category – Bartosz Milewski Dec 29 '16 at 07:40
  • 1
    @mnish huh? I use unicode characters all the time when coding Haskell in Emacs, don't see how `⊗` would be a problem. Nevertheless something ASCII like, whatever, `>*<` might be preferrable for compatibility. – leftaroundabout Dec 29 '16 at 15:17
  • @Bartosz Thanks, true enough! It would be quite interesting if that kind of high level statement actually leads to a concrete combinatorial description. You don't need to consider general co-Kleisli arrows, endomorphic arrows are enough as long as the derivation is natural. – mnish Dec 30 '16 at 01:13
  • Does the lens package do this? – mnish Dec 30 '16 at 02:54
  • Skimmed the documentation and I couldn't find a reason why it can't do this. Probably this is it. – mnish Dec 30 '16 at 03:18

0 Answers0