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.
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 -> a
and (>>=) :: 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.