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

Safe Haskell | None

Agda.Utils.Monad

Synopsis

- when_ :: Monad m => Bool -> m a -> m ()
- unless_ :: Monad m => Bool -> m a -> m ()
- whenJust :: Monad m => Maybe a -> (a -> m ()) -> m ()
- whenM :: Monad m => m Bool -> m a -> m ()
- unlessM :: Monad m => m Bool -> m a -> m ()
- whenJustM :: Monad m => m (Maybe a) -> (a -> m ()) -> m ()
- ifM :: Monad m => m Bool -> m a -> m a -> m a
- and2M :: Monad m => m Bool -> m Bool -> m Bool
- andM :: Monad m => [m Bool] -> m Bool
- or2M :: Monad m => m Bool -> m Bool -> m Bool
- orM :: Monad m => [m Bool] -> m Bool
- altM1 :: Monad m => (a -> m (Either err b)) -> [a] -> m (Either err b)
- mapM' :: (Foldable t, Monad m, Monoid b) => (a -> m b) -> t a -> m b
- forM' :: (Foldable t, Monad m, Monoid b) => t a -> (a -> m b) -> m b
- 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 :: (Monad m, Functor m) => (a -> m (Maybe b)) -> [a] -> m [b]
- 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
- bracket_ :: Monad m => m a -> (a -> m c) -> m b -> m b
- localState :: MonadState s m => m a -> m a
- readM :: (Error e, MonadError e m, Read a) => String -> m a
- (<$>) :: Functor f => (a -> b) -> f a -> f b
- (<*>) :: Applicative f => forall a b. f (a -> b) -> f a -> f b

# Documentation

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

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

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

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

whenJust :: Monad m => Maybe a -> (a -> m ()) -> m ()

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

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

whenJustM :: Monad m => m (Maybe a) -> (a -> m ()) -> m ()

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

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

Lazy monadic conjunction.

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

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

Lazy monadic disjunction.

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

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

Lazy monadic disjunction with `Either` truth values.

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

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 right-to-left). It might be preferable for right associative monoids.

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

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

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

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

`mapM` for the continuation monad. Terribly useful.

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

Requires both lists to have the same lengths.

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

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

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

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

bracket

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_

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

Restore state after computation.

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

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