The intuition behind the definition of the co-reader monad

Question

In https://hackage.haskell.org/package/category-extras-0.53.0/docs/Control-Comonad-Reader.html, the co-reader monad is defined, and the co-monadic type modality applies to a type a and generates a pair (r,a). The comonadic type modality w is therefore of type a -> (r, a).

This is quite different from the reader monad, in which the monadic type modality applies to a type a and generates a function of type r -> a, for a particular type r.

It is not clear to me why the co-monadic modality is not defined in a way analogous to the reader modality, so that, where w is the relevant co-monadic modality, we have w a := r -> a, and then the functions extract :: w a -> a and (<<=) :: (w a -> b) -> w a -> w b merely rearrange return :: a -> m a and bind (=<<) :: (a -> m b) -> m a -> m b, respectively (where m a : = r -> a).

This is to say, can the co-reader monad be defined analogously to the reader monad, except that we change the direction of the arrows? Is changing the arrows of bind and of return sufficient to generate (a (?)) co-reader monad? If not, then why not.

Furthermore, would it be possible to define a comonadic modality w as w a := r -> a, together with the functions extract :: w a -> a and (<<=) :: (w a -> b) -> w a -> w b?

Edit: this question has been totally rewritten in response to an objection that it was unclear.

There is no terminating implementation for the polymorphic type (e -> a) -> a, while it's easy to implement (e, a) -> a (with snd) and its curried variant a -> ( e -> a) (with const). We can't take the same functor from the monad and make it into a comonad. We need the left adjoint, which is provided by (un)currying. — chi
This is an interesting subject, but I'm voting to close as unclear for now. If you can make the question precise, please do. — Here's a short discussion on the reader and writer comonads: olivierverdier.com/posts/2014/12/31/reader-writer-monad-comonad — leftaroundabout
@chi What do you mean by a terminating implementation in this context? And why is that important? Why do we need the left adjoint? — user65526
@user65526 Just because in some model a formula is true, it does not mean that it can be proved (it could be false in other models). For the last question: intuitively, if I give you a function r->e but no r, there's no way for you to construct a e. More in general, the proposition (A->B)->B isn't an intuitionistic tautology (nor a classical one), so by Curry-Howard it can't be implemented. — chi

user65526 user65526 · Accepted Answer · 2020-06-23T09:41:46

Comonads and monads are universal constructions, in the sense that, given a monadic type modality m and a co-monadic type modality w, we must be able to construct m a and w a and the relevant functions (return :: a -> m a and extract:: wa -> aand (>>=) :: m a -> ( a -> m b) -> m b and (<<=) :: (w a -> b) -> w a -> w b), for any type a).

The problem is that when w a:= r -> a, extract:: wa -> a is not universally derivable, for all types a. In the simply typed lambda calculus, for example, we cannot find a lambda term of type wa -> a, for any type a (though in special cases, where a is instantiated to a certain type, this may be possible).

Consequently, defining the co-monadic reader modality in this way fails to provide a universal construction of the appropriate type.

The intuition behind the definition of the co-reader monad

1 Answers