Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 cSource
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 aSource
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) -> rSource
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 aSource
Finally for the Error class. Errors in the finally part take precedence over prior errors.
bracketSource
:: (Error e, MonadError e m)
=> m aAcquires resource. Run first.
-> a -> m cReleases resource. Run last.
-> a -> m bComputes 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 aSource
readM :: (Monad m, Read a) => String -> m aSource
<$>
<*>
Produced by Haddock version 2.4.2