ST and runST interface in Coq (WIP)

gistfile1.txt

Class fmonad (M : (Type -> Type) -> Type) := {
  fmreturn : forall {A : Type -> Type} {B}, (B -> A B) -> M A;
  fmbind : forall {A B : Type -> Type} {C}, M A -> ((C -> A C) -> M B) -> M B
}.

Class ST (T : (Type -> Type) -> Type) := {
  monadOfST :> fmonad T;
  runST : forall {A}, T (fun _ => A) -> A
}.