Indexed monads are a generalisation of monads where, from a functional programming perspective, a monadic type constructor is annotated (indexed) by another type representing effect information that explains the effects of a computation, i.e., values of type M r a are effectul computations of values of type a with effects r. They provide a way to give finer-grained information about impurity and capture a greater class of effectul computations that normal monads.
In Haskell, indexed monads are defined something like:
class IxMonad (m :: * -> * -> *) where type Unit m type Plus m s t return :: a -> m (Unit m) a (>>=) :: m s a -> (a -> m t b) -> m (Plus m s t) b
where the type-level function Unit describes the trivial "pure" effect, and Plus combines effect information from subcomputations. These form a monoid.
- Slides from talk at Fun in the Afternoon (12 March 2014 @ Facebook, London)
- We previously proposed indexed comonads in " Coeffects: Unified static analysis of context-dependence" (Tomas Petricek, Dominic Orchard, and Alan Mycroft, ICALP 2013). Indexed comonads have various other related indexed structures to give a semantics to the lambda calculus for coeffects, whereas indexed monads (their dual) do not need as much structure to give a semantics for effects.
- "The semantic marriage of monads and effects (extended abstract)" (Dominic Orchard, Tomas Petricek, Alan Mycroft, 2013, [arXiv:1401.5391]) briefly explains more of the theoretical basis.
- "Parametric effect monads and the semantics of effect systems" (Katsumata, POPL 2014) introduces the same concept (called instead parametric effect monads) with more theoretical background.