| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Utils.Monad

Synopsis

(<.>) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c
whenM :: Monad m => m Bool -> m () -> m ()
unlessM :: Monad m => m Bool -> m () -> m ()
ifM :: Monad m => m Bool -> m a -> m a -> m a
forgetM :: Applicative m => m a -> m ()
concatMapM :: Applicative m => (a -> m [b]) -> [a] -> m [b]
forceM :: Monad m => [a] -> m ()
commuteM :: (Traversable f, Applicative m) => f (m a) -> m (f a)
type Cont r a = (a -> r) -> r
thread :: (a -> Cont r b) -> [a] -> Cont r [b]
zipWithM' :: Monad m => (a -> b -> m c) -> [a] -> [b] -> m [c]
finally :: (Error e, MonadError e m) => m a -> m b -> m a
bracket :: (Error e, MonadError e m) => m a -> (a -> m c) -> (a -> m b) -> m b
mapMaybeM :: Applicative m => (a -> m b) -> Maybe a -> m (Maybe b)
liftEither :: MonadError e m => Either e a -> m a
readM :: (Monad m, Read a) => String -> m a
<$>
<*>

Documentation

(<.>) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c | Source

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

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

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

forgetM :: Applicative m => m a -> m () | Source

concatMapM :: Applicative m => (a -> m [b]) -> [a] -> m [b] | Source

forceM :: Monad m => [a] -> m () | Source

Depending on the monad you have to look at the result for the force to be effective. For the `IO` monad you do.

commuteM :: (Traversable f, Applicative m) => f (m a) -> m (f a) | Source

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.

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

:: (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.

mapMaybeM :: Applicative m => (a -> m b) -> Maybe a -> m (Maybe b) | Source

liftEither :: MonadError e m => Either e a -> m a | Source

readM :: (Monad m, Read a) => String -> m a | Source

<$>
<*>
Produced by Haddock version 2.4.2