Indexed monads

**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

**Slides from talk at Fun in the Afternoon**(12 March 2014 @ Facebook, London)

#### Code

- GitHub
- Hackage (cabal install ixmonad)
- Stencil specifications example

#### References

- 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.