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

Agda.Utils.Monad

Synopsis

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

fmapM :: (Traversable f, Applicative m) => (a -> m b) -> f a -> m (f b)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

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.

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

liftEither :: MonadError e m => Either e a -> m aSource

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

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

An infix synonym for fmap.

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

Sequential application.