[Agda] Indexed Monads

[Ulf Norell]

On Sun, Feb 24, 2008 at 7:44 PM, Dan Doel <dan.doel at gmail.com> wrote:

>
> Specifically: indexed monads (and applicative functors, for that matter).
> I
> hadn't seen them before, but was able to find some brief explanation
> online
> describing them. However, unlike most of the articles I found, the indexed
> monads in the standard library are indexed by values rather than types.
> Thus,
> to get back to type-indexed monads, one must use a function (I -> Set), as
> in
> the state monad included.
>
> This, of course, works fine for the ordinary state monad, as one can
> choose
> the unit type as the index set, and (\_ -> S) as the function, where S is
> the
> type of state. However, one of the motivations for using indexed monads is
> a
> state monad where the state type can change over the course of the
> computation. But this requires an index type rich enough to represent all
> the
> types the state can take on, and a corresponding function.


Anyhow, to sum up, I was just wondering if there was some particular reason
> for choosing value-indexed monads, or some way of using them in a less
> cumbersome manner that I'm totally missing. I suppose I could see their
> use
> in lieu of phantom types (phantom values?), but it seems like an odd
> choice
> to me, given that the examples of indexed monads I found relied on the
> indices being types.


The motivation for choosing the value-indexed state monad is that it gives
you control over which types the state can take. As such it is a
generalization of the normal state monad with a state of a fixed type to a
state monad where the state is a family of types. As you note, the state
monad where the state can be an arbitrary type doesn't specialize to the
normal state monad.

P.S.: If desired, I could provide the source for the delimited continuation
> monad. I attempted to stick as close as possible to the format in
> Category.Monad.State. Though it's nothing particularly complex (shift and
> reset with a single prompt), it's another motivator for having/example of
> indexed monads.


That would be interesting.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080225/c35fe5c3/attachment.html