module Haskell.Prim.Applicative where
open import Haskell.Prim
open import Haskell.Prim.Either
open import Haskell.Prim.Foldable
open import Haskell.Prim.Functor
open import Haskell.Prim.List
open import Haskell.Prim.Maybe
open import Haskell.Prim.Monoid
open import Haskell.Prim.Tuple
record Applicative (f : Set → Set) : Set₁ where
infixl 4 _<*>_
field
pure : a → f a
_<*>_ : f (a → b) → f a → f b
overlap ⦃ super ⦄ : Functor f
_<*_ : f a → f b → f a
x <* y = const <$> x <*> y
_*>_ : f a → f b → f b
x *> y = const id <$> x <*> y
open Applicative ⦃ ... ⦄ public
{-# COMPILE AGDA2HS Applicative existing-class #-}
instance
iApplicativeList : Applicative List
iApplicativeList .pure x = x ∷ []
iApplicativeList ._<*>_ fs xs = concatMap (λ f → map f xs) fs
iApplicativeMaybe : Applicative Maybe
iApplicativeMaybe .pure = Just
iApplicativeMaybe ._<*>_ (Just f) (Just x) = Just (f x)
iApplicativeMaybe ._<*>_ _ _ = Nothing
iApplicativeEither : Applicative (Either a)
iApplicativeEither .pure = Right
iApplicativeEither ._<*>_ (Right f) (Right x) = Right (f x)
iApplicativeEither ._<*>_ (Left e) _ = Left e
iApplicativeEither ._<*>_ _ (Left e) = Left e
iApplicativeFun : Applicative (λ b → a → b)
iApplicativeFun .pure = const
iApplicativeFun ._<*>_ f g x = f x (g x)
iApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_)
iApplicativeTuple₂ .pure x = mempty , x
iApplicativeTuple₂ ._<*>_ (a , f) (b , x) = a <> b , f x
iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_)
iApplicativeTuple₃ .pure x = mempty , mempty , x
iApplicativeTuple₃ ._<*>_ (a , b , f) (a₁ , b₁ , x) = a <> a₁ , b <> b₁ , f x
iApplicativeTuple₄ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →
Applicative (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ []))
iApplicativeTuple₄ .pure x = mempty ; mempty ; mempty ; x ; tt
iApplicativeTuple₄ ._<*>_ (a ; b ; c ; f ; tt) (a₁ ; b₁ ; c₁ ; x ; tt) =
a <> a₁ ; b <> b₁ ; c <> c₁ ; f x ; tt