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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Monad

Contents

- Orphan instances

Synopsis

- (==<<) :: Monad m => (a -> b -> m c) -> (m a, m b) -> m c
- whenM :: Monad m => m Bool -> m () -> m ()
- unlessM :: Monad m => m Bool -> m () -> m ()
- guardM :: (Monad m, MonadPlus m) => m Bool -> m ()
- ifM :: Monad m => m Bool -> m a -> m a -> m a
- ifNotM :: Monad m => m Bool -> m a -> m a -> m a
- and2M :: Monad m => m Bool -> m Bool -> m Bool
- andM :: (Foldable f, Monad m) => f (m Bool) -> m Bool
- allM :: (Functor f, Foldable f, Monad m) => f a -> (a -> m Bool) -> m Bool
- or2M :: Monad m => m Bool -> m Bool -> m Bool
- orM :: (Foldable f, Monad m) => f (m Bool) -> m Bool
- anyM :: (Functor f, 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, 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
- 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)
- mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
- forMaybeM :: Monad m => [a] -> (a -> m (Maybe b)) -> m [b]
- dropWhileM :: Monad m => (a -> m Bool) -> [a] -> m [a]
- 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
- finally :: MonadError e m => m a -> m () -> m a
- tryMaybe :: (MonadError e m, Functor m) => m a -> m (Maybe a)
- bracket_ :: Monad m => m a -> (a -> m ()) -> m b -> m b
- localState :: MonadState s m => m a -> m a
- readM :: (Error e, MonadError e m, Read a) => String -> m a
- when :: Applicative f => Bool -> f () -> f ()
- unless :: Applicative f => Bool -> f () -> f ()
- class (Alternative m, Monad m) => MonadPlus (m :: Type -> Type) where
  - mzero :: m a
  - mplus :: m a -> 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

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

Binary bind.

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

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

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

Monadic guard.

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

Monadic if-then-else.

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

    ifNotM mc = ifM (not $ mc)

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

Lazy monadic conjunction.

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

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

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

Lazy monadic disjunction.

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

anyM :: (Functor f, 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, Monad m, Monoid b) => (a -> m b) -> t a -> m b Source #

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

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

Generalized version of `forM_ :: Monad 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 #

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

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

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

The `for` version of `mapMaybeM`.

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

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

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`.

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.

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

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

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.

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

Restore state after computation.

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

when :: Applicative f => Bool -> f () -> f () Source #

Conditional execution of `Applicative` expressions. For example,

    when debug (putStrLn "Debugging")

will output the string `Debugging` if the Boolean value `debug` is `True`, and otherwise do nothing.

unless :: Applicative f => Bool -> f () -> f () Source #

The reverse of `when`.

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

MonadPlus [] | Since: base-2.1
Instance details Defined in GHC.Base Methods mzero :: [a] Source # mplus :: [a] -> [a] -> [a] Source #
MonadPlus Maybe | Since: base-2.1
Instance details Defined in GHC.Base Methods mzero :: Maybe a Source # mplus :: Maybe a -> Maybe a -> Maybe a Source #
MonadPlus IO | Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods mzero :: IO a Source # mplus :: IO a -> IO a -> IO a Source #
MonadPlus Seq |
Instance details Defined in Data.Edison.Seq.SimpleQueue Methods mzero :: Seq a Source # mplus :: Seq a -> Seq a -> Seq a Source #
MonadPlus Seq |
Instance details Defined in Data.Edison.Seq.BankersQueue Methods mzero :: Seq a Source # mplus :: Seq a -> Seq a -> Seq 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 Result |
Instance details Defined in Data.Aeson.Types.Internal Methods mzero :: Result a Source # mplus :: Result a -> Result a -> Result 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 Option | Since: base-4.9.0.0
Instance details Defined in Data.Semigroup Methods mzero :: Option a Source # mplus :: Option a -> Option a -> Option a Source #
MonadPlus STM | Since: base-4.3.0.0
Instance details Defined in GHC.Conc.Sync Methods mzero :: STM a Source # mplus :: STM a -> STM a -> STM a Source #
MonadPlus ReadPrec | Since: base-2.1
Instance details Defined in Text.ParserCombinators.ReadPrec Methods mzero :: ReadPrec a Source # mplus :: ReadPrec a -> ReadPrec a -> ReadPrec a Source #
MonadPlus ReadP | Since: base-2.1
Instance details Defined in Text.ParserCombinators.ReadP Methods mzero :: ReadP a Source # mplus :: ReadP a -> ReadP a -> ReadP a Source #
MonadPlus Get | Since: 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 P | Since: base-2.1
Instance details Defined in Text.ParserCombinators.ReadP Methods mzero :: P a Source # mplus :: P a -> P a -> P 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 DList |
Instance details Defined in Data.DList Methods mzero :: DList a Source # mplus :: DList a -> DList a -> DList a Source #
MonadPlus (U1 :: Type -> Type) | Since: base-4.9.0.0
Instance details Defined in GHC.Generics Methods mzero :: U1 a Source # mplus :: U1 a -> U1 a -> U1 a Source #
(ArrowApply a, ArrowPlus a) => MonadPlus (ArrowMonad a) | Since: base-4.6.0.0
Instance details Defined in 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 Data.Proxy Methods mzero :: Proxy a Source # mplus :: Proxy a -> Proxy a -> Proxy 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 #
Monad m => MonadPlus (ListT m) |
Instance details Defined in Control.Monad.Trans.List Methods mzero :: ListT m a Source # mplus :: ListT m a -> ListT m a -> ListT m 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 #
MonadPlus (ReadP t) Source # |
Instance details Defined in Agda.Utils.Parser.ReadP Methods mzero :: ReadP t a Source # mplus :: ReadP t a -> ReadP t a -> ReadP t a Source #
MonadPlus (Parser i) |
Instance details Defined in Data.Attoparsec.Internal.Types Methods mzero :: Parser i a Source # mplus :: Parser i a -> Parser i a -> Parser i a Source #
MonadPlus f => MonadPlus (Rec1 f) | Since: base-4.9.0.0
Instance details Defined in GHC.Generics Methods mzero :: Rec1 f a Source # mplus :: Rec1 f a -> Rec1 f a -> Rec1 f a Source #
MonadPlus f => MonadPlus (Ap f) | Since: base-4.12.0.0
Instance details Defined in 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 Data.Semigroup.Internal Methods mzero :: Alt f a Source # mplus :: Alt f a -> Alt f a -> Alt f 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 (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 (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 #
(Monad m, Error e) => MonadPlus (ErrorT e m) |
Instance details Defined in Control.Monad.Trans.Error Methods mzero :: ErrorT e m a Source # mplus :: ErrorT e m a -> ErrorT e m a -> ErrorT e 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 #
(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 f, MonadPlus g) => MonadPlus (f :*: g) | Since: base-4.9.0.0
Instance details Defined in GHC.Generics Methods mzero :: (f :*: g) a Source # mplus :: (f :*: g) a -> (f :*: g) a -> (f :*: g) 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 (M1 i c f) | Since: base-4.9.0.0
Instance details Defined in GHC.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 #
(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 #

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

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

# Orphan instances

MonadFail Identity Source # |
Instance details Methods fail :: String -> Identity a Source #