[Agda] Indexed Monads

[Dan Doel]

Hello,

I've been playing with Agda 2 in my spare time lately, and have found it quite 
enjoyable (and rather remarkable; it's amazing how close to, say, Haskell one 
can get in terms of the conciseness of function definitions). However, part 
of the standard library has left be a bit confused, so I thought I'd ask 
about it, if it's not too much trouble.

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. The only way I 
came up with to use the included indexed state monad was as follows:

  natToType : ℕ -> Set
  natToType 0 = ℕ
  natToType 1 = Fin 1
  natToType n = [ ℕ ]

  test : {M : IFun ℕ}{i : ℕ}(SM : RawIMonadState natToType M)
         -> M i 2 ⊤
  test SM = put {_} {0} zero >> put {_} {1} fz >> put {_} {2} (zero ∷ [])
    where
    open RawIMonadState SM

Which, if you'll excuse my saying so, seems rather cumbersome. By contrast, I 
fooled around to make type-indexed monads (the main change being 'IFun = 
Set -> Set -> Set -> Set', and associated cleanup), and the code 
corresponding to the above is:

  test : {i : Set}{M : IFun}(SM : RawIMonadState M) -> M i [ ℕ ] ⊤
  test SM = put zero >> put tt >> put (zero ∷ [])
    where
    open RawIMonadState SM

which works without any overhead (although I changed fz to tt, as unresolved 
metas resulted from fz never being used and having no declared type).

I initially ran into the issue implementing a monad for delimited 
continuations, the definition of which was straight forward enough, but the 
use of which suffers from the same problem as the indexed state monad. And, 
it appears to me that all monads that rely on type indices will be the same 
way.

I can't, of course, claim that my type-indexed definition is perfect, either. 
For instance, my RawMonad records arbitrarily set the index type to unit to 
prevent problems with unresolved metas elsewhere. This means that the 
ordinary state monad doesn't fit with that record, however, as for that, one 
wants all indices to be of some fixed type S. This particular case turns out 
not to be much of a problem, as the indexed state monad works just as well 
(modulo the fz type issue mentioned above), but it would inhibit any other 
monad that wants a single, particular index type (reader and writer come to 
mind). Off the top of my head, a function : Set -> Set, like the above I -> 
Set might be used to overcome this, but it's still not ideal.

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.

Thanks very much for your time (and for Agda; it's very cool).
-- Dan Doel

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.