Agda-2.2.4: 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] 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.

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