{-# 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.Base
open import Data.List.Properties
open import Function
open import Relation.Binary.PropositionalEquality as P
using (_≡_; _≢_; _≗_; refl)
open P.≡-Reasoning
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
; _∣_ = _++_
}
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
}
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
)
monadT : ∀ {ℓ} → RawMonadT {ℓ} (_∘′ List)
monadT M = record
{ return = pure ∘′ [_]
; _>>=_ = λ mas f → mas >>= λ as → concat <$> mapM f as
} where open RawMonad M; open TraversableM M
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)
module Applicative where
private
module MP = MonadProperties
pam : ∀ {ℓ} {A B : Set ℓ} → List A → (A → B) → List B
pam xs f = xs >>= return ∘ f
left-zero : ∀ {ℓ} {A B : Set ℓ} (xs : List A) → (∅ ⊛ xs) ≡ ∅ {A = B}
left-zero xs = begin
∅ ⊛ xs ≡⟨⟩
(∅ >>= pam xs) ≡⟨ MonadProperties.left-zero (pam xs) ⟩
∅ ∎
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 ⟩
∅ ∎
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) ∎
private
not-left-distributive :
let fs = id ∷ id ∷ []; xs₁ = true ∷ []; xs₂ = true ∷ false ∷ [] in
(fs ⊛ (xs₁ ∣ xs₂)) ≢ (fs ⊛ xs₁ ∣ fs ⊛ xs₂)
not-left-distributive ()
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 ∎