The List monad

List.agda

module Categories.Agda.List where

open import Level
open import Categories.Category
open import Categories.Functor using (Functor; module Functor)
open import Categories.NaturalTransformation using (NaturalTransformation; module NaturalTransformation)
open import Categories.Adjunction
open import Categories.Monad
open import Categories.Agda
open import Categories.Support.PropositionalEquality
open import Categories.Support.Irrelevance

open import Algebra
open import Data.List
open import Data.List.Properties
open import Data.Product hiding (map)
open import Relation.Binary.PropositionalEquality

-- concatMap . pure == id
concatMap-pure : ∀ {ℓ} {A : Set ℓ} (xs : List A) → concatMap (λ x → x ∷ []) xs ≡ xs
concatMap-pure [] = refl
concatMap-pure (x ∷ xs) = cong (_∷_ x) (concatMap-pure xs)

-- mconcat
reduce : ∀ {c ℓ} (M : Monoid c ℓ) → (xs : List (Monoid.Carrier M)) → Monoid.Carrier M
reduce M = foldr (Monoid._∙_ M) (Monoid.ε M)

-- The explicit List monad
ListM : ∀ ℓ → Monad (Sets ℓ)
ListM ℓ = record
  { F = record
    { F₀ = List
    ; F₁ = map
    ; identity     = ≣-ext map-id
    ; homomorphism = ≣-ext map-compose
    }
  ; η = record { η = λ _ x → x ∷ []; commute = λ _ → refl }
  ; μ = record { η = λ _ → concat  ; commute = λ _ → ≣-ext concat-map }
  ; assoc     = ≣-ext assoc′
  ; identityˡ = ≣-ext concatMap-pure
  ; identityʳ = ≣-ext (proj₂ (Monoid.identity (monoid _)))
  }
  where
  assoc′ : ∀ {A : Set ℓ} (xs : List (List (List A))) → concat (map concat xs) ≡ concat (concat xs)
  assoc′ [] = refl
  assoc′ ([] ∷ xs₁) = assoc′ xs₁
  assoc′ ((xs ∷ xs₁) ∷ xs₂) = trans (Monoid.assoc (monoid _) xs (concat xs₁) (concat (map concat xs₂))) (cong (_++_ xs) (assoc′ (xs₁ ∷ xs₂)))

-- We're going to need monoid morphisms for our category of monoids. These are simply functions that preserve the monoidal structure: that is, the function must map ε to ε, composition to composition of the mapped parts, and must respect the equivalence relations of the monoids.
record MonoidMorphism {c ℓ} (M₁ M₂ : Monoid c ℓ) : Set (c ⊔ ℓ) where
  constructor monMor
  module M₁ = Monoid M₁
  module M₂ = Monoid M₂
  open M₁ using () renaming (_∙_ to _∙₁_; _≈_ to _≈₁_)
  open M₂ using () renaming (_∙_ to _∙₂_; _≈_ to _≈₂_)
  field
    f : M₁.Carrier → M₂.Carrier
    .identity     : f M₁.ε ≈₂ M₂.ε
    .homomorphism : ∀ x y → f (x ∙₁ y) ≈₂ f x ∙₂ f y
    .congruence   : ∀ {x y} → x ≈₁ y → f x ≈₂ f y

-- Applying the MonoidMorphism function to every element should act the same way as applying it afterwards
.foldr-congruence′ : ∀ {ℓ} {M₁ M₂ : Monoid ℓ ℓ} 
                  (f : MonoidMorphism M₁ M₂) (xs : List (Monoid.Carrier M₁)) → Monoid._≈_ M₂ (reduce M₂ (map (MonoidMorphism.f f) xs)) (MonoidMorphism.f f (reduce M₁ xs))
foldr-congruence′ {M₁ = M₁} {M₂} (monMor f i h c) [] = Monoid.sym M₂ (irr i)
foldr-congruence′ {M₁ = M₁} {M₂} (monMor f i h c) (x ∷ xs)
  = Monoid.trans M₂ (Monoid.∙-cong M₂ (Monoid.refl M₂) (foldr-congruence′ {M₁ = M₁} {M₂} (monMor f i h c) xs)) (Monoid.sym M₂ (irr h x (reduce M₁ xs)))

-- Two MonoidMorphisms are equal if their functions are equal (the proofs are irrelevant)
promote : ∀ {c ℓ} {M₁ M₂ : Monoid c ℓ} {F G : MonoidMorphism M₁ M₂} → MonoidMorphism.f F ≡ MonoidMorphism.f G → F ≡ G
promote {F = monMor f _ _ _} {monMor .f _ _ _} refl = refl

-- The identity MonoidMorphism
id : ∀ {c ℓ} {M : Monoid c ℓ} → MonoidMorphism M M
id {M = M} = monMor (λ x → x) (Monoid.refl M) (λ _ _ → Monoid.refl M) (λ eq → eq)

-- Composition
_∘_ : ∀ {c ℓ} {A B C : Monoid c ℓ} → MonoidMorphism B C → MonoidMorphism A B → MonoidMorphism A C
_∘_ {C = C} (monMor f i h c) (monMor g i′ h′ c′) = monMor (λ x → f (g x)) (C.trans (c i′) i) (λ x y → C.trans (c (h′ x y)) (h (g x) (g y))) (λ eq → c (c′ eq))
  where module C = Monoid C

-- Our category is pretty easy. The one piece to be aware of is that our objects are monoids such that the monoid's equivalence relation is propositional (i.e., Agda-native) equality. This is fine for our purposes because the only things we'll be putting into this category are free monoids that use propositional equality anyway. If we did the more finicky version of this proof we could drop the equality and make our functor from setoids (sets with custom equivalence relations) to monoids.
Monoids : ∀ ℓ → Category (suc ℓ) ℓ
Monoids ℓ = record
  { Obj = Σ[ M ∶ Monoid ℓ ℓ ] (Monoid._≈_ M ≡ _≡_)
  ; _⇒_ = λ f g → MonoidMorphism (proj₁ f) (proj₁ g)
  ; id = id
  ; _∘_ = _∘_
  ; ASSOC = λ _ _ _ → refl
  ; IDENTITYˡ = λ _ → refl
  ; IDENTITYʳ = λ _ → refl
  }

-- Forget the monoidal structure and pull out the underlying set
Forget : ∀ ℓ → Functor (Monoids ℓ) (Sets ℓ)
Forget ℓ = record
  { F₀ = λ M → Monoid.Carrier (proj₁ M)
  ; F₁ = MonoidMorphism.f
  ; identity = refl
  ; homomorphism = refl
  }

-- Make a monoid out of any set (a List). The monoid function in here has signature Set -> Monoid (from Data.List)
Free : ∀ ℓ → Functor (Sets ℓ) (Monoids ℓ)
Free ℓ = record
  { F₀ = λ A → monoid A , refl
  ; F₁ = λ f → monMor (map f) refl (map-++-commute f) (cong (map f))
  ; identity = promote (≣-ext map-id)
  ; homomorphism = promote (≣-ext map-compose)
  }

-- This is the crucial adjunction!
Adj : ∀ ℓ → Adjunction (Free ℓ) (Forget ℓ)
Adj ℓ = record
  { unit   = record { η = λ _ x → x ∷ []; commute = λ _ → refl } -- unit is pure
  ; counit = record -- counit is mconcat wrapped up in a monoid morphism
    { η = λ M → monMor (reduce (proj₁ M)) (Monoid.refl (proj₁ M)) (homomorphism′ M) (congruence′ M)
    ; commute = λ {X} {Y} f → promote (≣-ext (λ xs → conv Y (foldr-congruence′ {M₁ = proj₁ X} {proj₁ Y} f xs)))
    }
  ; zig = promote (≣-ext (λ xs → sym (concatMap-pure xs)))
  ; zag = λ {M} → ≣-ext (zag′ M)
  }
  where
  -- Some lemmas/helpers
  module Dummy (M : Σ[ M ∶ Monoid ℓ ℓ ] (Monoid._≈_ M ≡ _≡_)) where
    module M = Monoid (proj₁ M)
    open Monoid (proj₁ M) hiding (refl; sym; trans)

    reduce′ = reduce (proj₁ M)

    conv : ∀ {x y} → x ≈ y → x ≡ y
    conv {x} {y} = subst (λ q → q x y) (proj₂ M)

    homomorphism′ : (xs ys : List Carrier) → reduce′ (xs ++ ys) ≈ reduce′ xs ∙ reduce′ ys
    homomorphism′ [] ys = M.sym (proj₁ identity _)
    homomorphism′ (x ∷ xs) ys = M.trans (∙-cong M.refl (homomorphism′ xs ys)) (M.sym (M.assoc x (reduce′ xs) (reduce′ ys)))

    congruence′ : {x y : List Carrier} → x ≡ y → reduce′ x ≈ reduce′ y
    congruence′ {M} refl = M.refl

    zag′ : ∀ x → x ≡ x ∙ ε
    zag′ x = sym (conv (proj₂ identity x))

  open Dummy

-- This is the list monad that we get from our adjunction
ListM′ : ∀ ℓ → Monad (Sets ℓ)
ListM′ ℓ = Adjunction.monad (Adj ℓ)

-- Lo! The monads are equal! Once again we can use propositional equality because although I used a pattern-matching function like foldr, I was careful to use the same ones so the definitions reduce to the same thing. The proofs are obviously going to be different but they're irrelevant so they don't break our equality.
proof : ∀ ℓ → ListM ℓ ≡ ListM′ ℓ
proof ℓ = refl