Skip to content

Instantly share code, notes, and snippets.

@masaeedu
Last active September 16, 2019 09:02
Show Gist options
  • Save masaeedu/5892050bbbbef8d7601a96750b455724 to your computer and use it in GitHub Desktop.
Save masaeedu/5892050bbbbef8d7601a96750b455724 to your computer and use it in GitHub Desktop.
- 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)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment