Monads with depenent types

Stream: new members

[Simon Daniel]

Im Trying to write a Monad M that captures a Sequence of effects. Those effects produce Values that Depend on the Monads context (Nat in my example for read only state). I think this cannot be written as a monad, since it would require a Nat -> Type instead of just Type. But im kinda stuck finding a working solution. The dependent Values used in my effects are not meant to ever leave the monad context, and may only be created inside the context

inductive A (n1 n2: Nat) (α: Type)   where
| Some: n1 = n2 -> α -> A n1 n2 α
| None: n1 ≠ n2 -> A n1 n2 α

def B (n1:Nat) (a) := fun (n2:Nat) => A n1 n2 a

inductive Eff (n:Nat): (Nat -> Type) -> Type 1  where
| Create : (n2:Nat) -> (IO a) -> Eff n (B n2 a)

inductive M (n:Nat): (Nat -> Type) -> Type 1  where
| Do :  Eff n b -> ((b n) -> M n a) -> M n a
| Return: a -> M n (fun _ep => a)

def M.bind {α β}: M ep α → ((α ep) → M ep β) → M ep β
| M.Do eff next, next' => M.Do eff (fun x => bind (next x) next')
| M.Return v, next' => next' v

def M.pure (v: α):  M n (fun _ => α) :=
  M.Return v

instance: Monad (M n) where
  bind := M.bind
  pure := M.pure