------------------------------------------------------------------------ -- A variant of _⊛_ (for lists) ------------------------------------------------------------------------ module TotalParserCombinators.Applicative where open import Algebra open import Category.Monad open import Data.Bool open import Data.List as List import Data.List.Properties as ListProp open import Data.List.Any as Any using (Any) import Data.List.Any.BagAndSetEquality as Eq open import Data.List.Any.Properties as AnyProp open import Data.List.Any.Membership open import Data.Product open import Function open import Function.Inverse as Inv using (_⇿_) import Relation.Binary.EqReasoning as EqR open import Relation.Binary.HeterogeneousEquality using (_≅_; refl) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl) open Any.Membership-≡ open RawMonad List.monad private open module BagMonoid {A : Set} = CommutativeMonoid (Eq.commutativeMonoid bag A) using () renaming (∙-cong to _++-cong_) module ListMonoid {A : Set} = Monoid (List.monoid A) -- A helper function. private app : ∀ {A B} → List (A → B) → A → List B app fs x = List.map (λ f → f x) fs -- A variant of _⊛_. This function has the property that fs ⊛′ [] -- evaluates to []. infixl 50 _⊛′_ _⊛′_ : ∀ {A B} → List (A → B) → List A → List B fs ⊛′ xs = xs >>= app fs private right-zero : ∀ {A B} {fs : List (A → B)} → fs ⊛′ [] ≡ [] right-zero = refl ------------------------------------------------------------------------ -- _⊛′_ satisfies its (implicit) specification abstract ⊛′⇿⊛ : ∀ {A B} {fs : List (A → B)} xs {fx} → fx ∈ fs ⊛′ xs ⇿ fx ∈ fs ⊛ xs ⊛′⇿⊛ {fs = fs} xs {fx} = fx ∈ fs ⊛′ xs ⇿⟨ sym >>=⇿ ⟩ Any (λ x → fx ∈ app fs x) xs ⇿⟨ Any-cong (λ _ → Inv.sym map⇿) (_ ∎) ⟩ Any (λ x → Any (λ f → fx ≡ f x) fs) xs ⇿⟨ AnyProp.swap ⟩ Any (λ f → Any (λ x → fx ≡ f x) xs) fs ⇿⟨ ⊛⇿ ⟩ fx ∈ fs ⊛ xs ∎ where open Inv.EquationalReasoning ⇿ : ∀ {A B} {fs : List (A → B)} {xs fx} → (∃₂ λ f x → f ∈ fs × x ∈ xs × fx ≡ f x) ⇿ fx ∈ fs ⊛′ xs ⇿ {fs = fs} {xs} {fx} = (∃₂ λ f x → f ∈ fs × x ∈ xs × fx ≡ f x) ⇿⟨ ⊛-∈⇿ _ ⟩ fx ∈ fs ⊛ xs ⇿⟨ sym $ ⊛′⇿⊛ xs ⟩ fx ∈ fs ⊛′ xs ∎ where open Inv.EquationalReasoning ------------------------------------------------------------------------ -- Algebraic properties abstract -- A lemma. private app-++-commute : ∀ {A B} (fs gs : List (A → B)) x → app (fs ++ gs) x ≡ app fs x ++ app gs x app-++-commute fs gs x = ListProp.map-++-commute (λ f → f x) fs gs -- _⊛′_ preserves bag and set equality. cong : ∀ {k A B} {fs₁ fs₂ : List (A → B)} {xs₁ xs₂} → fs₁ ≈[ k ] fs₂ → xs₁ ≈[ k ] xs₂ → fs₁ ⊛′ xs₁ ≈[ k ] fs₂ ⊛′ xs₂ cong fs₁≈fs₂ xs₁≈xs₂ = Eq.>>=-cong xs₁≈xs₂ (λ x → Eq.map-cong (λ f → refl) fs₁≈fs₂) -- [] is a left zero for _⊛′_. left-zero : ∀ {A B} xs → (List (A → B) ∶ []) ⊛′ xs ≡ [] left-zero [] = refl left-zero (x ∷ xs) = left-zero xs -- _⊛′_ distributes over _++_ from the left. left-distributive : ∀ {A B} {fs : List (A → B)} xs₁ {xs₂} → fs ⊛′ (xs₁ ++ xs₂) ≡ fs ⊛′ xs₁ ++ fs ⊛′ xs₂ left-distributive [] = refl left-distributive {fs = fs} (x ∷ xs₁) {xs₂} = begin fs ⊛′ (x ∷ xs₁ ++ xs₂) ≡⟨ refl ⟩ app fs x ++ fs ⊛′ (xs₁ ++ xs₂) ≡⟨ P.cong (_++_ (app fs x)) (left-distributive xs₁) ⟩ app fs x ++ (fs ⊛′ xs₁ ++ fs ⊛′ xs₂) ≡⟨ P.sym $ ListMonoid.assoc (app fs x) _ _ ⟩ (app fs x ++ fs ⊛′ xs₁) ++ fs ⊛′ xs₂ ≡⟨ refl ⟩ fs ⊛′ (x ∷ xs₁) ++ fs ⊛′ xs₂ ∎ where open P.≡-Reasoning -- _⊛′_ does not distribute over _++_ from the right, if list equality -- is used. private not-right-distributive : let xs = true ∷ true ∷ []; fs₁ = id ∷ []; fs₂ = id ∷ not ∷ [] in (fs₁ ++ fs₂) ⊛′ xs ≢ fs₁ ⊛′ xs ++ fs₂ ⊛′ xs not-right-distributive () -- However, if bag equality is used, then a right distributivity law -- can be proved. The proof makes use of the commutativity of _++_. right-distributive : ∀ {A B} {fs₁ fs₂ : List (A → B)} xs → (fs₁ ++ fs₂) ⊛′ xs ≈[ bag ] fs₁ ⊛′ xs ++ fs₂ ⊛′ xs right-distributive [] = BagMonoid.refl right-distributive {fs₁ = fs₁} {fs₂} (x ∷ xs) = begin (fs₁ ++ fs₂) ⊛′ (x ∷ xs) ≡⟨ refl ⟩ app (fs₁ ++ fs₂) x ++ (fs₁ ++ fs₂) ⊛′ xs ≈⟨ BagMonoid.reflexive (app-++-commute fs₁ fs₂ x) ++-cong right-distributive xs ⟩ (app fs₁ x ++ app fs₂ x) ++ (fs₁ ⊛′ xs ++ fs₂ ⊛′ xs) ≡⟨ ListMonoid.assoc (app fs₁ x) _ _ ⟩ app fs₁ x ++ (app fs₂ x ++ (fs₁ ⊛′ xs ++ fs₂ ⊛′ xs)) ≈⟨ BagMonoid.refl {x = app fs₁ x} ++-cong (begin app fs₂ x ++ (fs₁ ⊛′ xs ++ fs₂ ⊛′ xs) ≡⟨ P.sym $ ListMonoid.assoc (app fs₂ x) _ _ ⟩ (app fs₂ x ++ fs₁ ⊛′ xs) ++ fs₂ ⊛′ xs ≈⟨ BagMonoid.comm (app fs₂ x) (fs₁ ⊛′ xs) ++-cong BagMonoid.refl ⟩ (fs₁ ⊛′ xs ++ app fs₂ x) ++ fs₂ ⊛′ xs ≡⟨ ListMonoid.assoc (fs₁ ⊛′ xs) _ _ ⟩ fs₁ ⊛′ xs ++ (app fs₂ x ++ fs₂ ⊛′ xs) ∎) ⟩ app fs₁ x ++ (fs₁ ⊛′ xs ++ (app fs₂ x ++ fs₂ ⊛′ xs)) ≡⟨ P.sym $ ListMonoid.assoc (app fs₁ x) _ _ ⟩ (app fs₁ x ++ fs₁ ⊛′ xs) ++ (app fs₂ x ++ fs₂ ⊛′ xs) ≡⟨ refl ⟩ fs₁ ⊛′ (x ∷ xs) ++ fs₂ ⊛′ (x ∷ xs) ∎ where open EqR ([ bag ]-Equality _) -- Applicative functor laws. identity : ∀ {A} (xs : List A) → return id ⊛′ xs ≡ xs identity [] = refl identity (x ∷ xs) = P.cong (_∷_ x) $ identity xs composition : ∀ {A B C} (fs : List (B → C)) (gs : List (A → B)) xs → return _∘′_ ⊛′ fs ⊛′ gs ⊛′ xs ≡ fs ⊛′ (gs ⊛′ xs) composition fs gs [] = refl composition fs gs (x ∷ xs) = begin return _∘′_ ⊛′ fs ⊛′ gs ⊛′ (x ∷ xs) ≡⟨ refl ⟩ app (return _∘′_ ⊛′ fs ⊛′ gs) x ++ (return _∘′_ ⊛′ fs ⊛′ gs ⊛′ xs) ≡⟨ P.cong₂ _++_ (lemma₁ gs) (composition fs gs xs) ⟩ fs ⊛′ app gs x ++ fs ⊛′ (gs ⊛′ xs) ≡⟨ P.sym $ left-distributive (app gs x) ⟩ fs ⊛′ (app gs x ++ (gs ⊛′ xs)) ≡⟨ refl ⟩ fs ⊛′ (gs ⊛′ (x ∷ xs)) ∎ where open P.≡-Reasoning lemma₁ : ∀ gs → app (return _∘′_ ⊛′ fs ⊛′ gs) x ≡ fs ⊛′ app gs x lemma₁ [] = refl lemma₁ (g ∷ gs) = begin app (return _∘′_ ⊛′ fs ⊛′ (g ∷ gs)) x ≡⟨ refl ⟩ app (app (return _∘′_ ⊛′ fs) g ++ (return _∘′_ ⊛′ fs) ⊛′ gs) x ≡⟨ app-++-commute (app (return _∘′_ ⊛′ fs) g) ((return _∘′_ ⊛′ fs) ⊛′ gs) x ⟩ app (app (return _∘′_ ⊛′ fs) g) x ++ app (return _∘′_ ⊛′ fs ⊛′ gs) x ≡⟨ P.cong₂ _++_ (lemma₂ fs) (lemma₁ gs) ⟩ app fs (g x) ++ fs ⊛′ app gs x ≡⟨ refl ⟩ fs ⊛′ app (g ∷ gs) x ∎ where lemma₂ : (fs : List _) → app (app (return _∘′_ ⊛′ fs) g) x ≡ app fs (g x) lemma₂ [] = refl lemma₂ (f ∷ fs) = P.cong (_∷_ (f (g x))) $ lemma₂ fs homomorphism : ∀ {A B : Set} (f : A → B) x → return f ⊛′ return x ≡ return (f x) homomorphism f x = refl interchange : ∀ {A B} (fs : List (A → B)) {x} → fs ⊛′ return x ≡ return (λ f → f x) ⊛′ fs interchange [] = refl interchange (f ∷ fs) {x} = begin (f ∷ fs) ⊛′ return x ≡⟨ refl ⟩ [ f x ] ++ fs ⊛′ return x ≡⟨ P.cong (_++_ [ f x ]) $ interchange fs ⟩ [ f x ] ++ return (λ f → f x) ⊛′ fs ≡⟨ refl ⟩ return (λ f → f x) ⊛′ (f ∷ fs) ∎ where open P.≡-Reasoning