Kleisli Construction of Monads (Equivalency of Category Theory Style and Haskell Style)

coq_kleisli.v

(******************************************************)
(** //// Kliesli Construction of Monads ////          *)
(******************************************************)

Require Import Logic.FunctionalExtensionality.


(*////////////////////////////////////////////////////*)
(** Preliminaries                                     *)
(*////////////////////////////////////////////////////*)

(* Identity morphisms *)
Definition id {a : Type} (x : a) : a := x.

(* Composition of morphisms *)
Definition Mcomp {a b c : Type}
                 (g : b -> c) (f : a -> b) (x : a) : c := g (f x).
Notation "g  [.]  f" := (Mcomp g f)
                        (at level 65, no associativity).

(* Axiom: Categorical endofunctors *)
Class CFunctor (F_obj : Type -> Type)
               (F_arr : forall a b : Type,
                        (a -> b) -> (F_obj a -> F_obj b)) := {
    CF_id :
        forall a : Type, F_arr a a id = id;
    CF_compat :
        forall (a b c : Type) (f : a -> b) (g : b -> c),
        F_arr a c (g [.] f) = F_arr b c g [.] F_arr a b f
}.

(* The identity functor *)
Definition I_obj (a : Type) : Type := a.
Definition I_arr : forall a b : Type,
                   (a -> b) -> (I_obj a -> I_obj b).
Proof.
    intros a b f.
    unfold I_obj.
    assumption.
Defined.

(* [I_obj, I_arr] is a functor. *)
Instance I_CF : CFunctor I_obj I_arr.
Proof.
    apply Build_CFunctor.
    
        (* I_arr maps id to id. *)
        unfold I_arr.
        trivial.
    
        (* I_arr is compatible with [.]. *)
        intros a b c f g.
        unfold I_arr.
        trivial.
Defined.

(* Composition of functors *)
Definition CFcomp (F_obj : Type -> Type)
                  (F_arr : forall a b : Type,
                           (a -> b) -> (F_obj a -> F_obj b))
                  (G_obj : Type -> Type)
                  (G_arr : forall a b : Type,
                           (a -> b) -> (G_obj a -> G_obj b)) :
                  (forall a b : Type,
                   (a -> b) ->
                   ((G_obj [.] F_obj) a -> (G_obj [.] F_obj) b)).
Proof.
    intros a b f.
    unfold Mcomp.
    apply G_arr.
    apply F_arr.
    assumption.
Defined.
Notation "[ F_obj , F_arr ]  [*]  [ G_obj , G_arr ]" :=
          (CFcomp F_obj F_arr G_obj G_arr).

(* Composite of functors is a functor. *)
Lemma CFcomp_CF : forall (F_obj : Type -> Type)
                         (F_arr : forall a b : Type,
                                  (a -> b) -> (F_obj a -> F_obj b))
                         (G_obj : Type -> Type)
                         (G_arr : forall a b : Type,
                                  (a -> b) -> (G_obj a -> G_obj b)),
                  CFunctor F_obj F_arr -> CFunctor G_obj G_arr ->
                  CFunctor (G_obj [.] F_obj)
                           ([F_obj, F_arr] [*] [G_obj, G_arr]).
Proof.
    intros F_obj F_arr G_obj G_arr H_F H_G.
    destruct H_F as [F_id F_compat].
    destruct H_G as [G_id G_compat].
    apply Build_CFunctor.
    
        (* composite maps id to id. *)
        intro a.
        unfold CFcomp.
        rewrite F_id.
        apply G_id.
    
        (* composition is compatible with [.]. *)
        intros a b c f g.
        unfold CFcomp.
        rewrite F_compat.
        rewrite G_compat.
        trivial.
Qed.

(* Axiom: Categorical Natural Transformation *)
Class CNatTrans (F_obj : Type -> Type)
                (F_arr : forall a b : Type,
                         (a -> b) -> (F_obj a -> F_obj b))
                (G_obj : Type -> Type)
                (G_arr : forall a b : Type,
                         (a -> b) -> (G_obj a -> G_obj b))
                (sigma : forall a : Type,
                         (F_obj a -> G_obj a)) := {
    CNT_CF_l :
        CFunctor F_obj F_arr;
    CNT_CF_r :
        CFunctor G_obj G_arr;
    CNT_natural :
        forall (a b : Type) (f : a -> b),
        G_arr a b f [.] sigma a = sigma b [.] F_arr a b f
}.

(* Axiom: Categorical Monad *)
Class CMonad (T_obj : Type -> Type)
             (T_arr : forall a b : Type,
                      (a -> b) -> (T_obj a -> T_obj b))
             (unit : forall a : Type,
                     (I_obj a -> T_obj a))
             (mult : forall a : Type,
                     ((T_obj [.] T_obj) a -> T_obj a)) := {
    CM_CF :
        CFunctor T_obj T_arr;
    CM_unit_CNT :
        CNatTrans I_obj I_arr T_obj T_arr unit;
    CM_mult_CNT :
        CNatTrans (T_obj [.] T_obj)
                  ([T_obj, T_arr] [*] [T_obj, T_arr])
                  T_obj T_arr mult;
    CM_unit_l :
        forall a : Type,
        mult a [.] unit (T_obj a) = id;
    CM_unit_r :
        forall a : Type,
        mult a [.] T_arr (I_obj a) (T_obj a) (unit a) = id;
    CM_mult_assoc :
        forall a : Type,
        mult a [.]
        T_arr ((T_obj [.] T_obj) a) (T_obj a) (mult a) =
        mult a [.]
        mult (T_obj a)
}.

(* Axiom: Haskell Functor *)
Class HFunctor (F : Type -> Type)
               (fmap : forall a b : Type,
                       (a -> b) -> (F a -> F b)) := {
    HF_id :
        forall a : Type, fmap a a id = id;
    HF_compat :
        forall (a b c : Type) (f : a -> b) (g : b -> c),
        fmap a c (g [.] f) = fmap b c g [.] fmap a b f
}.

(* Axiom: Haskell Monad *)
Class HMonad (m : Type -> Type)
             (return' : forall a : Type, a -> m a)
             (bind : forall a b : Type,
                     m a -> (a -> m b) -> m b) := {
    HM_id_l :
        forall (a b : Type) (f : a -> m b) (x : a),
        bind a b (return' a x) f = f x;
    HM_id_r :
        forall (a : Type) (x : m a),
        bind a a x (return' a) = x;
    HM_assoc :
        forall (a b c : Type) (f : a -> m b) (g : b -> m c)
               (x : m a),
        let gf y := bind b c (f y) g in
        bind a c x gf = bind b c (bind a b x f) g
}.


(*////////////////////////////////////////////////////*)
(** Categorical Monad --> Haskell Monad               *)
(*////////////////////////////////////////////////////*)

Section CMonad__HMonad.

(* Let [T, eta, mu] be a categorical monad. *)
Variable T_obj : Type -> Type.
Variable T_arr : forall a b : Type,
                 (a -> b) -> (T_obj a -> T_obj b).
Variable eta : forall a : Type,
               (I_obj a -> T_obj a).
Variable mu : forall a : Type,
              ((T_obj [.] T_obj) a -> T_obj a).
Hypothesis T_CM : CMonad T_obj T_arr eta mu.

(* Construction of the Haskell monad *)
Definition m' := T_obj.
Definition ret' := eta.
Definition star' {a b : Type} (f : a -> m' b) : m' a -> m' b :=
                 mu b [.] T_arr a (T_obj b) f.
Notation "f  [^*']" := (star' f)
                       (at level 30, no associativity).
Definition bind' (a b : Type) (x : m' a) (f : a -> m' b) : m' b :=
                 f [^*'] x.

(* Kleisli property 1 *)
Lemma Kleisli1' : forall a : Type, (ret' a) [^*'] = id.
Proof.
    intro a.
    unfold star'.
    unfold ret'.
    unfold I_obj.
    destruct T_CM as [_ _ _ _ eta_unit_r _].
    unfold I_obj in eta_unit_r.
    apply eta_unit_r.
Qed.

(* Associativity of Mcomp *)
Lemma Mcomp_assoc : forall (a b c d : Type)
                           (f : a -> b) (g : b -> c) (h : c -> d),
                           h [.] (g [.] f) = (h [.] g) [.] f.
Proof.
    intros a b c d f g h.
    unfold Mcomp.
    trivial.
Qed.

(* Kleisli property 2 *)
Lemma Kleisli2' : forall (a b : Type) (f : a -> m' b),
                  f [^*'] [.] ret' a = f.
Proof.
    intros a b f.
    unfold star'.
    unfold ret'.
    destruct T_CM as [_ eta_CNT _ eta_unit_l _ _].
    destruct eta_CNT as [_ _ eta_natural].
    unfold I_obj in *.
    rewrite <- Mcomp_assoc.
    specialize (eta_natural a (T_obj b) f).
    change ((fun y : a =>
                 mu b ((fun x =>
                            (T_arr a (T_obj b) f (eta a x))) y)) =
                             f).
    unfold Mcomp in eta_natural.
    rewrite eta_natural.
    change (mu b [.] (eta (T_obj b) [.] f) = f).
    rewrite Mcomp_assoc.
    rewrite eta_unit_l.
    extensionality x.
    trivial.
Qed.

(* Kleisli property 3 *)
Lemma Kleisli3' : forall (a b c : Type)
                         (f : a -> m' b) (g : b -> m' c),
                  g [^*'] [.] f [^*'] = (g [^*'] [.] f) [^*'].
Proof.
    intros a b c f g.
    unfold star'.
    destruct T_CM as [T_CF _ mu_CNT _ _ mu_assoc].
    destruct T_CF as [_ T_compat].
    destruct mu_CNT as [_ _ mu_natural].
    rewrite Mcomp_assoc.
    change ((mu c [.] (T_arr b (T_obj c) g [.] mu b)) [.]
             T_arr a (T_obj b) f =
             mu c [.]
             T_arr a (T_obj c)
                     ((mu c [.] T_arr b (T_obj c) g) [.]
             f)).
    specialize (mu_natural b (T_obj c) g).
    unfold Mcomp in mu_natural.
    change ((fun y : T_obj (T_obj b) =>
                 mu c ((fun x : T_obj (T_obj b) =>
                            T_arr b (T_obj c) g (mu b x)) y)) [.]
            T_arr a (T_obj b) f =
            mu c [.] T_arr a (T_obj c)
                           ((mu c [.] T_arr b (T_obj c) g) [.] f)).
    rewrite mu_natural.
    change ((mu c [.] (mu (T_obj c) [.]
            [T_obj, T_arr] [*] [T_obj, T_arr] b (T_obj c) g)) [.]
             T_arr a (T_obj b) f =
             mu c [.] T_arr a (T_obj c)
                            ((mu c [.] T_arr b (T_obj c) g) [.] f)).
    rewrite Mcomp_assoc.
    rewrite <- mu_assoc.
    unfold CFcomp.
    repeat rewrite T_compat.
    trivial.
Qed.

(* Haskell monads are obtained from categorical monads. *)
Theorem m'_HM : HMonad m' ret' bind'.
Proof.
    apply Build_HMonad.
    
        (* Left identity law *)
        intros a b f x.
        unfold bind'.
        change ((f [^*'] [.] ret' a) x = f x).
        rewrite Kleisli2'.
        trivial.
    
        (* Right identity law *)
        intros a x.
        unfold bind'.
        specialize (Kleisli1' a).
        intro H_K1'.
        unfold star' in *.
        unfold I_obj in H_K1'.
        rewrite H_K1'.
        trivial.
    
        (* Associativity *)
        intros a b c f g x gf.
        unfold bind' in *.
        specialize (Kleisli3' a b c f g).
        intro H_K3'.
        change ((gf [^*']) x = (g [^*'] [.] f [^*']) x).
        rewrite H_K3'.
        trivial.
Qed.

End CMonad__HMonad.


(*////////////////////////////////////////////////////*)
(** Haskell Monad --> Categorical Monad               *)
(*////////////////////////////////////////////////////*)

Section HMonad__CMonad.

(* Let [m, ret, bind] be a Haskell monad. *)
Variable m : Type -> Type.
Variable ret : forall a : Type, a -> m a.
Variable bind : forall (a b : Type), m a -> (a -> m b) -> m b.
Hypothesis m_HM : HMonad m ret bind.

(* The Kleisli star operator *)
Definition star {a b : Type} (f : a -> m b) (x : m a) : m b :=
                bind a b x f.
Notation "f  [^*]" := (star f)
                      (at level 30, no associativity).

(* Kleisli property 1 *)
Lemma Kleisli1 : forall a : Type, (ret a) [^*] = id.
Proof.
    intro a.
    unfold star.
    extensionality x.
    destruct m_HM as [_ ret_id_r _].
    rewrite ret_id_r.
    trivial.
Qed.

(* Kleisli property 2 *)
Lemma Kleisli2 : forall (a b : Type) (f : a -> m b),
                 f [^*] [.] ret a = f.
Proof.
    intros a b f.
    extensionality x.
    unfold Mcomp.
    unfold star.
    destruct m_HM as [ret_id_l _ _].
    apply ret_id_l.
Qed.

(* Kleisli property 3 *)
Lemma Kleisli3 : forall (a b c : Type)
                        (f : a -> m b) (g : b -> m c),
                 g [^*] [.] f [^*] = (g [^*] [.] f) [^*].
Proof.
    intros a b c f g.
    extensionality x.
    unfold Mcomp.
    unfold star.
    destruct m_HM as [_ _ bind_assoc].
    symmetry.
    trivial.
Qed.

(* Further assumption 1: Haskell monads are Haskell functors. *)
Variable mmap : forall a b : Type, (a -> b) -> (m a -> m b).
Hypothesis m_HF : HFunctor m mmap.

(* Construction of the categorical monad *)
Definition T'_obj := m.
Definition T'_arr (a b : Type) (f : a -> b) :
                  T'_obj a -> T'_obj b :=
                  (ret b [.] f) [^*].
Definition eta' := ret.
Definition mu' (a : Type) : (T'_obj [.] T'_obj) a -> T'_obj a :=
               id [^*].

(* T' is a categorical functor. *)
Instance T'_CF : CFunctor T'_obj T'_arr.
Proof.
    apply Build_CFunctor.
    
        (* T'_arr maps id to id. *)
        intro a.
        unfold T'_arr.
        (* replacement 1 *)
        replace (ret a [.] id) with (ret a).
        apply Kleisli1.
        
            (* proof of the replacement 1 *)
            extensionality x.
            trivial.
    
        (* T'_arr is compatible with [.]. *)
        intros a b c f g.
        unfold T'_arr.
        rewrite Kleisli3.
        change ((ret c [.] (g [.] f)) [^*] =
                (((ret c [.] g) [^*] [.] ret b) [.] f) [^*]).
        rewrite Kleisli2.
        rewrite Mcomp_assoc.
        trivial.
Defined.

(* Further assumption 2: Naturality of ret *)
Hypothesis ret_natural : forall (a b : Type) (f : a -> b),
                         (ret b [.] f) [^*] [.] ret a = ret b [.] f.

(* eta' is a natural transformation. *)
Instance eta'_CNT : CNatTrans I_obj I_arr T'_obj T'_arr eta'.
Proof.
    apply Build_CNatTrans.
    
        (* I is a categorical functor. *)
        apply I_CF.
    
       (* T' is a categorical functor. *)
        apply T'_CF.
    
        (* eta' is a natural transformation *)
        unfold T'_arr.
        unfold I_arr.
        unfold eta'.
        apply ret_natural.
Defined.

(* mu' is a natural transformation. *)
Instance mu'_CNT : CNatTrans (T'_obj [.] T'_obj)
                             ([T'_obj, T'_arr] [*] [T'_obj, T'_arr])
                             T'_obj T'_arr mu'.
Proof.
    apply Build_CNatTrans.
    
        (* T'^2 is a categorical functor. *)
        apply CFcomp_CF.
        apply T'_CF.
        apply T'_CF.
     
        (* T' is a categorical functor. *)
        apply T'_CF.
    
        (* mu' is a natural transformation. *)
        intros a b f.
        unfold CFcomp.
        unfold mu'.
        unfold T'_arr.
        unfold T'_obj.
        apply eq_trans with (((ret b [.] f) [^*]) [^*]).
    
            (* (ret b [.] f) [^*] [.] id [^*] =
               ((ret b [.] f) [^*]) [^*] *)
            specialize (Kleisli3 (m a) a b id (ret b [.] f)).
            intro H_K3.
            unfold Mcomp in *.
            rewrite H_K3.
            trivial.
        
            (* ((ret b [.] f) [^*]) [^*] =
               id [^*] [.]
               (ret (m b) [.] (ret b [.] f) [^*]) [^*] *)
            specialize (Kleisli2 (m b) b id).
            intro H_K2.
            specialize (Kleisli3 (m a) (m b) b
                                 (ret (m b) [.] (ret b [.] f) [^*])
                                 id).
            intro H_K3.
            unfold Mcomp in H_K3.
            unfold Mcomp.
            rewrite H_K3.
            change (((ret b [.] f) [^*]) [^*] =
                    (id [^*] [.]
                     (ret (m b) [.] (ret b [.] f) [^*])) [^*]).
            rewrite Mcomp_assoc.
            rewrite H_K2.
            trivial.
Defined.

(* eta' is the left unit. *)
Lemma eta'_unit_l : forall a : Type,
                    mu' a [.] eta' (T'_obj a) = id.
Proof.
    intro a.
    unfold mu'.
    unfold eta'.
    unfold T'_obj.
    apply Kleisli2.
Qed.

(* eta' is the right unit. *)
Lemma eta'_unit_r : forall a : Type,
                    mu' a [.] T'_arr (I_obj a) (T'_obj a) (eta' a) =
                    id.
Proof.
    intro a.
    unfold mu'.
    unfold eta'.
    unfold I_obj.
    unfold T'_arr.
    unfold T'_obj.
    specialize (Kleisli3 a (m a) a (ret (m a) [.] ret a) id).
    intro H_K3.
    unfold Mcomp in H_K3.
    unfold Mcomp.
    rewrite H_K3.
    change ((id [^*] [.] (ret (m a) [.] ret a)) [^*] = id).
    rewrite Mcomp_assoc.
    rewrite Kleisli2.
    (* replacement 1 *)
    replace (id [.] ret a) with (ret a).
    apply Kleisli1.
    
        (* proof of the replacement 1 *)
        extensionality x.
        trivial.
Qed.

(* mu' is associative. *)
Lemma mu'_assoc : forall a : Type,
                  mu' a [.]
                  T'_arr ((T'_obj [.] T'_obj) a) (T'_obj a)
                         (mu' a) =
                  mu' a [.] mu' (T'_obj a).
Proof.
    intro a.
    unfold mu'.
    unfold T'_arr.
    unfold T'_obj.
    apply eq_trans with ((id [^*]) [^*]).
    
        (* id [^*] [.] (ret (m a) [.] id [^*]) [^*] =
           (id [^*]) [^*] *)
        specialize (Kleisli2 (m a) a id).
        intro H_K2.
        specialize (Kleisli3 (m (m a)) (m a) a
                             (ret (m a) [.] id [^*]) id).
        intro H_K3.
        unfold Mcomp in H_K3.
        unfold Mcomp.
        rewrite H_K3.
        change ((id [^*] [.] (ret (m a) [.] id [^*])) [^*] =
                (id [^*]) [^*]).
        rewrite Mcomp_assoc.
        rewrite H_K2.
        trivial.
    
        (* (id [^*]) [^*] = id [^*] [.] id [^*] *)
        specialize (Kleisli3 (m (m a)) (m a) a id id).
        intro H_K3.
        unfold Mcomp in *.
        rewrite H_K3.
        trivial.
Qed.

(* Categorical monads are obtained from Haskell monads. *)
Theorem T'_CM : CMonad T'_obj T'_arr eta' mu'.
Proof.
    apply Build_CMonad.
    
        (* T' is a functor *)
        apply T'_CF.
    
        (* eta' is a natural transformation *)
        apply eta'_CNT.
    
        (* mu' is a natural transformation *)
        apply mu'_CNT.
    
        (* Left unit law *)
        apply eta'_unit_l.
    
        (* Right unit law *)
        apply eta'_unit_r.
    
        (* Associativity *)
        apply mu'_assoc.
Qed.

End HMonad__CMonad.