------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of List
------------------------------------------------------------------------

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

module Data.List.Categorical where

open import Category.Functor
open import Category.Applicative
open import Category.Monad
open import Data.Bool.Base using (false; true)
open import Data.List
open import Data.List.Properties
open import Function
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; _≗_; refl)
open P.≡-Reasoning

------------------------------------------------------------------------
-- List applicative functor

functor :  {}  RawFunctor {} List
functor = record { _<$>_ = map }

applicative :  {}  RawApplicative {} List
applicative = record
  { pure = [_]
  ; _⊛_  = λ fs as  concatMap  f  map f as) fs
  }

applicativeZero :  {}  RawApplicativeZero {} List
applicativeZero = record
  { applicative = applicative
  ;            = []
  }

alternative :  {}  RawAlternative {} List
alternative = record
  { applicativeZero = applicativeZero
  ; _∣_             = _++_
  }

------------------------------------------------------------------------
-- List monad

monad :  {}  RawMonad {} List
monad = record
  { return = [_]
  ; _>>=_  = flip concatMap
  }

monadZero :  {}  RawMonadZero {} List
monadZero = record
  { monad           = monad
  ; applicativeZero = applicativeZero
  }

monadPlus :  {}  RawMonadPlus {} List
monadPlus = record
  { monad = monad
  ; alternative = alternative
  }

------------------------------------------------------------------------
-- Get access to other monadic functions

module TraversableA {f F} (App : RawApplicative {f} F) where

  open RawApplicative App

  sequenceA :  {A}  List (F A)  F (List A)
  sequenceA []       = pure []
  sequenceA (x  xs) = _∷_ <$> x  sequenceA xs

  mapA :  {a} {A : Set a} {B}  (A  F B)  List A  F (List B)
  mapA f = sequenceA  map f

  forA :  {a} {A : Set a} {B}  List A  (A  F B)  F (List B)
  forA = flip mapA

module TraversableM {m M} (Mon : RawMonad {m} M) where

  open RawMonad Mon

  open TraversableA rawIApplicative public
    renaming
    ( sequenceA to sequenceM
    ; mapA      to mapM
    ; forA      to forM
    )

------------------------------------------------------------------------
-- List monad transformer

monadT :  {}  RawMonadT {} (_∘′ List)
monadT M = record
  { return = pure ∘′ [_]
  ; _>>=_  = λ mas f  mas >>= λ as  concat <$> mapM f as
  } where open RawMonad M; open TraversableM M

------------------------------------------------------------------------
-- The list monad.

private
  open module LMP {} = RawMonadPlus (monadPlus { = })

module MonadProperties where

  left-identity :  {} {A B : Set } (x : A) (f : A  List B) 
                  (return x >>= f)  f x
  left-identity x f = ++-identityʳ (f x)

  right-identity :  {} {A : Set } (xs : List A) 
                   (xs >>= return)  xs
  right-identity []       = refl
  right-identity (x  xs) = P.cong (x ∷_) (right-identity xs)

  left-zero :  {} {A B : Set } (f : A  List B)  ( >>= f)  
  left-zero f = refl

  right-zero :  {} {A B : Set } (xs : List A) 
               (xs >>= const )   {A = B}
  right-zero []       = refl
  right-zero (x  xs) = right-zero xs

  private

    not-left-distributive :
      let xs = true  false  []; f = return; g = return in
      (xs >>= λ x  f x  g x)  ((xs >>= f)  (xs >>= g))
    not-left-distributive ()

  right-distributive :  {} {A B : Set }
                       (xs ys : List A) (f : A  List B) 
                       (xs  ys >>= f)  ((xs >>= f)  (ys >>= f))
  right-distributive []       ys f = refl
  right-distributive (x  xs) ys f = begin
    f x  (xs  ys >>= f)              ≡⟨ P.cong (f x ∣_) $ right-distributive xs ys f 
    f x  ((xs >>= f)  (ys >>= f))    ≡⟨ P.sym $ ++-assoc (f x) _ _ 
    ((f x  (xs >>= f))  (ys >>= f))  

  associative :  {} {A B C : Set }
                (xs : List A) (f : A  List B) (g : B  List C) 
                (xs >>= λ x  f x >>= g)  (xs >>= f >>= g)
  associative []       f g = refl
  associative (x  xs) f g = begin
    (f x >>= g)  (xs >>= λ x  f x >>= g)  ≡⟨ P.cong ((f x >>= g) ∣_) $ associative xs f g 
    (f x >>= g)  (xs >>= f >>= g)          ≡⟨ P.sym $ right-distributive (f x) (xs >>= f) g 
    (f x  (xs >>= f) >>= g)                

  cong :  {} {A B : Set } {xs₁ xs₂} {f₁ f₂ : A  List B} 
         xs₁  xs₂  f₁  f₂  (xs₁ >>= f₁)  (xs₂ >>= f₂)
  cong {xs₁ = xs} refl f₁≗f₂ = P.cong concat (map-cong f₁≗f₂ xs)

------------------------------------------------------------------------
-- The applicative functor derived from the list monad.

-- Note that these proofs (almost) show that RawIMonad.rawIApplicative
-- is correctly defined. The proofs can be reused if proof components
-- are ever added to RawIMonad and RawIApplicative.

module Applicative where

  private

    module MP = MonadProperties

    -- A variant of flip map.

    pam :  {} {A B : Set }  List A  (A  B)  List B
    pam xs f = xs >>= return  f

  -- ∅ is a left zero for _⊛_.

  left-zero :  {} {A B : Set } (xs : List A)  (  xs)   {A = B}
  left-zero xs = begin
      xs          ≡⟨⟩
    ( >>= pam xs)  ≡⟨ MonadProperties.left-zero (pam xs) 
                   

  -- ∅ is a right zero for _⊛_.

  right-zero :  {} {A B : Set } (fs : List (A  B))  (fs  )  
  right-zero {} fs = begin
    fs              ≡⟨⟩
    (fs >>= pam )    ≡⟨ (MP.cong (refl {x = fs}) λ f 
                          MP.left-zero (return  f)) 
    (fs >>= λ _  )  ≡⟨ MP.right-zero fs 
                     

  -- _⊛_ distributes over _∣_ from the right.

  right-distributive :  {} {A B : Set } (fs₁ fs₂ : List (A  B)) xs 
                       ((fs₁  fs₂)  xs)  (fs₁  xs  fs₂  xs)
  right-distributive fs₁ fs₂ xs = begin
    (fs₁  fs₂)  xs                     ≡⟨⟩
    (fs₁  fs₂ >>= pam xs)               ≡⟨ MonadProperties.right-distributive fs₁ fs₂ (pam xs) 
    (fs₁ >>= pam xs)  (fs₂ >>= pam xs)  ≡⟨⟩
    (fs₁  xs  fs₂  xs)                

  -- _⊛_ does not distribute over _∣_ from the left.

  private

    not-left-distributive :
      let fs = id  id  []; xs₁ = true  []; xs₂ = true  false  [] in
      (fs  (xs₁  xs₂))  (fs  xs₁  fs  xs₂)
    not-left-distributive ()

  -- Applicative functor laws.

  identity :  {a} {A : Set a} (xs : List A)  (return id  xs)  xs
  identity xs = begin
    return id  xs          ≡⟨⟩
    (return id >>= pam xs)  ≡⟨ MonadProperties.left-identity id (pam xs) 
    (xs >>= return)         ≡⟨ MonadProperties.right-identity xs 
    xs                      

  private

    pam-lemma :  {} {A B C : Set }
                (xs : List A) (f : A  B) (fs : B  List C) 
                (pam xs f >>= fs)  (xs >>= λ x  fs (f x))
    pam-lemma xs f fs = begin
      (pam xs f >>= fs)                   ≡⟨ P.sym $ MP.associative xs (return  f) fs 
      (xs >>= λ x  return (f x) >>= fs)  ≡⟨ MP.cong (refl {x = xs})  x  MP.left-identity (f x) fs) 
      (xs >>= λ x  fs (f x))             

  composition :  {} {A B C : Set }
                (fs : List (B  C)) (gs : List (A  B)) xs 
                (return _∘′_  fs  gs  xs)  (fs  (gs  xs))
  composition {} fs gs xs = begin
    return _∘′_  fs  gs  xs                      ≡⟨⟩
    (return _∘′_ >>= pam fs >>= pam gs >>= pam xs)  ≡⟨ MP.cong (MP.cong (MP.left-identity _∘′_ (pam fs))
                                                                               f  refl {x = pam gs f}))
                                                                   fg  refl {x = pam xs fg}) 
    (pam fs _∘′_ >>= pam gs >>= pam xs)             ≡⟨ MP.cong (pam-lemma fs _∘′_ (pam gs))  _  refl) 
    ((fs >>= λ f  pam gs (f ∘′_)) >>= pam xs)      ≡⟨ P.sym $ MP.associative fs  f  pam gs (_∘′_ f)) (pam xs) 
    (fs >>= λ f  pam gs (f ∘′_) >>= pam xs)        ≡⟨ (MP.cong (refl {x = fs}) λ f 
                                                        pam-lemma gs (f ∘′_) (pam xs)) 
    (fs >>= λ f  gs >>= λ g  pam xs (f ∘′ g))     ≡⟨ (MP.cong (refl {x = fs}) λ f 
                                                        MP.cong (refl {x = gs}) λ g 
                                                        P.sym $ pam-lemma xs g (return  f)) 
    (fs >>= λ f  gs >>= λ g  pam (pam xs g) f)    ≡⟨ (MP.cong (refl {x = fs}) λ f 
                                                        MP.associative gs (pam xs) (return  f)) 
    (fs >>= pam (gs >>= pam xs))                    ≡⟨⟩
    fs  (gs  xs)                                  

  homomorphism :  {} {A B : Set } (f : A  B) x 
                 (return f  return x)  return (f x)
  homomorphism f x = begin
    return f  return x            ≡⟨⟩
    (return f >>= pam (return x))  ≡⟨ MP.left-identity f (pam (return x)) 
    pam (return x) f               ≡⟨ MP.left-identity x (return  f) 
    return (f x)                   

  interchange :  {} {A B : Set } (fs : List (A  B)) {x} 
                (fs  return x)  (return  f  f x)  fs)
  interchange fs {x} = begin
    fs  return x                    ≡⟨⟩
    (fs >>= pam (return x))          ≡⟨ (MP.cong (refl {x = fs}) λ f 
                                         MP.left-identity x (return  f)) 
    (fs >>= λ f  return (f x))      ≡⟨⟩
    (pam fs  f  f x))             ≡⟨ P.sym $ MP.left-identity  f  f x) (pam fs) 
    (return  f  f x) >>= pam fs)  ≡⟨⟩
    return  f  f x)  fs