[Agda] Indexed Monads

[Nils Anders Danielsson]

On Sun, Feb 24, 2008 at 19:44, Dan Doel <dan.doel at gmail.com> wrote:
>
> [...] 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.

(Late reply, but I came to think of this thread today.)

Some time this spring Ulf added a "shallow injectivity" check to Agda.
By using this check Agda can infer the indices for you, under certain
restrictions:

  data U : Set where
    nat  : U
    fin1 : U
    list : (t : U) -> U

  El : U -> Set
  El nat      = ℕ
  El fin1     = Fin 1
  El (list t) = List (El t)

  test : {M : IFun U}{i : U}(SM : RawIMonadState El M)
         -> M i _ ⊤
  test SM = put zero >> put fz >> put (zero ∷ [])
    where open RawIMonadState SM

> Anyhow, to sum up, I was just wondering if there was some particular
> reason for choosing value-indexed monads

One advantage is that one can pattern match on data type values.

-- 
/NAD