------------------------------------------------------------------------
-- 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  _<*>_ _<*_ _*>_
  infixl  _⊛_ _<⊛_ _⊛>_
  infix   _⊗_
  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-<*>