monad_coercion.v

(* Monad with Coercion *)

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

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:
      forall a, a == a;
    equiv_sym:
      forall a b, a == b -> b == a;
    equiv_trans:
      forall a b c, a == b -> b == c -> a == c
  }.
Coercion equiv_eq: Equivalence >-> relation.
Notation "x == y" := (equiv_eq x y) (at level 85, no associativity).

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

Class Modifier :=
  {
    modifier_f: Setoid -> Setoid;

    modifier_equiv (X: Setoid): Equivalence (modifier_f X)
  }.
Coercion modifier_f: Modifier >-> Funclass.
Existing Instance modifier_equiv.

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.