8-39.v

(* bindの記法を予約 *)
Reserved Notation "x >>= y" (at level 110, left associativity).

(* モナド *)
Class Monad(M:Type -> Type) := {
  bind {A B} : M A -> (A -> M B) -> M B
    where "x >>= f" := (bind x f);
  ret {A} : A -> M A;
  left_id : forall {A:Type} {B:Type} (x:A) (f:A -> M B), ((ret x) >>= f) = (f x);
  right_id : forall {A:Type} (x:M A), (x >>= ret) = x;
  assoc : forall {A:Type} {B:Type} {C:Type} (a:M A) (b:A -> M B) (c:B -> M C) , ((a >>= b) >>= c) = (a >>= (fun x => ((b x) >>= c)))
}.

Notation "x >>= f" := (@bind _ _ _ _ x f).

Require Import List.

Program Instance ListMonad : Monad list := {|
  bind A B m f := flat_map f m;
  ret A x := (cons x nil)
|}.
Next Obligation.
rewrite app_nil_r.
reflexivity.
Qed.
Next Obligation.
unfold flat_map.
simpl.
induction x.
reflexivity.
f_equal.
assumption.
Qed.
Next Obligation.
intros.
induction a.
simpl.
reflexivity.
simpl.
rewrite <- IHa.
cut (forall (A B : Type)(l l' : list A)(f : A -> list B),flat_map f (l++l') = flat_map f l ++ flat_map f l').
intros.
rewrite H.
reflexivity.
induction l.
simpl.
intros.
reflexivity.
intros.
simpl.
rewrite IHl.
rewrite app_ass.
reflexivity.
Qed.
Definition foo : list nat := 1 :: 2 :: 3 :: nil.

(* 内包記法もどき *)
(*
  do x <- foo
     y <- foo
     (x, y)
*)
Definition bar := Eval lazy in
  foo >>= (fun x =>
  foo >>= (fun y =>
  ret (x, y))).

Print bar.