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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Monad

Synopsis

- when :: (IsBool b, Monad m) => b -> m () -> m ()
- unless :: (IsBool b, Monad m) => b -> m () -> m ()
- guard :: (IsBool b, MonadPlus m) => b -> m ()
- bracket_ :: Monad m => m a -> (a -> m ()) -> m b -> m b
- finally :: MonadError e m => m a -> m () -> m a
- andM :: (Foldable f, Monad m) => f (m Bool) -> m Bool
- ifM :: Monad m => m Bool -> m a -> m a -> m a
- whenM :: Monad m => m Bool -> m () -> m ()
- unlessM :: Monad m => m Bool -> m () -> m ()
- and2M :: Monad m => m Bool -> m Bool -> m Bool
- guardWithError :: MonadError e m => e -> Bool -> m ()
- mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
- tryMaybe :: (MonadError e m, Functor m) => m a -> m (Maybe a)
- anyM :: (Foldable f, Monad m) => (a -> m Bool) -> f a -> m Bool
- or2M :: Monad m => m Bool -> m Bool -> m Bool
- tell1 :: (Monoid ws, Singleton w ws, MonadWriter ws m) => w -> m ()
- concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
- dropWhileM :: Monad m => (a -> m Bool) -> [a] -> m [a]
- (==<<) :: Monad m => (a -> b -> m c) -> (m a, m b) -> m c
- (<*!>) :: Monad m => m (a -> b) -> m a -> m b
- guardM :: (Monad m, MonadPlus m) => m Bool -> m ()
- ifNotM :: Monad m => m Bool -> m a -> m a -> m a
- allM :: (Foldable f, Monad m) => (a -> m Bool) -> f a -> m Bool
- forallM :: (Foldable f, Monad m) => f a -> (a -> m Bool) -> m Bool
- orM :: (Foldable f, Monad m) => f (m Bool) -> m Bool
- existsM :: (Foldable f, Monad m) => f a -> (a -> m Bool) -> m Bool
- altM1 :: Monad m => (a -> m (Either err b)) -> [a] -> m (Either err b)
- orEitherM :: (Monoid e, Monad m, Functor m) => [m (Either e b)] -> m (Either e b)
- mapM' :: (Foldable t, Applicative m, Monoid b) => (a -> m b) -> t a -> m b
- forM' :: (Foldable t, Applicative m, Monoid b) => t a -> (a -> m b) -> m b
- mapMM :: (Traversable t, Monad m) => (a -> m b) -> m (t a) -> m (t b)
- forMM :: (Traversable t, Monad m) => m (t a) -> (a -> m b) -> m (t b)
- mapMM_ :: (Foldable t, Monad m) => (a -> m ()) -> m (t a) -> m ()
- forMM_ :: (Foldable t, Monad m) => m (t a) -> (a -> m ()) -> m ()
- mapMaybeMM :: Monad m => (a -> m (Maybe b)) -> m [a] -> m [b]
- forMaybeM :: Monad m => [a] -> (a -> m (Maybe b)) -> m [b]
- forMaybeMM :: Monad m => m [a] -> (a -> m (Maybe b)) -> m [b]
- dropWhileEndM :: Monad m => (a -> m Bool) -> [a] -> m [a]
- partitionM :: (Functor m, Applicative m) => (a -> m Bool) -> [a] -> m ([a], [a])
- fromMaybeMP :: MonadPlus m => Maybe a -> m a
- catMaybesMP :: MonadPlus m => m (Maybe a) -> m a
- scatterMP :: (MonadPlus m, Foldable t) => m (t a) -> m a
- tryCatch :: (MonadError e m, Functor m) => m () -> m (Maybe e)
- localState :: MonadState s m => m a -> m a
- embedWriter :: forall w (m :: Type -> Type) a. (Monoid w, Monad m) => Writer w a -> WriterT w m a
- class (Alternative m, Monad m) => MonadPlus (m :: Type -> Type) where
  - mzero :: m a
  - mplus :: m a -> m a -> m a
- liftM2 :: Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
- void :: Functor f => f a -> f ()
- liftA2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c
- join :: Monad m => m (m a) -> m a
- class (forall (m :: Type -> Type). Monad m => Monad (t m)) => MonadTrans (t :: (Type -> Type) -> Type -> Type) where
  - lift :: Monad m => m a -> t m a
- forM_ :: (Foldable t, Monad m) => t a -> (a -> m b) -> m ()
- liftM3 :: Monad m => (a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
- liftM4 :: Monad m => (a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
- msum :: (Foldable t, MonadPlus m) => t (m a) -> m a
- forM :: (Traversable t, Monad m) => t a -> (a -> m b) -> m (t b)
- filterM :: Applicative m => (a -> m Bool) -> [a] -> m [a]
- (>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
- (<=<) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c
- zipWithM :: Applicative m => (a -> b -> m c) -> [a] -> [b] -> m [c]
- zipWithM_ :: Applicative m => (a -> b -> m c) -> [a] -> [b] -> m ()
- foldM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b
- (<$!>) :: Monad m => (a -> b) -> m a -> m b
- tryError :: MonadError e m => m a -> m (Either e a)
- withError :: MonadError e m => (e -> e) -> m a -> m a
- (<$>) :: Functor f => (a -> b) -> f a -> f b
- (<*>) :: Applicative f => f (a -> b) -> f a -> f b
- (<$) :: Functor f => a -> f b -> f a

# Documentation

when :: (IsBool b, Monad m) => b -> m () -> m () Source #

unless :: (IsBool b, Monad m) => b -> m () -> m () Source #

guard :: (IsBool b, MonadPlus m) => b -> m () Source #

bracket_ Source #

Arguments

:: Monad m |
=> m a | Acquires resource. Run first.
-> (a -> m ()) | Releases resource. Run last.
-> m b | Computes result. Run in-between.
-> m b |

Bracket without failure. Typically used to preserve state.

finally :: MonadError e m => m a -> m () -> m a Source #

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

andM :: (Foldable f, Monad m) => f (m Bool) -> m Bool Source #

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

Monadic if-then-else.

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

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

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

Lazy monadic conjunction.

guardWithError :: MonadError e m => e -> Bool -> m () Source #

Like `guard`, but raise given error when condition fails.

mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b] Source #

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

tryMaybe :: (MonadError e m, Functor m) => m a -> m (Maybe a) Source #

Try a computation, return `Nothing` if an `Error` occurs.

anyM :: (Foldable f, Monad m) => (a -> m Bool) -> f a -> m Bool Source #

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

Lazy monadic disjunction.

tell1 :: (Monoid ws, Singleton w ws, MonadWriter ws m) => w -> m () Source #

Output a single value.

concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] Source #

dropWhileM :: Monad m => (a -> m Bool) -> [a] -> m [a] Source #

A monadic version of ``dropWhile` :: (a -> Bool) -> [a] -> [a]`.

(==<<) :: Monad m => (a -> b -> m c) -> (m a, m b) -> m c Source #

Binary bind.

(<*!>) :: Monad m => m (a -> b) -> m a -> m b infixl 4 Source #

Strict `ap`

guardM :: (Monad m, MonadPlus m) => m Bool -> m () Source #

Monadic guard.

ifNotM :: Monad m => m Bool -> m a -> m a -> m a Source #

    ifNotM mc = ifM (not $ mc)

allM :: (Foldable f, Monad m) => (a -> m Bool) -> f a -> m Bool Source #

forallM :: (Foldable f, Monad m) => f a -> (a -> m Bool) -> m Bool Source #

orM :: (Foldable f, Monad m) => f (m Bool) -> m Bool Source #

existsM :: (Foldable f, Monad m) => f a -> (a -> m Bool) -> m Bool Source #

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

Lazy monadic disjunction with `Either` truth values. Returns the last error message if all fail.

orEitherM :: (Monoid e, Monad m, Functor m) => [m (Either e b)] -> m (Either e b) Source #

Lazy monadic disjunction with accumulation of errors in a monoid. Errors are discarded if we succeed.

mapM' :: (Foldable t, Applicative m, Monoid b) => (a -> m b) -> t a -> m b Source #

Generalized version of `traverse_ :: Applicative 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 left-to-right). It might be preferable for right associative monoids.

forM' :: (Foldable t, Applicative m, Monoid b) => t a -> (a -> m b) -> m b Source #

Generalized version of `for_ :: Applicative m => [a] -> (a -> m ()) -> m ()`

mapMM :: (Traversable t, Monad m) => (a -> m b) -> m (t a) -> m (t b) Source #

forMM :: (Traversable t, Monad m) => m (t a) -> (a -> m b) -> m (t b) Source #

mapMM_ :: (Foldable t, Monad m) => (a -> m ()) -> m (t a) -> m () Source #

forMM_ :: (Foldable t, Monad m) => m (t a) -> (a -> m ()) -> m () Source #

mapMaybeMM :: Monad m => (a -> m (Maybe b)) -> m [a] -> m [b] Source #

A version of ``mapMaybeM`` with a computation for the input list.

forMaybeM :: Monad m => [a] -> (a -> m (Maybe b)) -> m [b] Source #

The `for` version of `mapMaybeM`.

forMaybeMM :: Monad m => m [a] -> (a -> m (Maybe b)) -> m [b] Source #

The `for` version of `mapMaybeMM`.

dropWhileEndM :: Monad m => (a -> m Bool) -> [a] -> m [a] Source #

A monadic version of ``dropWhileEnd` :: (a -> Bool) -> [a] -> m [a]`. Effects happen starting at the end of the list until `p` becomes false.

partitionM :: (Functor m, Applicative m) => (a -> m Bool) -> [a] -> m ([a], [a]) Source #

A ``monadic'` version of @`partition` :: (a -> Bool) -> [a] -> ([a],[a])

fromMaybeMP :: MonadPlus m => Maybe a -> m a Source #

Translates `Maybe` to `MonadPlus`.

catMaybesMP :: MonadPlus m => m (Maybe a) -> m a Source #

Generalises the `catMaybes` function from lists to an arbitrary `MonadPlus`.

scatterMP :: (MonadPlus m, Foldable t) => m (t a) -> m a Source #

Branch over elements of a monadic `Foldable` data structure.

tryCatch :: (MonadError e m, Functor m) => m () -> m (Maybe e) Source #

Run a command, catch the exception and return it.

localState :: MonadState s m => m a -> m a Source #

Restore state after computation.

embedWriter :: forall w (m :: Type -> Type) a. (Monoid w, Monad m) => Writer w a -> WriterT w m a Source #

class (Alternative m, Monad m) => MonadPlus (m :: Type -> Type) where Source #

Monads that also support choice and failure.

Minimal complete definition

Nothing

Methods

mzero :: m a Source #

The identity of `mplus`. It should also satisfy the equations

    mzero >>= f  =  mzero
    v >> mzero   =  mzero

The default definition is

    mzero = empty

mplus :: m a -> m a -> m a Source #

An associative operation. The default definition is

    mplus = (<|>)

#### Instances

Instances details

MonadPlus NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods mzero :: NLM a Source # mplus :: NLM a -> NLM a -> NLM a Source #
MonadPlus IResult |
Instance details Defined in Data.Aeson.Types.Internal Methods mzero :: IResult a Source # mplus :: IResult a -> IResult a -> IResult a Source #
MonadPlus Parser |
Instance details Defined in Data.Aeson.Types.Internal Methods mzero :: Parser a Source # mplus :: Parser a -> Parser a -> Parser a Source #
MonadPlus Result |
Instance details Defined in Data.Aeson.Types.Internal Methods mzero :: Result a Source # mplus :: Result a -> Result a -> Result a Source #
MonadPlus Get | Since: binary-0.7.1.0
Instance details Defined in Data.Binary.Get.Internal Methods mzero :: Get a Source # mplus :: Get a -> Get a -> Get a Source #
MonadPlus Seq |
Instance details Defined in Data.Sequence.Internal Methods mzero :: Seq a Source # mplus :: Seq a -> Seq a -> Seq a Source #
MonadPlus DList |
Instance details Defined in Data.DList.Internal Methods mzero :: DList a Source # mplus :: DList a -> DList a -> DList a Source #
MonadPlus STM | Takes the first non-`retry`ing `STM` action. Since: base-4.3.0.0
Instance details Defined in GHC.Internal.Conc.Sync Methods mzero :: STM a Source # mplus :: STM a -> STM a -> STM a Source #
MonadPlus P | Since: base-2.1
Instance details Defined in GHC.Internal.Text.ParserCombinators.ReadP Methods mzero :: P a Source # mplus :: P a -> P a -> P a Source #
MonadPlus ReadP | Since: base-2.1
Instance details Defined in GHC.Internal.Text.ParserCombinators.ReadP Methods mzero :: ReadP a Source # mplus :: ReadP a -> ReadP a -> ReadP a Source #
MonadPlus ReadPrec | Since: base-2.1
Instance details Defined in GHC.Internal.Text.ParserCombinators.ReadPrec Methods mzero :: ReadPrec a Source # mplus :: ReadPrec a -> ReadPrec a -> ReadPrec a Source #
MonadPlus IO | Takes the first non-throwing `IO` action's result. `mzero` throws an exception. Since: base-4.9.0.0
Instance details Defined in GHC.Internal.Base Methods mzero :: IO a Source # mplus :: IO a -> IO a -> IO a Source #
MonadPlus Array |
Instance details Defined in Data.Primitive.Array Methods mzero :: Array a Source # mplus :: Array a -> Array a -> Array a Source #
MonadPlus SmallArray |
Instance details Defined in Data.Primitive.SmallArray Methods mzero :: SmallArray a Source # mplus :: SmallArray a -> SmallArray a -> SmallArray a Source #
MonadPlus Vector |
Instance details Defined in Data.Vector Methods mzero :: Vector a Source # mplus :: Vector a -> Vector a -> Vector a Source #
MonadPlus Vector |
Instance details Defined in Data.Vector.Strict Methods mzero :: Vector a Source # mplus :: Vector a -> Vector a -> Vector a Source #
MonadPlus Maybe | Picks the leftmost `Just` value, or, alternatively, `Nothing`. Since: base-2.1
Instance details Defined in GHC.Internal.Base Methods mzero :: Maybe a Source # mplus :: Maybe a -> Maybe a -> Maybe a Source #
MonadPlus [] | Combines lists by concatenation, starting from the empty list. Since: base-2.1
Instance details Defined in GHC.Internal.Base Methods mzero :: [a] Source # mplus :: [a] -> [a] -> [a] Source #
(Functor m, Applicative m, Monad m) => MonadPlus (ListT m) Source # |
Instance details Defined in Agda.Utils.ListT Methods mzero :: ListT m a Source # mplus :: ListT m a -> ListT m a -> ListT m a Source #
Monad m => MonadPlus (CatchT m) |
Instance details Defined in Control.Monad.Catch.Pure Methods mzero :: CatchT m a Source # mplus :: CatchT m a -> CatchT m a -> CatchT m a Source #
MonadPlus r => MonadPlus (Data r) |
Instance details Defined in Generic.Data.Internal.Data Methods mzero :: Data r a Source # mplus :: Data r a -> Data r a -> Data r a Source #
(ArrowApply a, ArrowPlus a) => MonadPlus (ArrowMonad a) | Since: base-4.6.0.0
Instance details Defined in GHC.Internal.Control.Arrow Methods mzero :: ArrowMonad a a0 Source # mplus :: ArrowMonad a a0 -> ArrowMonad a a0 -> ArrowMonad a a0 Source #
MonadPlus (Proxy :: Type -> Type) | Since: base-4.9.0.0
Instance details Defined in GHC.Internal.Data.Proxy Methods mzero :: Proxy a Source # mplus :: Proxy a -> Proxy a -> Proxy a Source #
MonadPlus (U1 :: Type -> Type) | Since: base-4.9.0.0
Instance details Defined in GHC.Internal.Generics Methods mzero :: U1 a Source # mplus :: U1 a -> U1 a -> U1 a Source #
Monad m => MonadPlus (MaybeT m) |
Instance details Defined in Control.Monad.Trans.Maybe Methods mzero :: MaybeT m a Source # mplus :: MaybeT m a -> MaybeT m a -> MaybeT m a Source #
MonadPlus m => MonadPlus (Kleisli m a) | Since: base-4.14.0.0
Instance details Defined in GHC.Internal.Control.Arrow Methods mzero :: Kleisli m a a0 Source # mplus :: Kleisli m a a0 -> Kleisli m a a0 -> Kleisli m a a0 Source #
MonadPlus f => MonadPlus (Ap f) | Since: base-4.12.0.0
Instance details Defined in GHC.Internal.Data.Monoid Methods mzero :: Ap f a Source # mplus :: Ap f a -> Ap f a -> Ap f a Source #
MonadPlus f => MonadPlus (Alt f) | Since: base-4.8.0.0
Instance details Defined in GHC.Internal.Data.Semigroup.Internal Methods mzero :: Alt f a Source # mplus :: Alt f a -> Alt f a -> Alt f a Source #
MonadPlus f => MonadPlus (Rec1 f) | Since: base-4.9.0.0
Instance details Defined in GHC.Internal.Generics Methods mzero :: Rec1 f a Source # mplus :: Rec1 f a -> Rec1 f a -> Rec1 f a Source #
(Monoid w, Functor m, MonadPlus m) => MonadPlus (AccumT w m) |
Instance details Defined in Control.Monad.Trans.Accum Methods mzero :: AccumT w m a Source # mplus :: AccumT w m a -> AccumT w m a -> AccumT w m a Source #
(Monad m, Monoid e) => MonadPlus (ExceptT e m) |
Instance details Defined in Control.Monad.Trans.Except Methods mzero :: ExceptT e m a Source # mplus :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a Source #
MonadPlus m => MonadPlus (IdentityT m) |
Instance details Defined in Control.Monad.Trans.Identity Methods mzero :: IdentityT m a Source # mplus :: IdentityT m a -> IdentityT m a -> IdentityT m a Source #
MonadPlus m => MonadPlus (ReaderT r m) |
Instance details Defined in Control.Monad.Trans.Reader Methods mzero :: ReaderT r m a Source # mplus :: ReaderT r m a -> ReaderT r m a -> ReaderT r m a Source #
MonadPlus m => MonadPlus (SelectT r m) |
Instance details Defined in Control.Monad.Trans.Select Methods mzero :: SelectT r m a Source # mplus :: SelectT r m a -> SelectT r m a -> SelectT r m a Source #
MonadPlus m => MonadPlus (StateT s m) |
Instance details Defined in Control.Monad.Trans.State.Lazy Methods mzero :: StateT s m a Source # mplus :: StateT s m a -> StateT s m a -> StateT s m a Source #
MonadPlus m => MonadPlus (StateT s m) |
Instance details Defined in Control.Monad.Trans.State.Strict Methods mzero :: StateT s m a Source # mplus :: StateT s m a -> StateT s m a -> StateT s m a Source #
(Functor m, MonadPlus m) => MonadPlus (WriterT w m) |
Instance details Defined in Control.Monad.Trans.Writer.CPS Methods mzero :: WriterT w m a Source # mplus :: WriterT w m a -> WriterT w m a -> WriterT w m a Source #
(Monoid w, MonadPlus m) => MonadPlus (WriterT w m) |
Instance details Defined in Control.Monad.Trans.Writer.Lazy Methods mzero :: WriterT w m a Source # mplus :: WriterT w m a -> WriterT w m a -> WriterT w m a Source #
(Monoid w, MonadPlus m) => MonadPlus (WriterT w m) |
Instance details Defined in Control.Monad.Trans.Writer.Strict Methods mzero :: WriterT w m a Source # mplus :: WriterT w m a -> WriterT w m a -> WriterT w m a Source #
MonadPlus m => MonadPlus (Reverse m) | Derived instance.
Instance details Defined in Data.Functor.Reverse Methods mzero :: Reverse m a Source # mplus :: Reverse m a -> Reverse m a -> Reverse m a Source #
(MonadPlus f, MonadPlus g) => MonadPlus (Product f g) | Since: base-4.9.0.0
Instance details Defined in Data.Functor.Product Methods mzero :: Product f g a Source # mplus :: Product f g a -> Product f g a -> Product f g a Source #
(MonadPlus f, MonadPlus g) => MonadPlus (f :*: g) | Since: base-4.9.0.0
Instance details Defined in GHC.Internal.Generics Methods mzero :: (f :*: g) a Source # mplus :: (f :*: g) a -> (f :*: g) a -> (f :*: g) a Source #
MonadPlus f => MonadPlus (M1 i c f) | Since: base-4.9.0.0
Instance details Defined in GHC.Internal.Generics Methods mzero :: M1 i c f a Source # mplus :: M1 i c f a -> M1 i c f a -> M1 i c f a Source #
(Functor m, MonadPlus m) => MonadPlus (RWST r w s m) |
Instance details Defined in Control.Monad.Trans.RWS.CPS Methods mzero :: RWST r w s m a Source # mplus :: RWST r w s m a -> RWST r w s m a -> RWST r w s m a Source #
(Monoid w, MonadPlus m) => MonadPlus (RWST r w s m) |
Instance details Defined in Control.Monad.Trans.RWS.Lazy Methods mzero :: RWST r w s m a Source # mplus :: RWST r w s m a -> RWST r w s m a -> RWST r w s m a Source #
(Monoid w, MonadPlus m) => MonadPlus (RWST r w s m) |
Instance details Defined in Control.Monad.Trans.RWS.Strict Methods mzero :: RWST r w s m a Source # mplus :: RWST r w s m a -> RWST r w s m a -> RWST r w s m a Source #

liftM2 :: Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r Source #

Promote a function to a monad, scanning the monadic arguments from left to right.

#### Examples

Expand

    >>> liftM2 (+) [0,1] [0,2]
    [0,2,1,3]

    >>> liftM2 (+) (Just 1) Nothing
    Nothing

    >>> liftM2 (+) (+ 3) (* 2) 5
    18

void :: Functor f => f a -> f () Source #

``void` value` discards or ignores the result of evaluation, such as the return value of an `IO` action.

#### Examples

Expand

Replace the contents of a ``Maybe` `Int`` with unit:

    >>> void Nothing
    Nothing

    >>> void (Just 3)
    Just ()

Replace the contents of an ``Either` `Int` `Int`` with unit, resulting in an ``Either` `Int` `()``:

    >>> void (Left 8675309)
    Left 8675309

    >>> void (Right 8675309)
    Right ()

Replace every element of a list with unit:

    >>> void [1,2,3]
    [(),(),()]

Replace the second element of a pair with unit:

    >>> void (1,2)
    (1,())

Discard the result of an `IO` action:

    >>> mapM print [1,2]
    1
    2
    [(),()]

    >>> void $ mapM print [1,2]
    1
    2

liftA2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c Source #

Lift a binary function to actions.

Some functors support an implementation of `liftA2` that is more efficient than the default one. In particular, if `fmap` is an expensive operation, it is likely better to use `liftA2` than to `fmap` over the structure and then use `<*>`.

This became a typeclass method in 4.10.0.0. Prior to that, it was a function defined in terms of `<*>` and `fmap`.

#### Example

Expand

    >>> liftA2 (,) (Just 3) (Just 5)
    Just (3,5)

    >>> liftA2 (+) [1, 2, 3] [4, 5, 6]
    [5,6,7,6,7,8,7,8,9]

join :: Monad m => m (m a) -> m a Source #

The `join` function is the conventional monad join operator. It is used to remove one level of monadic structure, projecting its bound argument into the outer level.

'``join` bss`' can be understood as the `do` expression

    do bs <- bss
       bs

#### Examples

Expand

    >>> join [[1, 2, 3], [4, 5, 6], [7, 8, 9]]
    [1,2,3,4,5,6,7,8,9]

    >>> join (Just (Just 3))
    Just 3

A common use of `join` is to run an `IO` computation returned from an `STM` transaction, since `STM` transactions can't perform `IO` directly. Recall that

    atomically :: STM a -> IO a

is used to run `STM` transactions atomically. So, by specializing the types of `atomically` and `join` to

    atomically :: STM (IO b) -> IO (IO b)
    join       :: IO (IO b)  -> IO b

we can compose them as

    join . atomically :: STM (IO b) -> IO b

to run an `STM` transaction and the `IO` action it returns.

class (forall (m :: Type -> Type). Monad m => Monad (t m)) => MonadTrans (t :: (Type -> Type) -> Type -> Type) where Source #

The class of monad transformers. For any monad `m`, the result `t m` should also be a monad, and `lift` should be a monad transformation from `m` to `t m`, i.e. it should satisfy the following laws:

-     lift . return = return

-     lift (m >>= f) = lift m >>= (lift . f)

Since 0.6.0.0 and for GHC 8.6 and later, the requirement that `t m` be a `Monad` is enforced by the implication constraint `forall m. `Monad` m => `Monad` (t m)` enabled by the `QuantifiedConstraints` extension.

### Ambiguity error with GHC 9.0 to 9.2.2

Expand

These versions of GHC have a bug (https://gitlab.haskell.org/ghc/ghc/-/issues/20582) which causes constraints like

    (MonadTrans t, forall m. Monad m => Monad (t m)) => ...

to be reported as ambiguous. For transformers 0.6 and later, this can be fixed by removing the second constraint, which is implied by the first.

Methods

lift :: Monad m => m a -> t m a Source #

Lift a computation from the argument monad to the constructed monad.

#### Instances

Instances details

MonadTrans PureConversionT Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods lift :: Monad m => m a -> PureConversionT m a Source #
MonadTrans BlockT Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lift :: Monad m => m a -> BlockT m a Source #
MonadTrans TCMT Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lift :: Monad m => m a -> TCMT m a Source #
MonadTrans NamesT Source # |
Instance details Defined in Agda.TypeChecking.Names Methods lift :: Monad m => m a -> NamesT m a Source #
MonadTrans ListT Source # |
Instance details Defined in Agda.Utils.ListT Methods lift :: Monad m => m a -> ListT m a Source #
MonadTrans ChangeT Source # |
Instance details Defined in Agda.Utils.Update Methods lift :: Monad m => m a -> ChangeT m a Source #
MonadTrans CatchT |
Instance details Defined in Control.Monad.Catch.Pure Methods lift :: Monad m => m a -> CatchT m a Source #
MonadTrans InputT |
Instance details Defined in System.Console.Haskeline.InputT Methods lift :: Monad m => m a -> InputT m a Source #
MonadTrans MaybeT |
Instance details Defined in Control.Monad.Trans.Maybe Methods lift :: Monad m => m a -> MaybeT m a Source #
MonadTrans (STT s) |
Instance details Defined in Control.Monad.ST.Trans.Internal Methods lift :: Monad m => m a -> STT s m a Source #
Monoid w => MonadTrans (AccumT w) |
Instance details Defined in Control.Monad.Trans.Accum Methods lift :: Monad m => m a -> AccumT w m a Source #
MonadTrans (ExceptT e) |
Instance details Defined in Control.Monad.Trans.Except Methods lift :: Monad m => m a -> ExceptT e m a Source #
MonadTrans (IdentityT :: (Type -> Type) -> Type -> Type) |
Instance details Defined in Control.Monad.Trans.Identity Methods lift :: Monad m => m a -> IdentityT m a Source #
MonadTrans (ReaderT r) |
Instance details Defined in Control.Monad.Trans.Reader Methods lift :: Monad m => m a -> ReaderT r m a Source #
MonadTrans (SelectT r) |
Instance details Defined in Control.Monad.Trans.Select Methods lift :: Monad m => m a -> SelectT r m a Source #
MonadTrans (StateT s) |
Instance details Defined in Control.Monad.Trans.State.Lazy Methods lift :: Monad m => m a -> StateT s m a Source #
MonadTrans (StateT s) |
Instance details Defined in Control.Monad.Trans.State.Strict Methods lift :: Monad m => m a -> StateT s m a Source #
MonadTrans (WriterT w) |
Instance details Defined in Control.Monad.Trans.Writer.CPS Methods lift :: Monad m => m a -> WriterT w m a Source #
Monoid w => MonadTrans (WriterT w) |
Instance details Defined in Control.Monad.Trans.Writer.Lazy Methods lift :: Monad m => m a -> WriterT w m a Source #
Monoid w => MonadTrans (WriterT w) |
Instance details Defined in Control.Monad.Trans.Writer.Strict Methods lift :: Monad m => m a -> WriterT w m a Source #
MonadTrans (ContT r) |
Instance details Defined in Control.Monad.Trans.Cont Methods lift :: Monad m => m a -> ContT r m a Source #
MonadTrans (EquivT s c v) |
Instance details Defined in Data.Equivalence.Monad Methods lift :: Monad m => m a -> EquivT s c v m a Source #
MonadTrans (RWST r w s) |
Instance details Defined in Control.Monad.Trans.RWS.CPS Methods lift :: Monad m => m a -> RWST r w s m a Source #
Monoid w => MonadTrans (RWST r w s) |
Instance details Defined in Control.Monad.Trans.RWS.Lazy Methods lift :: Monad m => m a -> RWST r w s m a Source #
Monoid w => MonadTrans (RWST r w s) |
Instance details Defined in Control.Monad.Trans.RWS.Strict Methods lift :: Monad m => m a -> RWST r w s m a Source #

forM_ :: (Foldable t, Monad m) => t a -> (a -> m b) -> m () Source #

`forM_` is `mapM_` with its arguments flipped. For a version that doesn't ignore the results see `forM`.

`forM_` is just like `for_`, but specialised to monadic actions.

liftM3 :: Monad m => (a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r Source #

Promote a function to a monad, scanning the monadic arguments from left to right (cf. `liftM2`).

liftM4 :: Monad m => (a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r Source #

Promote a function to a monad, scanning the monadic arguments from left to right (cf. `liftM2`).

msum :: (Foldable t, MonadPlus m) => t (m a) -> m a Source #

The sum of a collection of actions using `(<|>)`, generalizing `concat`.

`msum` is just like `asum`, but specialised to `MonadPlus`.

#### Examples

Expand

Basic usage, using the `MonadPlus` instance for `Maybe`:

    >>> msum [Just "Hello", Nothing, Just "World"]
    Just "Hello"

forM :: (Traversable t, Monad m) => t a -> (a -> m b) -> m (t b) Source #

`forM` is `mapM` with its arguments flipped. For a version that ignores the results see `forM_`.

filterM :: Applicative m => (a -> m Bool) -> [a] -> m [a] Source #

This generalizes the list-based `filter` function.

    runIdentity (filterM (Identity . p) xs) == filter p xs

#### Examples

Expand

    >>> filterM (\x -> do
          putStrLn ("Keep: " ++ show x ++ "?")
          answer <- getLine
          pure (answer == "y"))
        [1, 2, 3]
    Keep: 1?
    y
    Keep: 2?
    n
    Keep: 3?
    y
    [1,3]

    >>> filterM (\x -> do
          putStr (show x)
          x' <- readLn
          pure (x == x'))
        [1, 2, 3]
    12
    22
    33
    [2,3]

(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c infixr 1 Source #

Left-to-right composition of `Kleisli` arrows.

'`(bs `>=>` cs) a`' can be understood as the `do` expression

    do b <- bs a
       cs b

or in terms of ``(>>=)`` as

    bs a >>= cs

(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c infixr 1 Source #

Right-to-left composition of Kleisli arrows. `(`>=>`)`, with the arguments flipped.

Note how this operator resembles function composition `(`.`)`:

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

zipWithM :: Applicative m => (a -> b -> m c) -> [a] -> [b] -> m [c] Source #

The `zipWithM` function generalizes `zipWith` to arbitrary applicative functors.

zipWithM_ :: Applicative m => (a -> b -> m c) -> [a] -> [b] -> m () Source #

`zipWithM_` is the extension of `zipWithM` which ignores the final result.

foldM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b Source #

The `foldM` function is analogous to `foldl`, except that its result is encapsulated in a monad. Note that `foldM` works from left-to-right over the list arguments. This could be an issue where `(`>>`)` and the `folded function' are not commutative.

    foldM f a1 [x1, x2, ..., xm]

    ==

    do
      a2 <- f a1 x1
      a3 <- f a2 x2
      ...
      f am xm

If right-to-left evaluation is required, the input list should be reversed.

Note: `foldM` is the same as `foldlM`

(<$!>) :: Monad m => (a -> b) -> m a -> m b infixl 4 Source #

Strict version of `<$>`.

Since: base-4.8.0.0

tryError :: MonadError e m => m a -> m (Either e a) Source #

`MonadError` analogue to the `try` function.

withError :: MonadError e m => (e -> e) -> m a -> m a Source #

`MonadError` analogue to the `withExceptT` function. Modify the value (but not the type) of an error. The type is fixed because of the functional dependency `m -> e`. If you need to change the type of `e` use `mapError` or `modifyError`.

(<$>) :: Functor f => (a -> b) -> f a -> f b infixl 4 Source #

An infix synonym for `fmap`.

The name of this operator is an allusion to `$`. Note the similarities between their types:

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

Whereas `$` is function application, `<$>` is function application lifted over a `Functor`.

#### Examples

Expand

Convert from a ``Maybe` `Int`` to a ``Maybe` `String`` using `show`:

    >>> show <$> Nothing
    Nothing

    >>> show <$> Just 3
    Just "3"

Convert from an ``Either` `Int` `Int`` to an ``Either` `Int`` `String` using `show`:

    >>> show <$> Left 17
    Left 17

    >>> show <$> Right 17
    Right "17"

Double each element of a list:

    >>> (*2) <$> [1,2,3]
    [2,4,6]

Apply `even` to the second element of a pair:

    >>> even <$> (2,2)
    (2,True)

(<*>) :: Applicative f => f (a -> b) -> f a -> f b infixl 4 Source #

Sequential application.

A few functors support an implementation of `<*>` that is more efficient than the default one.

#### Example

Expand

Used in combination with ``(<$>)``, ``(<*>)`` can be used to build a record.

    >>> data MyState = MyState {arg1 :: Foo, arg2 :: Bar, arg3 :: Baz}

    >>> produceFoo :: Applicative f => f Foo
    >>> produceBar :: Applicative f => f Bar
    >>> produceBaz :: Applicative f => f Baz

    >>> mkState :: Applicative f => f MyState
    >>> mkState = MyState <$> produceFoo <*> produceBar <*> produceBaz

(<$) :: Functor f => a -> f b -> f a infixl 4 Source #

Replace all locations in the input with the same value. The default definition is ``fmap` . `const``, but this may be overridden with a more efficient version.

#### Examples

Expand

Perform a computation with `Maybe` and replace the result with a constant value if it is `Just`:

    >>> 'a' <$ Just 2
    Just 'a'
    >>> 'a' <$ Nothing
    Nothing