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 = t a -> (a -> f b) -> f (t b)
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 f a
forall a. f a
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 Bool -> f a -> f a
forall (f :: * -> *) a. Alternative f => Bool -> f a -> f a
?*> a -> f a
forall a. 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 = (a -> f a) -> t a -> f a
forall (f :: * -> *) (t :: * -> *) a b.
(Alternative f, Foldable t) =>
(a -> f b) -> t a -> f b
foldMapA a -> f a
forall a. a -> f a
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 = Alt f b -> f b
forall {k} (f :: k -> *) (a :: k). Alt f a -> f a
getAlt (Alt f b -> f b) -> (t a -> Alt f b) -> t a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Alt f b) -> t a -> Alt f b
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (f b -> Alt f b
forall {k} (f :: k -> *) (a :: k). f a -> Alt f a
Alt (f b -> Alt f b) -> (a -> f b) -> a -> Alt f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f b
f)