------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of List
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.List.Effectful where

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

private
  variable
     : Level
    A : Set 

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

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

applicative : RawApplicative {} List
applicative = record
  { rawFunctor = functor
  ; pure = [_]
  ; _<*>_  = ap
  }

empty : RawEmpty {} List
empty = record { empty = [] }

choice : RawChoice {} List
choice = record { _<|>_ = _++_ }

applicativeZero : RawApplicativeZero {} List
applicativeZero = record
  { rawApplicative = applicative
  ; rawEmpty = empty
  }

alternative : RawAlternative {} List
alternative = record
  { rawApplicativeZero = applicativeZero
  ; rawChoice = choice
  }

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

monad :  {}  RawMonad {} List
monad = record
  { rawApplicative = applicative
  ; _>>=_  = flip concatMap
  }

join : List (List A)  List A
join = Join.join monad

monadZero :  {}  RawMonadZero {} List
monadZero = record
  { rawMonad = monad
  ; rawEmpty = empty
  }

monadPlus :  {}  RawMonadPlus {} List
monadPlus = record
  { rawMonadZero = monadZero
  ; rawChoice  = choice
  }

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

module TraversableA {f g F} (App : RawApplicative {f} {g} 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 n M} (Mon : RawMonad {m} {n} M) where

  open RawMonad Mon

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

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

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

module MonadProperties where

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

  right-identity :  {} {A : Set } (xs : List A) 
                   (xs >>= pure)  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 = pure; g = pure 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 >>= pure  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 (pure  f)) 
    (fs >>= λ _  )  ≡⟨ MP.right-zero fs 
                     

  unfold-<$> :  {} {A B : Set }  (f : A  B) (as : List A) 
               (f <$> as)  (pure f  as)
  unfold-<$> f as = P.sym (++-identityʳ (f <$> as))

  -- _⊛_ unfolds to binds.
  unfold-⊛ :  {} {A B : Set }  (fs : List (A  B)) (as : List A) 
             (fs  as)  (fs >>= pam as)
  unfold-⊛ fs as = begin
    fs  as
      ≡⟨ concatMap-cong  f  P.cong (map f) (concatMap-pure as)) fs 
    concatMap  f  map f (concatMap pure as)) fs
      ≡⟨ concatMap-cong  f  map-concatMap f pure as) fs 
    concatMap  f  concatMap  x  pure (f x)) as) fs
      ≡⟨⟩
    (fs >>= pam as)
      

  -- _⊛_ 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                     ≡⟨ unfold-⊛ (fs₁  fs₂) xs 
    (fs₁  fs₂ >>= pam xs)               ≡⟨ MonadProperties.right-distributive fs₁ fs₂ (pam xs) 
    (fs₁ >>= pam xs)  (fs₂ >>= pam xs)  ≡⟨ P.cong₂ _∣_ (unfold-⊛ fs₁ xs) (unfold-⊛ fs₂ 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)  (pure id  xs)  xs
  identity xs = begin
    pure id  xs          ≡⟨ unfold-⊛ (pure id) xs 
    (pure id >>= pam xs)  ≡⟨ MonadProperties.left-identity id (pam xs) 
    (xs >>= pure)         ≡⟨ 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)                 ≡⟨ MP.associative xs (pure  f) fs 
      (xs >>= λ x  pure (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 
                (pure _∘′_  fs  gs  xs)  (fs  (gs  xs))
  composition {} fs gs xs = begin
    pure _∘′_  fs  gs  xs
      ≡⟨ unfold-⊛ (pure _∘′_  fs  gs) xs 
    (pure _∘′_  fs  gs >>= pam xs)
      ≡⟨ P.cong (_>>= pam xs) (unfold-⊛ (pure _∘′_  fs) gs) 
    (pure _∘′_  fs >>= pam gs >>= pam xs)
      ≡⟨ P.cong  h  h >>= pam gs >>= pam xs) (unfold-⊛ (pure _∘′_) fs) 
    (pure _∘′_ >>= 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)
      ≡⟨ 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 (pure  f)) 
    (fs >>= λ f  gs >>= λ g  pam (pam xs g) f)
      ≡⟨ MP.cong (refl {x = fs})  f  MP.associative gs (pam xs) (pure  f)) 
    (fs >>= pam (gs >>= pam xs))
      ≡⟨ unfold-⊛ fs (gs >>= pam xs) 
    fs  (gs >>= pam xs)
      ≡⟨ P.cong (fs ⊛_) (unfold-⊛ gs xs) 
    fs  (gs  xs)
      

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

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