Agda-2.4.0.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Utils.Monad

Synopsis

Documentation

when_ :: Monad m => Bool -> m a -> m () Source

when_ is just Control.Monad.when with a more general type.

unless_ :: Monad m => Bool -> m a -> m () Source

unless_ is just Control.Monad.unless with a more general type.

whenM :: Monad m => m Bool -> m a -> m () Source

unlessM :: Monad m => m Bool -> m a -> m () Source

ifM :: Monad m => m Bool -> m a -> m a -> m a Source

Monadic if-then-else.

ifNotM :: Monad m => m Bool -> m a -> m a -> m a Source

ifNotM mc = ifM (not $ mc)

and2M :: Monad m => m Bool -> m Bool -> m Bool Source

Lazy monadic conjunction.

andM :: Monad m => [m Bool] -> m Bool Source

or2M :: Monad m => m Bool -> m Bool -> m Bool Source

Lazy monadic disjunction.

orM :: Monad m => [m Bool] -> m Bool Source

altM1 :: Monad m => (a -> m (Either err b)) -> [a] -> m (Either err b) Source

Lazy monadic disjunction with Either truth values.

mapM' :: (Foldable t, Monad m, Monoid b) => (a -> m b) -> t a -> m b Source

Generalized version of mapM_ :: Monad m => (a -> m ()) -> [a] -> m () Executes effects and collects results in left-to-right order. Works best with left-associative monoids.

Note that there is an alternative

mapM' f t = foldr mappend mempty $ mapM f t

that collects results in right-to-left order (effects still left-to-right). It might be preferable for right associative monoids.

forM' :: (Foldable t, Monad m, Monoid b) => t a -> (a -> m b) -> m b Source

Generalized version of forM_ :: Monad m => [a] -> (a -> m ()) -> m ()

type Cont r a = (a -> r) -> r Source

thread :: (a -> Cont r b) -> [a] -> Cont r [b] Source

mapM for the continuation monad. Terribly useful.

zipWithM' :: Monad m => (a -> b -> m c) -> [a] -> [b] -> m [c] Source

Requires both lists to have the same lengths.

mapMaybeM :: (Monad m, Functor m) => (a -> m (Maybe b)) -> [a] -> m [b] Source

A monadic version of mapMaybe :: (a -> Maybe b) -> [a] -> [b].

dropWhileM :: Monad m => (a -> m Bool) -> [a] -> m [a] Source

A monadic version of dropWhile :: (a -> Bool) -> [a] -> [a].

finally :: (Error e, MonadError e m) => m a -> m b -> m a Source

Finally for the Error class. Errors in the finally part take precedence over prior errors.

bracket Source

Arguments

:: (Error e, MonadError e m) 
=> m a

Acquires resource. Run first.

-> (a -> m c)

Releases resource. Run last.

-> (a -> m b)

Computes result. Run in-between.

-> m b 

Bracket for the Error class.

bracket_ Source

Arguments

:: Monad m 
=> m a

Acquires resource. Run first.

-> (a -> m c)

Releases resource. Run last.

-> m b

Computes result. Run in-between.

-> m b 

Bracket without failure. Typically used to preserve state.

localState :: MonadState s m => m a -> m a Source

Restore state after computation.

readM :: (Error e, MonadError e m, Read a) => String -> m a Source

(<$>) :: Functor f => (a -> b) -> f a -> f b infixl 4

An infix synonym for fmap.

(<*>) :: Applicative f => forall a b. f (a -> b) -> f a -> f b

Sequential application.

(<$) :: Functor f => forall a b. a -> f b -> f a

Replace all locations in the input with the same value. The default definition is fmap . const, but this may be overridden with a more efficient version.