freemonoid.v

(* The free monoid functor ([list]) is a monad *)

Set Implicit Arguments.
Set Contextual Implicit.
Set Maximal Implicit Insertion.

From Coq Require Import
  List
  Setoid
  Morphisms.
Import ListNotations.

Record Category : Type :=
  { obj :> Type
  ; hom : obj -> obj -> Type
  ; eq_hom : forall {a b : obj},
      hom a b -> hom a b -> Prop
  ; Equivalence_eq_hom : forall {a b : obj},
      Equivalence (@eq_hom a b)
  ; id : forall {a : obj},
      hom a a
  ; cat : forall {a b c : obj},
      hom a b -> hom b c -> hom a c
  ; Proper_cat : forall {a b c : obj},
      Proper (eq_hom ==> eq_hom ==> eq_hom) (@cat a b c)
  ; cat_append_empty_l : forall {a b : obj} (f : hom a b),
      eq_hom (cat id f) f
  ; cat_append_empty_r : forall {a b : obj} (f : hom a b),
      eq_hom (cat f id) f
  ; cat_assoc : forall {a b c d : obj} (f : hom a b) (g : hom b c) (h : hom c d),
      eq_hom (cat (cat f g) h) (cat f (cat g h))
  }.

Existing Instance Equivalence_eq_hom.

Generalizable Variables C D E.
Implicit Types C D E : Category.

Declare Scope cat_scope.
Delimit Scope cat_scope with cat.

Infix "=~" := (eq_hom _) (at level 70) : cat_scope.
Infix ">>>" := (cat _) (at level 50) : cat_scope.

Local Open Scope cat.

Record Functor (C D : Category) : Type :=
  { map_obj :> C -> D
  ; map : forall {a b : C},
      hom C a b -> hom D (map_obj a) (map_obj b)
  ; Proper_map :> forall {a b : C},
      Proper (eq_hom C ==> eq_hom D) (@map a b)
  ; map_id : forall {a : C},
      map (id C (a := a)) =~ id D
  ; map_cat : forall {a b c : C} (f : hom C a b) (g : hom C b c),
      map (f >>> g) =~ map f >>> map g
  }.

Existing Instance Proper_map.

Generalizable Variables F G M.

(* Unit-counit adjunction *)
Record Adjunction C D (F : Functor D C) (G : Functor C D) : Type :=
  { counit : forall {a : C},
      hom C (F (G a)) a
  ; unit : forall {a : D},
      hom D a (G (F a))
  ; adj_FGF : forall {a : D},
      map F unit >>> counit =~ id C (a := F a)
  ; adj_GFG : forall {a : C},
      unit >>> map G counit =~ id D (a := G a)
  ; natural_counit : forall {a b : C} (f : hom C a b),
      map F (map G f) >>> counit =~ counit >>> f
  ; natural_unit : forall {a b : D} (f : hom D a b),
      f >>> unit =~ unit >>> map G (map F f)
  }.

Arguments counit {C D F G} A {a} : rename.
Arguments unit {C D F G} A {a} : rename.

(* Extra (unused): Hom-set adjunction *)
Record HAdjunction `(F : Functor D C) (G : Functor C D) : Type :=
  { forget : forall {a : D} {b : C},
      hom C (F a) b -> hom D a (G b)
  ; generate : forall {a : D} {b : C},
      hom D a (G b) -> hom C (F a) b
  ; forget_generate : forall {a : D} {b : C} (h : hom C (F a) b),
      generate (forget h) =~ h
  ; generate_forget : forall {a : D} {b : C} (h : hom D a (G b)),
      forget (generate h) =~ h
    (* TODO: naturality *)
  }.

Record Monad (C : Category) : Type :=
  { asFunctor :> Functor C C
  ; F := asFunctor
  ; ret : forall {a : C}, hom C a (F a)
  ; join : forall {a : C}, hom C (F (F a)) (F a)
  ; ret_join : forall {a : C},
      ret >>> join (a := a) =~ id C
  ; map_ret_join : forall {a : C},
      map F ret >>> join (a := a) =~ id C
  ; join_join : forall {a : C},
      map F (join (a := a)) >>> join =~ join >>> join
  ; natural_ret : forall {a b : C} (f : hom C a b),
      f >>> ret =~ ret >>> map F f
  ; natural_join : forall {a b : C} (f : hom C a b),
      map F (map F f) >>> join =~ join >>> map F f
  }.

Declare Scope eq_scope.
Delimit Scope eq_scope with eq.
Infix ">>>" := transitivity : eq_scope.

Definition composeF `(G : Functor D E) `(F : Functor C D) : Functor C E :=
  {| map_obj := fun c => G (F c)
   ; map := fun a b f => map G (map F f)
   ; Proper_map := fun a b f f' Ef => Proper_map G _ _ (Proper_map F f f' Ef)
   ; map_id := fun a => (Proper_map G _ _ (map_id F) >>> map_id G)%eq
   ; map_cat := fun a b c f g => (Proper_map G _ _ (map_cat F f g) >>> map_cat G _ _)%eq
  |}.

(* [rw] vs [rewrite]:
   Con:
     [rw] requires an equation with the same LHS as the goal,
     whereas [rewrite] only needs an equation on a subterm of the goal (whether LHS or
     RHS, it doesn't even have to be an equation) and automatically infers a
     [Proper] instance for the context;
   Pro:
     [rw] can unify the LHSs of the given equation and the goal up to convertibility,
     whereas [rewrite] pretty much requires the LHSs to match exactly. *)
Tactic Notation "rw" uconstr(H) := apply (transitivity H).
Tactic Notation "rw" "<-" uconstr(H) := apply (transitivity (symmetry H)).

Definition Monad_Adjunction `(F : Functor D C) `(G : Functor C D) (FG : Adjunction F G)
  : Monad D.
Proof. refine
  {| asFunctor := composeF G F
   ; ret := fun a => unit FG (a := a)
   ; join := fun a => map G (counit FG (a := F a))
  |}.
  - (* ret_join *) intros a.
    exact (adj_GFG FG).
  - (* map_ret_join *) intros a.
    rw <- (map_cat G _ _).
    rw (Proper_map G _ _ (adj_FGF FG)).
    rw (map_id G).
    reflexivity.
  - (* join_join *) intros a.
    rw <- (map_cat G _ _).
    rw (Proper_map G _ _ (natural_counit FG _)).
    rw (map_cat G _ _).
    reflexivity.
  - (* natural_ret *) intros a b f.
    exact (natural_unit FG f).
  - (* natural_join *) intros a b f.
    rw <- (map_cat G _ _).
    rw (Proper_map G _ _ (natural_counit FG _)).
    rw (map_cat G _ _).
    reflexivity.
Defined.

(* As one big term. *)
Definition Monad_Adjunction_2 `(F : Functor D C) `(G : Functor C D) (FG : Adjunction F G)
  : Monad D :=
  {| asFunctor := composeF G F
   ; ret := fun a => unit FG (a := a) : hom D a (composeF G F a)
   ; join := fun a => map G (counit FG (a := F a))
   ; ret_join := fun a => adj_GFG FG
   ; map_ret_join := fun a => 
       ( symmetry (map_cat G _ _) >>>
         Proper_map G _ _ (adj_FGF FG) >>>
         map_id G )%eq
   ; join_join := fun a =>
       ( symmetry (map_cat G _ _) >>>
         Proper_map G _ _ (natural_counit FG _) >>>
         map_cat G _ _ )%eq
   ; natural_ret := fun a b f => natural_unit FG f
   ; natural_join := fun a b f =>
       ( symmetry (map_cat G _ _) >>>
         Proper_map G _ _ (natural_counit FG _) >>>
         map_cat G _ _ )%eq
  |}.

Definition eq_fun (a b : Type) (f g : a -> b) : Prop :=
  forall x, f x = g x.

Definition Equivalence_fun {a b : Type} : Equivalence (@eq_fun a b) :=
  Equivalence.pointwise_equivalence eq_equivalence.

Import EqNotations.

Definition ap_eq {a b : Type} {f g : a -> b} {x y : a} (Ef : eq_fun f g) (Ex : x = y) : f x = g y :=
  rew [fun y => f x = g y] Ex in
  rew Ef x in
  eq_refl.

Definition TYPE : Category :=
  {| obj := Type
   ; hom := fun a b => a -> b
   ; eq_hom := @eq_fun
   ; Equivalence_eq_hom := @Equivalence_fun
   ; id := fun a x => x
   ; cat := fun a b c f g x => g (f x)
   ; Proper_cat := fun a b c f f' Ef g g' Eg x =>
       ap_eq Eg (ap_eq Ef eq_refl)
   ; cat_append_empty_l := fun a b f x => eq_refl
   ; cat_append_empty_r := fun a b f x => eq_refl
   ; cat_assoc := fun a b c d f g h x => eq_refl
  |}.

Canonical TYPE.

Record Monoid : Type :=
  { carrier :> Type
  ; append : carrier -> carrier -> carrier
  ; empty : carrier
  ; append_empty_l : forall x, append empty x = x
  ; append_empty_r : forall x, append x empty = x
  ; append_assoc : forall x y z, append (append x y) z = append x (append y z)
  }.

Record monoid_morphism (a b : Monoid) :=
  { morphism_carrier :> a -> b
  ; morphism_empty : morphism_carrier (empty a) = empty b
  ; morphism_append : forall {x y : a},
      morphism_carrier (append a x y) = append b (morphism_carrier x) (morphism_carrier y)
  }.

Definition Equivalence_projection {a b : Type} (f : a -> b) (r : b -> b -> Prop)
    (EQ : Equivalence r)
  : Equivalence (fun x y => r (f x) (f y)).
Proof.
  constructor.
  - intros x; reflexivity.
  - intros x y H; symmetry; apply H.
  - intros x y z H1 H2; etransitivity; eassumption.
Qed.

Definition id_morphism (a : Monoid) : monoid_morphism a a :=
  {| morphism_carrier := fun x => x
   ; morphism_empty := eq_refl
   ; morphism_append := fun x y => eq_refl
  |}.

Definition cat_morphism (a b c : Monoid) (f : monoid_morphism a b) (g : monoid_morphism b c)
  : monoid_morphism a c :=
  {| morphism_carrier := fun x => g (f x)
   ; morphism_empty := (f_equal g (morphism_empty f) >>> morphism_empty g)%eq
   ; morphism_append := fun x y => (f_equal g (morphism_append f) >>> morphism_append g)%eq
  |}.

Definition MONOID : Category :=
  {| obj := Monoid
   ; hom := monoid_morphism
   ; eq_hom := @eq_fun
   ; Equivalence_eq_hom := fun a b => Equivalence_projection morphism_carrier Equivalence_fun
   ; id := @id_morphism
   ; cat := @cat_morphism
   ; Proper_cat := fun a b c f f' Ef g g' Eg x =>
       ap_eq Eg (ap_eq Ef eq_refl)
   ; cat_append_empty_l := fun a b f x => eq_refl
   ; cat_append_empty_r := fun a b f x => eq_refl
   ; cat_assoc := fun a b c d f g h x => eq_refl
  |}.

Canonical MONOID.

Definition list_monoid (a : Type) : Monoid :=
  {| carrier := list a
   ; empty := nil
   ; append := app (A := a)
   ; append_empty_l := app_nil_l (A := a)
   ; append_empty_r := app_nil_r (A := a)
   ; append_assoc := fun x y z => eq_sym (app_assoc (A := a) x y z)
  |}.

Canonical list_monoid.

Definition map_list_monoid (a b : Type) (f : a -> b)
  : monoid_morphism (list_monoid a) (list_monoid b) :=
  {| morphism_carrier := List.map f
   ; morphism_empty := eq_refl
   ; morphism_append := List.map_app f
  |}.

Definition LIST : Functor TYPE MONOID :=
  {| map_obj := list_monoid
   ; map := fun a b => map_list_monoid
   ; Proper_map := fun a b f f' Ef => List.map_ext f f' Ef
   ; map_id := List.map_id
   ; map_cat := fun a b c f g l => eq_sym (map_map f g l)
  |}.

Definition FORGET : Functor MONOID TYPE :=
  {| map_obj := carrier
   ; map := fun a b => morphism_carrier
   ; Proper_map := fun a b f f' Ef => Ef
   ; map_id := fun a x => eq_refl
   ; map_cat := fun a b c f g l => eq_refl
  |}.

Fixpoint fold (M : Monoid) (xs : list M) : M :=
  match xs with
  | [] => empty M
  | x :: xs => append M x (fold M xs)
  end.

Lemma fold_append (M : Monoid) (xs ys : list M)
  : fold M (xs ++ ys) = append M (fold M xs) (fold M ys).
Proof.
  induction xs; cbn.
  - rewrite append_empty_l. reflexivity.
  - rewrite append_assoc. f_equal. assumption.
Qed.

Definition fold_map_monoid (M : Monoid) : monoid_morphism (LIST (FORGET M)) M :=
  {| morphism_carrier := fold M
   ; morphism_empty := eq_refl
   ; morphism_append := fold_append M
  |}.

Definition Adjunction_LIST_FORGET : Adjunction LIST FORGET.
Proof. refine
  {| counit := @fold_map_monoid
   ; unit := fun a x => [x]
  |}.
  - (* FGF *) intros a. cbn. intros xs.
    induction xs; cbn.
    + reflexivity.
    + f_equal. assumption.
  - (* GFG *) intros M. cbn. intros xs.
    apply append_empty_r.
  - (* natural_counit *) intros M N f. cbn. intros xs.
    induction xs; cbn.
    + rewrite morphism_empty. reflexivity.
    + rewrite morphism_append. f_equal. assumption.
  - (* natural_unit *) intros a b f. cbn. intros x.
    reflexivity.
Defined.

(* What Haskellers call "Monad" *)
Class TypeMonad (m : Type -> Type) : Type :=
  { tret : forall {a}, a -> m a
  ; tjoin : forall {a}, m (m a) -> m a
  ; tmap : forall {a b}, (a -> b) -> m a -> m b
  ; tret_tjoin : forall {a} (u : m a),
      tjoin (tret u) = u
  ; tmap_tret_tjoin : forall {a} (u : m a),
      tjoin (tmap tret u) = u
  ; tjoin_tjoin : forall {a} (u : m (m (m a))),
      tjoin (tmap tjoin u) = tjoin (tjoin u)
  ; tret_tmap : forall {a b} (f : a -> b) (x : a),
      tmap f (tret x) = tret (f x)
  ; tjoin_tmap : forall {a b} (f : a -> b) (u : m (m a)),
      tmap f (tjoin u) = tjoin (tmap (tmap f) u)
  ; tmap_id : forall {a} (u : m a),
      tmap (fun x => x) u = u
  ; tmap_compose : forall {a b c} (f : a -> b) (g : b -> c) (u : m a),
      tmap (fun x => g (f x)) u = tmap g (tmap f u)
  }.

Definition bind {m : Type -> Type} `{TypeMonad m} {a b : Type}
    (u : m a) (k : a -> m b) : m b :=
  tjoin (tmap k u).

Declare Scope monad_scope.
Delimit Scope monad_scope with monad.
Local Open Scope monad_scope.

Infix ">>=" := bind (at level 60) : monad_scope.

Definition TypeMonad_Monad (M : Monad TYPE) : TypeMonad M :=
  {| tret := fun a => ret M
   ; tjoin := fun a => join M
   ; tmap := fun a b f => map M f
   ; tret_tjoin := fun a => ret_join M
   ; tmap_tret_tjoin := fun a => map_ret_join M
   ; tjoin_tjoin := fun a => join_join M
   ; tret_tmap := fun a b f => symmetry (natural_ret M f)
   ; tjoin_tmap := fun a b f => symmetry (natural_join M f)
   ; tmap_id := fun a => map_id M
   ; tmap_compose := fun a b c => map_cat M
  |}.

Instance TypeMonad_list : TypeMonad list :=
  TypeMonad_Monad (Monad_Adjunction Adjunction_LIST_FORGET).

Print Assumptions TypeMonad_list.

Compute [1; 2; 3] >>= fun n => repeat n n.
Compute (tret 3 : list nat).