The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

Hello list.

I was working on some simple monad implementations a few weeks ago. The
implementations for the identity, option, and error monads were very
easy but I became stuck when it came to proving the monad laws for the
State monad. I've gone back to them today but have gotten no further. Any
advice on how to prove the laws would be appreciated!

--8<--

Module Type Base.
  Parameter M : Type -> Type.

  Parameter bind     : forall {A B : Type}, M A -> (A -> M B) -> M B.
  Parameter return_m : forall {A : Type}, A -> M A.

  (* return x >>= f = f x *)
  Parameter left_identity : forall (A B : Type) (x : A) (f : A -> M B),
    bind (return_m x) f = f x.

  (* m >>= return = m *)
  Parameter right_identity : forall (A : Type) (m : M A),
    bind m return_m = m.

  (* (m >>= f) >>= g = m >>= (\x -> f x >>= g) *)
  Parameter associativity : forall (A B C : Type) (f : A -> M B) (g : B -> M 
C) (m : M A),
    bind (bind m f) g = bind m (fun z => bind (f z) g).

End Base.

Module Type Notations (MT : Base).
  Notation "x >>= y" := (MT.bind x y)            (at level 42, left 
associativity).
  Notation "x >>  y" := (MT.bind x (fun _ => y)) (at level 42, left 
associativity).
End Notations.

Inductive state (S A : Type) :=
  | State : (S -> (A * S)) -> state S A.

Definition run {S A : Type} (m : state S A) : (S -> (A * S)) :=
  match m with
    State c => c
  end.

Module Monad_State <: Base.
  Parameter S : Type.
  Definition M := state S.

  Definition bind {A B : Type} (m : M A) (f : A -> M B) : M B :=
    State S B (fun s =>
      match run m s with
        | (a, s') => run (f a) s'
      end).

  Definition return_m {A : Type} (x : A) : M A :=
    State S A (fun s => (x, s)).

  Lemma left_identity : forall (A B : Type) (x : A) (f : A -> M B),
    bind (return_m x) f = f x.
  Proof.
    admit.
  Defined.

  Lemma right_identity : forall (A : Type) (m : M A),
    bind m return_m = m.
  Proof.
    admit.
  Defined.

  Lemma associativity : forall {A B C : Type} (f : A -> M B) (g : B -> M C) 
(m : M A),
    bind (bind m f) g = bind m (fun z => bind (f z) g).
  Proof.
    admit.
  Defined.

End Monad_State.

--8<--