The Coq mailing list

[Thomas Strathmann <thomas AT pdp7.org>]

On 2/18/11 18:21 , AUGER Cedric wrote:
> I wanted to learn what is a monad, so I read some tutorial on it and
> wrote this implementation in Coq
> (http://coq.inria.fr/cocorico/AUGER_Monad).

Nice. Attached is an implementation of the list monad I adapted from a 
small exercise I did a while ago. Perhaps it's useful if you plan on 
building a sort of library around monads like the Haskell one.

        Thomas

--
Thomas S. Strathmann                            http://pdp7.org/blog/
Require Import List.

Instance ListMonad : Monad list :=
  {| 
     return_ := fun (A : Type) (a : A)  => a :: nil;
     bind := fun (A : Type) (m : list A) (B : Type) (f : A -> list B) => 
flat_map f m
  |}.
(* right unit *)
induction a.
simpl.
reflexivity.
simpl.
rewrite <- IHa.
reflexivity.
(* left unit *)
intros.
simpl.
rewrite <- app_nil_end.
reflexivity.
(* associativity *)
induction ma.
simpl.
trivial.
intros.
simpl.
cut (flat_map g (f a ++ flat_map f ma) =
           flat_map g (f a) ++ flat_map g (flat_map f ma)).
intros.
rewrite H.
rewrite IHma.
reflexivity.
induction (f a).
simpl.
reflexivity.
simpl.
rewrite IHl.
rewrite app_ass.
reflexivity.
Defined.