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