-- List monad

{-# OPTIONS --without-K --safe #-}

module ListMonad where

-- agda-stdlib
open import Data.List
open import Data.List.Properties
import Relation.Binary.PropositionalEquality as ≡

-- agda-categories
open import Categories.Monad
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation
open import Categories.Category.Instance.Sets

List-functor : ∀ {o} → Endofunctor (Sets o)
List-functor = record
  { F₀           = List
  ; F₁           = map
  ; identity     = map-id _
  ; homomorphism = map-compose _
  ; F-resp-≈     = λ f≈g → map-cong (λ _ → f≈g) _
  }

singleton-NT : ∀ {o} → NaturalTransformation idF (List-functor {o})
singleton-NT = record
  { η       = λ X → [_]
  ; commute = λ f → ≡.refl -- [_] ∘ f ≈ map f ∘ [_]
  }

concat-NT : ∀ {o} → NaturalTransformation (List-functor ∘F List-functor) (List-functor {o})
concat-NT = record
  { η       = λ X → concat
  ; commute = λ f {xss} → concat-map {f = f} xss -- concat ∘ map (map f) ≈ map f ∘ concat
  }

concat-++ : ∀ {a} {A : Set a} (xss yss : List (List A)) →
  concat (xss ++ yss) ≡.≡ concat xss ++ concat yss
concat-++ []         yss = ≡.refl
concat-++ (xs ∷ xss) yss = begin
  xs ++ concat (xss ++ yss)        ≡⟨ ≡.cong (xs ++_) (concat-++ xss yss) ⟩
  xs ++ (concat xss ++ concat yss) ≡⟨ ≡.sym (++-assoc xs (concat xss) (concat yss)) ⟩
  (xs ++ concat xss) ++ concat yss ∎
  where open ≡.≡-Reasoning

concat-map-concat : ∀ {a} {A : Set a} (xsss : List (List (List A))) →
  concat (map concat xsss) ≡.≡ concat (concat xsss)
concat-map-concat []           = ≡.refl
concat-map-concat (xss ∷ xsss) = begin
  concat xss ++ concat (map concat xsss) ≡⟨ ≡.cong (concat xss ++_) (concat-map-concat xsss) ⟩
  concat xss ++ concat (concat xsss)     ≡⟨ ≡.sym (concat-++ xss (concat xsss)) ⟩
  concat (xss ++ concat xsss)            ∎
  where open ≡.≡-Reasoning

concat-map-singleton : ∀ {a} {A : Set a} (xs : List A) →
  concat (map [_] xs) ≡.≡ xs
concat-map-singleton []       = ≡.refl
concat-map-singleton (x ∷ xs) = ≡.cong (x ∷_) (concat-map-singleton xs)

concat-singleton : ∀ {a} {A : Set a} (xs : List A) →
  concat [ xs ] ≡.≡ xs
concat-singleton xs = ++-identityʳ xs

List-monad : ∀ {o} → Monad (Sets o)
List-monad = record
  { F         = List-functor
  ; η         = singleton-NT
  ; μ         = concat-NT
  ; assoc     = λ {_ xsss} → concat-map-concat xsss
  ; identityˡ = λ {_ xs} → concat-map-singleton xs
  ; identityʳ = λ {_ xs} → concat-singleton xs
  }