Module Type MONAD.
 Set Implicit Arguments.
 Parameter M : forall (A : Type), Type.
 Parameter ret : forall (A : Type), A -> (M A).
 Parameter bind : forall (A B : Type), M A -> (A -> M B) -> M B.
 
 Infix ">>=" := bind (at level 20, left associativity) : monad_scope.
 Open Scope monad_scope.

 Axiom left_neutral : forall (A B : Type) (f : A -> M B) (a : A), 
   (ret a) >>= f = f a.
 Axiom right_neutral : forall (A B : Type) (m : M A), 
   m >>= (fun a : A => ret a) = m.
 Axiom assoc : forall (A B C : Type) (m : M A) (k : A -> M B)(h : B -> M C),
   m >>= (fun x : A => k x >>= h) = (m >>= k) >>= h.
End MONAD.

Inductive Maybe (A:Type) : Type := 
  | Nothing : Maybe A
  | Just : A -> Maybe A.


Module MaybeMonad <: MONAD. 
  Set Implicit Arguments.
  
  Definition M := Maybe.
  
  Definition ret (A : Type) := fun a:A => Just A a.
  
  Fixpoint bind (A : Type) (B : Type) (l : M A) (f : A -> M B) {struct l} : M B :=
  match l with
    | Nothing => Nothing B
    | Just a => f a
  end.
  
  Infix ">>=" := bind (at level 20, left associativity) : monad_scope.
  Open Scope monad_scope.
  
  Lemma left_neutral : forall (A B : Type) (f : A -> M B) (a : A), 
   (ret a) >>= f = f a.
  Proof.
   intros.
   simpl.
   reflexivity.
  Defined.
  
  Lemma right_neutral : forall (A B : Type) (m : M A), 
    m >>= (fun a : A => ret a) = m.
  Proof.
    intros.
    induction m.
     simpl.
      reflexivity.
    simpl.
      auto.
  Defined.
  
  Lemma assoc : forall (A B C : Type) (m : M A) (k : A -> M B)(h : B -> M C),
   m >>= (fun x : A => k x >>= h) = (m >>= k) >>= h.
  Proof.
    intros.
    induction m.
     simpl.
       reflexivity.
    simpl.
      reflexivity.   
  Defined.
  
  
End MaybeMonad.