------------------------------------------------------------------------ -- The Agda standard library -- -- Applicative functors ------------------------------------------------------------------------ -- Note that currently the applicative functor laws are not included -- here. {-# OPTIONS --cubical-compatible --safe #-} module Effect.Applicative where open import Data.Bool.Base using (Bool; true; false) open import Data.Product.Base using (_×_; _,_) open import Data.Unit.Polymorphic.Base using (⊤) open import Effect.Choice using (RawChoice) open import Effect.Empty using (RawEmpty) open import Effect.Functor as Fun using (RawFunctor) open import Function.Base using (const; flip; _∘′_) open import Level using (Level; suc; _⊔_) open import Relation.Binary.PropositionalEquality.Core using (_≡_) private variable f g : Level A B C : Set f ------------------------------------------------------------------------ -- The type of raw applicatives record RawApplicative (F : Set f → Set g) : Set (suc f ⊔ g) where infixl 4 _<*>_ _<*_ _*>_ infixl 4 _⊛_ _<⊛_ _⊛>_ infix 4 _⊗_ field rawFunctor : RawFunctor F pure : A → F A _<*>_ : F (A → B) → F A → F B open RawFunctor rawFunctor public _<*_ : F A → F B → F A a <* b = const <$> a <*> b _*>_ : F A → F B → F B a *> b = flip const <$> a <*> b zipWith : (A → B → C) → F A → F B → F C zipWith f x y = f <$> x <*> y zip : F A → F B → F (A × B) zip = zipWith _,_ -- Haskell-style alternative name for pure return : A → F A return = pure -- backwards compatibility: unicode variants _⊛_ : F (A → B) → F A → F B _⊛_ = _<*>_ _<⊛_ : F A → F B → F A _<⊛_ = _<*_ _⊛>_ : F A → F B → F B _⊛>_ = _*>_ _⊗_ : F A → F B → F (A × B) _⊗_ = zip module _ where open RawApplicative open RawFunctor -- Smart constructor mkRawApplicative : (F : Set f → Set g) → (pure : ∀ {A} → A → F A) → (app : ∀ {A B} → F (A → B) → F A → F B) → RawApplicative F mkRawApplicative F pure app .rawFunctor ._<$>_ = app ∘′ pure mkRawApplicative F pure app .pure = pure mkRawApplicative F pure app ._<*>_ = app ------------------------------------------------------------------------ -- The type of raw applicatives with a zero record RawApplicativeZero (F : Set f → Set g) : Set (suc f ⊔ g) where field rawApplicative : RawApplicative F rawEmpty : RawEmpty F open RawApplicative rawApplicative public open RawEmpty rawEmpty public guard : Bool → F ⊤ guard true = pure _ guard false = empty ------------------------------------------------------------------------ -- The type of raw alternative applicatives record RawAlternative (F : Set f → Set g) : Set (suc f ⊔ g) where field rawApplicativeZero : RawApplicativeZero F rawChoice : RawChoice F open RawApplicativeZero rawApplicativeZero public open RawChoice rawChoice public ------------------------------------------------------------------------ -- The type of applicative morphisms record Morphism {F₁ F₂ : Set f → Set g} (A₁ : RawApplicative F₁) (A₂ : RawApplicative F₂) : Set (suc f ⊔ g) where module A₁ = RawApplicative A₁ module A₂ = RawApplicative A₂ field functorMorphism : Fun.Morphism A₁.rawFunctor A₂.rawFunctor open Fun.Morphism functorMorphism public field op-pure : (x : A) → op (A₁.pure x) ≡ A₂.pure x op-<*> : (f : F₁ (A → B)) (x : F₁ A) → op (f A₁.⊛ x) ≡ (op f A₂.⊛ op x) -- backwards compatibility: unicode variants op-⊛ = op-<*>