Side-effects are comonadic: dependently graded comonads and parametric right adjoint monads.

There's a sort of motto in functional programming that "monads are about effectful functions, and comonads are about context-sensitive functions". This motto misrepresents the foundational work of Moggi and Kieburtz on (co)monadic semantics for programs: Moggi identifies monads as "notions of computation", of which one notion is computation with side effects, while Kieburtz identifies some comonads as concerning effects which arise from interaction with the context of computation. But if side-effects are effects on the "side", shouldn't all effects arise from interaction with the context of computation? Can all effectful computation be handled comonadically?

In this talk, we'll introduce dependently graded comonads as a generalization of graded comonads where the grade can depend on the domain type of a Kliesli morphism. We'll see a few examples of dependently graded comonads before discovering that these examples look somewhat familiar. This familiarity will be explained by a theorem: every parametric right adjoint monad admits a (left adjoint) dependently graded comonad, and these have isomorphic Kleisli categories. Since parametric right adjoint monads include all monads whose underlying action on types is given by a strictly positive type constructor, this theorem shows that Moggi's side-effect monads can all be transposed into dependently graded comonads --- showing ultimately that effectful computation is comonadic in nature.

Joint work with Matteo Capucci.