monad_coercion.v

(* Monad with Coercion *)

Require Import ssreflect.

Definition relation (A: Type) := A -> A -> Prop.
Hint Unfold relation.

Definition refl {A: Type}(R: relation A)
  := forall a, R a a.
Definition sym {A: Type}(R: relation A)
  := forall a b, R a b -> R b a.
Definition trans {A: Type}(R: relation A)
  := forall a b c, R a b -> R b c -> R a c.
(* Class Reflexivity {A: Type}(R: relation A) := *)
(*   { refl:> forall a, R a a }. *)
(* Class Symmetricity {A: Type}(R: relation A) := *)
(*   { sym:> forall a b, R a b -> R b a }. *)
(* Class Transitivity {A: Type}(R: relation A) := *)
(*   { trans:> forall a b c, R a b -> R b c -> R a c }. *)
Hint Unfold refl sym trans.

Reserved Notation "x == y" (at level 85, no associativity).
Class Equivalence (A: Type) :=
  {
    equiv_eq: relation A where "x == y" := (equiv_eq x y);
    equiv_refl: refl equiv_eq;
    equiv_sym: sym equiv_eq;
    equiv_trans: trans equiv_eq
  }.
(* Coercion equiv_eq: Equivalence >-> relation. *)
Notation "x == y" := (equiv_eq x y) (at level 85, no associativity).
Hint Resolve equiv_refl equiv_sym equiv_trans.
Hint Opaque equiv_refl equiv_sym equiv_trans.

Program Instance make_Equivalence
        {A: Type}(eq: relation A)
        (eq_refl: refl eq)
        (eq_sym: sym eq)
        (eq_trans: trans eq)
: Equivalence A
  :=
    {
      equiv_eq := eq;
      equiv_refl := eq_refl;
      equiv_sym := eq_sym;
      equiv_trans := eq_trans
    }.

Program Instance eq_Equivalence (A: Type): Equivalence A | 100
  := {
      equiv_eq := eq
    }.
Next Obligation.
  congruence.
Qed.
Next Obligation.
  congruence.
Qed.
Next Obligation.
  congruence.
Qed.

Class Setoid :=
  {
    setoid_type: Set;
    setoid_equiv: Equivalence setoid_type
  }.
Coercion setoid_type: Setoid >-> Sortclass.
Existing Instance setoid_equiv.

Class Morphism (X Y: Setoid) :=
  {
    morphism_f: X -> Y;
    morphism_eq:
      forall x x',
        x == x' -> morphism_f x == morphism_f x'
  }.
Coercion morphism_f: Morphism >-> Funclass.
Notation "X --> Y" := (Morphism X Y) (at level 60, right associativity).


Program Instance Morphism_Setoid (X Y: Setoid): Setoid :=
  {
    setoid_type := X --> Y;
    setoid_equiv := make_Equivalence (fun f g: X --> Y =>
                                       forall x: X, f x == g x)
                                    _ _ _
  }.
Next Obligation.
  move => X Y f x; by apply equiv_refl.
Qed.
Next Obligation.
  move => X Y f g Heq x; by apply equiv_sym.
Qed.
Next Obligation.
  move => X Y f g h Heqfg Heqgh x;
         move: (Heqfg x) (Heqgh x);
           by apply equiv_trans.
Qed.

Class Modifier :=
  {
    modifier_type X: Setoid;
    modifier_func X Y: X --> Y -> (modifier_type X --> modifier_type Y)
  }.
Coercion modifier_type: Modifier >-> Funclass.

Reserved Notation "x >>= f" (at level 60, right associativity).
Class Monad :=
  {
    monad_modifier: Modifier;
    ret {X: Setoid}: X -> monad_modifier X;
    bind {X Y: Setoid}:
      (X -> monad_modifier Y) -> monad_modifier X -> monad_modifier Y
      where "x >>= f" := (bind f x);
                                                                    
    ret_left:
      forall (X: Setoid)(m: monad_modifier X),
        m >>= ret == m;

    ret_right:
      forall (X Y: Setoid)(x: X)(f: X -> monad_modifier Y),
             f x == (ret x) >>= f
  }.
Coercion monad_modifier: Monad >-> Modifier.
Notation "x >>= f" := (bind f x) (at level 60, right associativity).


Goal (forall (m: Monad)(X: Setoid)(y: m X), (ret y) >>= ret == ret y).
Proof.
  intros; apply ret_left.
Qed.

Program Instance option_Setoid (X: Setoid): Setoid :=
  {
    setoid_type := option X;
    setoid_equiv := eq_Equivalence (option X)
  }.

Program Instance option_Morphism {X Y: Setoid}(f: X --> Y)
: option_Setoid X --> option_Setoid Y
  := {
      morphism_f := fun m => match m with Some x => Some (f x)
                                       | None => None end
    }.
Next Obligation.
  simpl.
  move => X Y f [x |] [x' |] //; congruence.
Qed.

Program Instance option_Modifier: Modifier :=
  {
    modifier_type := option_Setoid;
    modifier_func X Y f := option_Morphism f
  }.

Program Instance Maybe: Monad :=
  {
    monad_modifier := option_Modifier;
    ret X a := Some a;
    bind X Y f m := match m with Some x => f x | _ => None end
  }.
Next Obligation.
  simpl; congruence.
Qed.
Next Obligation.
  simpl.
  move => X [x |] //.
Qed.
Next Obligation.
  simpl.
  move => X Y x f //.
Qed.

(* CAUTION! Stack overflow!!  *)
Check (ret (Monad:=Maybe) 2 == Some 2).