module Agda.Utils.Applicative
( (?*>)
, (?$>)
, foldA
, foldMapA
, forA
)
where
import Control.Applicative
import Data.Monoid ( Alt(..) )
import Data.Traversable ( for )
forA :: (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
forA :: forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
forA = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for
(?*>) :: Alternative f => Bool -> f a -> f a
Bool
b ?*> :: forall (f :: * -> *) a. Alternative f => Bool -> f a -> f a
?*> f a
f = if Bool
b then f a
f else forall (f :: * -> *) a. Alternative f => f a
empty
(?$>) :: Alternative f => Bool -> a -> f a
Bool
b ?$> :: forall (f :: * -> *) a. Alternative f => Bool -> a -> f a
?$> a
a = Bool
b forall (f :: * -> *) a. Alternative f => Bool -> f a -> f a
?*> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
foldA :: (Alternative f, Foldable t) => t a -> f a
foldA :: forall (f :: * -> *) (t :: * -> *) a.
(Alternative f, Foldable t) =>
t a -> f a
foldA = forall (f :: * -> *) (t :: * -> *) a b.
(Alternative f, Foldable t) =>
(a -> f b) -> t a -> f b
foldMapA forall (f :: * -> *) a. Applicative f => a -> f a
pure
foldMapA :: (Alternative f, Foldable t) => (a -> f b) -> t a -> f b
foldMapA :: forall (f :: * -> *) (t :: * -> *) a b.
(Alternative f, Foldable t) =>
(a -> f b) -> t a -> f b
foldMapA a -> f b
f = forall {k} (f :: k -> *) (a :: k). Alt f a -> f a
getAlt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall {k} (f :: k -> *) (a :: k). f a -> Alt f a
Alt forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f b
f)