module Prelude.Applicative import Builtins import Prelude.Basics import Prelude.Classes import Prelude.Functor ---- Applicative functors/Idioms infixl 2 <$> class Functor f => Applicative (f : Type -> Type) where pure : a -> f a (<$>) : f (a -> b) -> f a -> f b infixl 2 <$ (<$) : Applicative f => f a -> f b -> f a a <$ b = map const a <$> b infixl 2 $> ($>) : Applicative f => f a -> f b -> f b a $> b = map (const id) a <$> b ||| Lift a function to an applicative liftA : Applicative f => (a -> b) -> f a -> f b liftA f a = pure f <$> a ||| Lift a two-argument function to an applicative liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c liftA2 f a b = (map f a) <$> b ||| Lift a three-argument function to an applicative liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d liftA3 f a b c = (map f a) <$> b <$> c infixl 3 <|> class Applicative f => Alternative (f : Type -> Type) where empty : f a (<|>) : f a -> f a -> f a ||| `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False` guard : Alternative f => Bool -> f () guard a = if a then pure () else empty ||| Conditionally execute an applicative expression when : Applicative f => Bool -> Lazy (f ()) -> f () when True f = Force f when False f = pure ()