------------------------------------------------------------------------ -- 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 ∎