Agda-2.6.2.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Monad

Synopsis

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, 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 #

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

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

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.

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.

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

Branch over elements of a monadic Foldable data structure.

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.

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

Run a command, catch the exception and return it.

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

Like guard, but raise given error when condition fails.

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.

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

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 () #

The reverse of when.

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

Monads that also support choice and failure.

Minimal complete definition

Nothing

Methods

mzero :: m a #

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 #

An associative operation. The default definition is

mplus = (<|>)

Instances

Instances details
MonadPlus []

Since: base-2.1

Instance details

Defined in GHC.Base

Methods

mzero :: [a] #

mplus :: [a] -> [a] -> [a] #

MonadPlus Maybe

Since: base-2.1

Instance details

Defined in GHC.Base

Methods

mzero :: Maybe a #

mplus :: Maybe a -> Maybe a -> Maybe a #

MonadPlus IO

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

mzero :: IO a #

mplus :: IO a -> IO a -> IO a #

MonadPlus IResult 
Instance details

Defined in Data.Aeson.Types.Internal

Methods

mzero :: IResult a #

mplus :: IResult a -> IResult a -> IResult a #

MonadPlus Result 
Instance details

Defined in Data.Aeson.Types.Internal

Methods

mzero :: Result a #

mplus :: Result a -> Result a -> Result a #

MonadPlus Parser 
Instance details

Defined in Data.Aeson.Types.Internal

Methods

mzero :: Parser a #

mplus :: Parser a -> Parser a -> Parser a #

MonadPlus Option

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup

Methods

mzero :: Option a #

mplus :: Option a -> Option a -> Option a #

MonadPlus STM

Since: base-4.3.0.0

Instance details

Defined in GHC.Conc.Sync

Methods

mzero :: STM a #

mplus :: STM a -> STM a -> STM a #

MonadPlus ReadPrec

Since: base-2.1

Instance details

Defined in Text.ParserCombinators.ReadPrec

Methods

mzero :: ReadPrec a #

mplus :: ReadPrec a -> ReadPrec a -> ReadPrec a #

MonadPlus ReadP

Since: base-2.1

Instance details

Defined in Text.ParserCombinators.ReadP

Methods

mzero :: ReadP a #

mplus :: ReadP a -> ReadP a -> ReadP a #

MonadPlus Get

Since: binary-0.7.1.0

Instance details

Defined in Data.Binary.Get.Internal

Methods

mzero :: Get a #

mplus :: Get a -> Get a -> Get a #

MonadPlus Seq 
Instance details

Defined in Data.Sequence.Internal

Methods

mzero :: Seq a #

mplus :: Seq a -> Seq a -> Seq a #

MonadPlus DList 
Instance details

Defined in Data.DList.Internal

Methods

mzero :: DList a #

mplus :: DList a -> DList a -> DList a #

MonadPlus SmallArray 
Instance details

Defined in Data.Primitive.SmallArray

MonadPlus Array 
Instance details

Defined in Data.Primitive.Array

Methods

mzero :: Array a #

mplus :: Array a -> Array a -> Array a #

MonadPlus Vector 
Instance details

Defined in Data.Vector

Methods

mzero :: Vector a #

mplus :: Vector a -> Vector a -> Vector a #

MonadPlus P

Since: base-2.1

Instance details

Defined in Text.ParserCombinators.ReadP

Methods

mzero :: P a #

mplus :: P a -> P a -> P a #

MonadPlus NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

mzero :: NLM a #

mplus :: NLM a -> NLM a -> NLM a #

MonadPlus (U1 :: Type -> Type)

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Methods

mzero :: U1 a #

mplus :: U1 a -> U1 a -> U1 a #

MonadPlus (Parser i) 
Instance details

Defined in Data.Attoparsec.Internal.Types

Methods

mzero :: Parser i a #

mplus :: Parser i a -> Parser i a -> Parser i a #

(ArrowApply a, ArrowPlus a) => MonadPlus (ArrowMonad a)

Since: base-4.6.0.0

Instance details

Defined in Control.Arrow

Methods

mzero :: ArrowMonad a a0 #

mplus :: ArrowMonad a a0 -> ArrowMonad a a0 -> ArrowMonad a a0 #

MonadPlus (Proxy :: Type -> Type)

Since: base-4.9.0.0

Instance details

Defined in Data.Proxy

Methods

mzero :: Proxy a #

mplus :: Proxy a -> Proxy a -> Proxy a #

Monad m => MonadPlus (MaybeT m) 
Instance details

Defined in Control.Monad.Trans.Maybe

Methods

mzero :: MaybeT m a #

mplus :: MaybeT m a -> MaybeT m a -> MaybeT m a #

Monad m => MonadPlus (ListT m) 
Instance details

Defined in Control.Monad.Trans.List

Methods

mzero :: ListT m a #

mplus :: ListT m a -> ListT m a -> ListT m a #

(Functor m, Applicative m, Monad m) => MonadPlus (ListT m) Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

mzero :: ListT m a #

mplus :: ListT m a -> ListT m a -> ListT m a #

MonadPlus f => MonadPlus (Rec1 f)

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Methods

mzero :: Rec1 f a #

mplus :: Rec1 f a -> Rec1 f a -> Rec1 f a #

MonadPlus m => MonadPlus (Kleisli m a)

Since: base-4.14.0.0

Instance details

Defined in Control.Arrow

Methods

mzero :: Kleisli m a a0 #

mplus :: Kleisli m a a0 -> Kleisli m a a0 -> Kleisli m a a0 #

MonadPlus f => MonadPlus (Ap f)

Since: base-4.12.0.0

Instance details

Defined in Data.Monoid

Methods

mzero :: Ap f a #

mplus :: Ap f a -> Ap f a -> Ap f a #

MonadPlus f => MonadPlus (Alt f)

Since: base-4.8.0.0

Instance details

Defined in Data.Semigroup.Internal

Methods

mzero :: Alt f a #

mplus :: Alt f a -> Alt f a -> Alt f a #

MonadPlus m => MonadPlus (IdentityT m) 
Instance details

Defined in Control.Monad.Trans.Identity

Methods

mzero :: IdentityT m a #

mplus :: IdentityT m a -> IdentityT m a -> IdentityT m a #

(Monad m, Monoid e) => MonadPlus (ExceptT e m) 
Instance details

Defined in Control.Monad.Trans.Except

Methods

mzero :: ExceptT e m a #

mplus :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a #

MonadPlus m => MonadPlus (ReaderT r m) 
Instance details

Defined in Control.Monad.Trans.Reader

Methods

mzero :: ReaderT r m a #

mplus :: ReaderT r m a -> ReaderT r m a -> ReaderT r m a #

MonadPlus m => MonadPlus (StateT s m) 
Instance details

Defined in Control.Monad.Trans.State.Strict

Methods

mzero :: StateT s m a #

mplus :: StateT s m a -> StateT s m a -> StateT s m a #

(Monoid w, MonadPlus m) => MonadPlus (WriterT w m) 
Instance details

Defined in Control.Monad.Trans.Writer.Lazy

Methods

mzero :: WriterT w m a #

mplus :: WriterT w m a -> WriterT w m a -> WriterT w m a #

MonadPlus m => MonadPlus (StateT s m) 
Instance details

Defined in Control.Monad.Trans.State.Lazy

Methods

mzero :: StateT s m a #

mplus :: StateT s m a -> StateT s m a -> StateT s m a #

(Monad m, Error e) => MonadPlus (ErrorT e m) 
Instance details

Defined in Control.Monad.Trans.Error

Methods

mzero :: ErrorT e m a #

mplus :: ErrorT e m a -> ErrorT e m a -> ErrorT e m a #

(Monoid w, MonadPlus m) => MonadPlus (WriterT w m) 
Instance details

Defined in Control.Monad.Trans.Writer.Strict

Methods

mzero :: WriterT w m a #

mplus :: WriterT w m a -> WriterT w m a -> WriterT w m a #

(MonadPlus f, MonadPlus g) => MonadPlus (f :*: g)

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Methods

mzero :: (f :*: g) a #

mplus :: (f :*: g) a -> (f :*: g) a -> (f :*: g) a #

(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 #

mplus :: Product f g a -> Product f g a -> Product f g a #

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 #

mplus :: M1 i c f a -> M1 i c f a -> M1 i c f a #

(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 #

mplus :: RWST r w s m a -> RWST r w s m a -> RWST r w s m a #

(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 #

mplus :: RWST r w s m a -> RWST r w s m a -> RWST r w s m a #

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

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 #

Sequential application.

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

Using ApplicativeDo: 'fs <*> as' can be understood as the do expression

do f <- fs
   a <- as
   pure (f a)

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

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.

Using ApplicativeDo: 'a <$ bs' can be understood as the do expression

do bs
   pure a

with an inferred Functor constraint.