List functor/monad (à la copumpkin/categories)

List.agda

module List where
  open import Categories.Agda
  import Categories.Functor as F
  import Categories.Monad as M
  import Categories.NaturalTransformation as NT
  open import Data.List as List
  open import Function using (id; _∘_)
  open import Relation.Binary.PropositionalEquality hiding ([_])

-- Utility

  open ≡-Reasoning
  open import Data.List.Properties using (concat-map)

  private
    xrefl : ∀ {a} {A : Set a} (x : A) → x ≡ x
    xrefl x = refl

    module ++-Props {ℓ} {A : Set ℓ} where
      open import Data.Product
      open import Algebra using (Monoid)
      open Algebra.Monoid (monoid A) hiding (∙-cong)
      open Algebra.Monoid (monoid A) public using () renaming (∙-cong to ++-cong)
      import Relation.Binary.PropositionalEquality as PropEq

      ++-[] : ∀ (x : List A) → x ++ [] ≡ x
      ++-[] = proj₂ identity

      distrib-concat-++ : ∀ (x y : List (List A))
                        → concat (x ++ y) ≡ concat x ++ concat y
      distrib-concat-++ []        y = PropEq.refl
      distrib-concat-++ (x₀ ∷ xₛ) y = begin
        concat ((x₀ ∷ xₛ) ++ y)       ≡⟨⟩
        concat (x₀ ∷ (xₛ ++ y))       ≡⟨⟩
        x₀ ++ concat (xₛ ++ y)        ≡⟨ ++-cong (xrefl x₀) (distrib-concat-++ xₛ y) ⟩
        x₀ ++ (concat xₛ ++ concat y) ≡⟨ PropEq.sym (assoc x₀ (concat xₛ) (concat y)) ⟩
        (x₀ ++ concat xₛ) ++ concat y ≡⟨⟩
        concat (x₀ ∷ xₛ) ++ concat y  ∎

    open ++-Props

-- List functor

  ListFunctor : ∀ {ℓ} → F.Endofunctor (Sets ℓ)
  ListFunctor {ℓ} = record {
      F₀           = List ;
      F₁           = map ;
      identity     = identity ;
      homomorphism = homomorphism ;
      F-resp-≡     = F-resp-≡
    }
    where
      identity : ∀ {A : Set ℓ}
               → ∀ {x : List A} → map id x ≡ id x
      identity {x = []}    = refl
      identity {x = _ ∷ _} = cong₂ _∷_ refl identity

      homomorphism : ∀ {X Y Z : Set ℓ} {f : X → Y} {g : Y → Z}
                   → ∀ {x} → map (g ∘ f) x ≡ (map g ∘ map f) x
      homomorphism {x = []}    = refl
      homomorphism {x = _ ∷ _} = cong₂ _∷_ refl homomorphism

      F-resp-≡ : ∀ {A B : Set ℓ} {f g : A → B}
               → (∀ {x} →     f x ≡     g x)
               → (∀ {x} → map f x ≡ map g x)
      F-resp-≡ f~g {x = []}    = refl
      F-resp-≡ f~g {x = _ ∷ _} = cong₂ _∷_ f~g (F-resp-≡ f~g)

-- List monad

  ListMonad : ∀ {ℓ} → M.Monad (Sets ℓ)
  ListMonad {ℓ} = record {
      F         = ListFunctor ;
      η         = η ;
      μ         = μ ;
      assoc     = λ {A} {x} → assoc {A} {x} ;
      identityˡ = idˡ ;
      identityʳ = idʳ
    }
    where
      η : NT.NaturalTransformation F.id ListFunctor
      η = record {
          η       = λ _ → [_] ;
          commute = λ _ → refl
        }

      μ : NT.NaturalTransformation (ListFunctor F.∘ ListFunctor) ListFunctor
      μ = record {
          η       = λ _     → concat ;
          commute = λ _ {x} → concat-map x
        }

      assoc : ∀ {A : Set ℓ} {x : List (List (List A))}
            → (concat ∘ map concat) x ≡ (concat ∘ concat) x
      assoc {x = []}      = refl
      assoc {x = x₀ ∷ xₛ} = begin
        (concat ∘ map concat) (x₀ ∷ xₛ)       ≡⟨⟩
        concat (map concat (x₀ ∷ xₛ))         ≡⟨⟩
        concat (concat x₀ ∷ map concat xₛ)    ≡⟨⟩
        concat x₀ ++ (concat ∘ map concat) xₛ ≡⟨ ++-cong (xrefl (concat x₀)) (assoc {x = xₛ}) ⟩
        concat x₀ ++ (concat ∘ concat) xₛ     ≡⟨ sym (distrib-concat-++ x₀ (concat xₛ)) ⟩
        concat (x₀ ++ concat xₛ)              ≡⟨⟩
        concat (concat (x₀ ∷ xₛ))             ≡⟨⟩
        (concat ∘ concat) (x₀ ∷ xₛ)           ∎

      idˡ : ∀ {A : Set ℓ} {x : List A}
          → (concat ∘ map [_]) x ≡ id x
      idˡ {x = []}      = refl
      idˡ {x = x₀ ∷ xₛ} = begin
        (concat ∘ map List.[_]) (x₀ ∷ xₛ) ≡⟨⟩
        concat ([ x₀ ] ∷ map [_] xₛ)      ≡⟨⟩
        [ x₀ ] ++ concat (map [_] xₛ)     ≡⟨ ++-cong (xrefl [ x₀ ]) idˡ ⟩
        [ x₀ ] ++ xₛ                      ≡⟨⟩
        x₀ ∷ xₛ                           ∎

      idʳ : ∀ {A : Set ℓ} {x : List A}
          → (concat ∘ [_]) x ≡ id x
      idʳ {x = []}      = refl
      idʳ {x = x₀ ∷ xₛ} = begin
        (concat ∘ [_]) (x₀ ∷ xₛ) ≡⟨⟩
        concat [ x₀ ∷ xₛ ]       ≡⟨⟩
        (x₀ ∷ xₛ) ++ concat []   ≡⟨⟩
        (x₀ ∷ xₛ) ++ []          ≡⟨ ++-[] (x₀ ∷ xₛ) ⟩
        x₀ ∷ xₛ                  ∎