- an adjunction `F -| G`
- is read "F is left adjoint to G"
- consist of functors `F : D -> C` and `G : C -> D`
- gives rise to a monad `GF : D -> D` and a comonad `FG : C -> C`
- adjunctions can be composed
- consider two adjunctions:
- `F' -| (G' : D -> E)`
- `F -| (G : C -> D)`
- their composition `(F' -| G') <<< (F -| G)` is an adjunction `FF' -| (G'G : C -> E)`
- it would look a little bit like a telescoping two legged thing
- this composed adjunction gives rise to a monad `G'GFF' : E -> E` and a comonad `FF'G'G : C -> C` by the same reasoning as would apply to any other adjunction
- notice how there is a monad `GF : D -> D` "sandwiched" in the monad `G'GFF'`, and analogously a comonad `F'G' : D -> D` "sandwiched" in the comonad `FF'G'G`
- the continuation monad `Cont r : Hask -> Hask`
- is formed by the adjunction `(_ -> r) -| ((_ -> r) : Hask_op -> Hask)`
- an arbitrary Haskell comonad `W = UV`
- is formed by an adjunction `U -| (V : Hask -> C)` for some category `C`
- we can compose the adjunctions underlying `Cont r` and `W` (`W` after `Cont r`)
- their composition is an adjunction `(U _) -> r -| (V (_ -> r) : Hask_op -> C)`
- this composed adjunction gives rise to a monad in Hask
- it induces the comonad `UV (_ -> r) -> r : Hask_op -> Hask_op` (where `UV = W`)
- a comonad in `Hask_op` is a monad in `Hask`
- so the composition gives rise to a monad `Co r = W (_ -> r) -> r` in Hask
- can the composed adjunction also give rise to a comonad in Hask? something is wrong...
- it induces the monad `V ((U _) -> r) -> r : C -> C`
- the problem unfortunately is that there is no trace left of our original `W`, and we're in some weird `C` category
we can perhaps run the whole exercise backwards by interpreting the adjunction underlying Cont
as its own dual, and trying to compose it with the adjunction underlying a monad. perhaps this will yield a useful comonad in Hask? (edited)