Set Implicit Arguments.

Class Monad (comp : Type -> Type) : Type :=
 {ret  : forall {A}, A -> comp A;
  bind : forall {A B}, 
         comp A -> (A -> comp B) -> comp B
 }.

Notation "X <- A ; B" := (bind A (fun X => B)) 
   (at level 30, right associativity).
Notation "'return' t" := (ret t) (at level 1).

Definition join comp {_:Monad comp} A 
           ( t : comp (comp A) ) : comp A
 := X <- t; X.

(** Monad of errors *)

Inductive Error A 
  := Raise : Error A | Val : A -> Error A.

Implicit Arguments Raise [[A]].

Definition bindError {A B:Type} 
 (a:Error A) (f : A -> Error B) : Error B := 
  match a with 
    | Raise => Raise
    | Val a => f a
  end.

Instance ErrMonad : Monad Error
   := {ret := Val; bind := @bindError}.

Require Export List.

Fixpoint mape A B (f:A -> Error B) (l : list A) 
 : Error (list B) := 
  match l with 
      nil => return nil
    | (a::m) => b <- f a; 
                mb <- mape f m; 
                return (b::mb)
  end.

Definition f (_:nat) := Raise (A:=nat).
Eval compute in (mape f nil).
Eval compute in (mape f (1::2::nil)).

(** State monad *)

Definition State (st A : Type) := st -> A * st.

Definition read st : State st st := fun s => (s,s).
Definition write st (f:st -> st) : State st unit 
     := fun s => (tt,f s).

Definition unitState st {A} (a:A) : State st A  
     := fun s => (a,s).

Definition bindState st {A B} 
  (a:State st A) (f : A -> State st B) : State st B 
     := fun s => let (a,s1) := a s in f a s1.

Instance StateMonad (st:Type) : Monad (State st) := 
   {ret := @unitState st; bind := @bindState st}.

Fixpoint mapst st A B (f:A -> State st B) (l : list A) 
: State st (list B) := 
  match l with 
        nil => return nil
   | (a::m) => b <- f a; 
               mb <- mapst f m; 
               return (b::mb)
  end.

(** Example *)

Definition st := nat.

Definition g (n: nat) : State st nat := 
     X <- write (fun (m:nat) => (n+m)%nat); 
     a <- read (st:=st); 
     return a.

Eval compute in (mapst g nil) 0.
Eval compute in (mapst g (1::2::3::4::nil)) 0.