Monad of Identity, Maybe, List

H.v

Require Import ssreflect.

Class Monad (M : Type -> Type) :=
{
  mreturn : forall {A}, A -> M A
; mbind : forall {A B}, M A -> (A -> M B) -> M B

; left_return : forall A B (a : A) (k : A -> M B), mbind (mreturn a) k = k a
; right_return : forall A (m : M A), mbind m mreturn = m
; composite : forall A B (m : M A) (k : A -> M A) (h : A -> M B),
                mbind m (fun x => mbind (k x) h) = mbind (mbind m k) h
}.

Inductive Identity (A : Type) : Type :=
  | runIdentity : A -> Identity A.

Instance: Monad Identity :=
{
  mreturn A x := runIdentity A x
; mbind A B m k :=
    match m with
      | runIdentity m' => k m'
    end
}.
Proof.
  intros. by [].

  intros.
  case m.
  by intros.

  intros.
  case m.
  intro.
  case (k a).
  by simpl.
Qed.

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

Instance: Monad Maybe :=
{
  mreturn A x := Just A x
; mbind A B m k :=
    match m with
      | Just a => k a
      | Nothing => Nothing B
    end
}.
Proof.
  by intros.

  intros.
  case m. by []. by [].

  intros.
  case m. by [].
  intros.
  case (k a). by []. by [].
Qed.

Inductive List (A : Type) : Type :=
  | nil : List A
  | cons : A -> List A -> List A.

Fixpoint append {A : Type} (l1 l2 : List A) : List A :=
  match l1 with
    | nil => l2
    | cons x xs => cons A x (append xs l2)
  end.

Fixpoint foldr {A B : Type} (f : A -> B -> B) (b : B) (la : List A) : B :=
  match la with
    | nil => b
    | cons x xs => f x (foldr f b xs)
  end.

Instance: Monad List :=
{
  mreturn A x := cons A x (nil A)
; mbind A B m k := foldr (fun x y => append (k x) y) (nil B) m
}.
Proof.
  intros.
  unfold foldr.
  induction (k a).
    by simpl.
    simpl. by rewrite IHl.
  
  intros.
  induction m.
    by simpl.
    simpl. by rewrite IHm.

  intros.
  induction m.
    by simpl.
    simpl. rewrite IHm.
    induction (k a).
      by simpl.
      simpl.
      induction (h a0).
        by simpl.
        simpl. by rewrite IHl0.
Qed.