ExtLib.Structures.MonadLaws

Require Import Setoid.
Require Import Coq.Classes.Morphisms.
Require Import ExtLib.Structures.Monads.
Require Import ExtLib.Data.Fun.
Require Import ExtLib.Data.Unit.

Set Implicit Arguments.
Set Strict Implicit.

Section MonadLaws.
  Variable m : Type -> Type.
  Variable M : Monad m.

  Class MonadLaws :=
  { bind_of_return : forall {A B} (a : A) (f : A -> m B),
      bind (ret a) f = f a
  ; bind_associativity :
      forall {A B C} (aM:m A) (f:A -> m B) (g:B -> m C),
        bind (bind aM f) g = bind aM (fun a => bind (f a) g)
  }.

  Class MonadTLaws {n} (nM : Monad n) (MT : MonadT m n) :=
  { lift_ret : forall {T} (x : T),
      lift (ret x) = ret x
  ; lift_bind : forall {T U} (c : n T) (f : T -> n U),
      lift (bind c f) = bind (lift c) (fun x => lift (f x))
  }.

  Section with_state.
    Context {S : Type}.

    Class MonadStateLaws (MS : MonadState S m) : Type :=
    { get_put : bind get put = ret tt
    ; put_get : forall x : S,
        bind (put x) (fun _ => get) = bind (put x) (fun _ => ret x)
    ; put_put : forall {A} (x y : S) (f : unit -> m A),
        bind (put x) (fun _ => bind (put y) f) = bind (put y) f
    ; get_get : forall {A} (f : S -> S -> m A),
        bind get (fun s => bind get (f s)) = bind get (fun s => f s s)
    ; get_ignore : forall {A} (aM : m A),
        bind get (fun _ => aM) = aM
    }.

    Class MonadReaderLaws (MR : MonadReader S m) : Type :=
    { ask_local : forall f : S -> S,
        local f ask = bind ask (fun x => ret (f x))
    ; local_bind : forall {A B} (aM : m A) (f : S -> S) (g : A -> m B),
          local f (bind aM g) = bind (local f aM) (fun x => local f (g x))
    ; local_ret : forall {A} (x : A) (f : S -> S),
        local f (ret x) = ret x
    ; local_local : forall {T} (s s' : S -> S) (c : m T),
        local s (local s' c) = local (fun x => s' (s x)) c
    }.

  End with_state.

  Class MonadZeroLaws (MZ : MonadZero m) : Type :=
  { bind_zero : forall {A B} (f : A -> m B),
      bind mzero f = mzero
  }.

  Class MonadFixLaws (MF : MonadFix m) : Type :=
  { mleq : forall {T}, relation T -> relation (m T)
  ; mfix_monotonic : forall {T U} (F : (T -> m U) -> T -> m U),
    respectful eq (mleq eq) (mfix F) (F (mfix F))
  }.

End MonadLaws.