Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Monad

Synopsis

Documentation

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

Strict ap

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

Binary bind.

allM :: (Foldable f, Monad m) => (a -> m Bool) -> f a -> 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.

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

Lazy monadic conjunction.

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

anyM :: (Foldable f, Monad m) => (a -> m Bool) -> f a -> m Bool 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.

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

Generalises the catMaybes function from lists to an arbitrary MonadPlus.

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

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.

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

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

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

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

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.

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

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

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

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.

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

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

Translates Maybe to MonadPlus.

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

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

Monadic guard.

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

Like guard, but raise given error when condition fails.

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)

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

Restore state after computation.

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.

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

mapMM_ :: (Foldable t, Monad m) => (a -> m ()) -> m (t a) -> 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.

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

Lazy monadic disjunction.

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.

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

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

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

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

Branch over elements of a monadic Foldable data structure.

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

Output a single value.

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

Run a command, catch the exception and return it.

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

Try a computation, return Nothing if an Error occurs.

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

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

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

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

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

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.

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

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

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

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 #

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

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

Strict version of <$>.

Since: base-4.8.0.0

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

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

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

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

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

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]

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

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

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

The zipWithM function generalizes zipWith to arbitrary applicative functors.

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

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

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

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.

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

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"

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

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

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

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

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

MonadError analogue to the try function.

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

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.

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

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]

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 NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

mzero :: NLM a #

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

MonadPlus IResult # 
Instance details

Defined in Data.Aeson.Types.Internal

Methods

mzero :: IResult a #

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

MonadPlus Parser # 
Instance details

Defined in Data.Aeson.Types.Internal

Methods

mzero :: Parser a #

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

MonadPlus Result # 
Instance details

Defined in Data.Aeson.Types.Internal

Methods

mzero :: Result a #

mplus :: Result a -> Result a -> Result 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 STM #

Takes the first non-retrying STM action.

Since: base-4.3.0.0

Instance details

Defined in GHC.Internal.Conc.Sync

Methods

mzero :: STM a #

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

MonadPlus P #

Since: base-2.1

Instance details

Defined in GHC.Internal.Text.ParserCombinators.ReadP

Methods

mzero :: P a #

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

MonadPlus ReadP #

Since: base-2.1

Instance details

Defined in GHC.Internal.Text.ParserCombinators.ReadP

Methods

mzero :: ReadP a #

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

MonadPlus ReadPrec #

Since: base-2.1

Instance details

Defined in GHC.Internal.Text.ParserCombinators.ReadPrec

Methods

mzero :: ReadPrec a #

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

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 #

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

MonadPlus Array # 
Instance details

Defined in Data.Primitive.Array

Methods

mzero :: Array a #

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

MonadPlus SmallArray # 
Instance details

Defined in Data.Primitive.SmallArray

MonadPlus Vector # 
Instance details

Defined in Data.Vector

Methods

mzero :: Vector a #

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

MonadPlus Vector # 
Instance details

Defined in Data.Vector.Strict

Methods

mzero :: Vector a #

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

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 #

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

MonadPlus [] #

Combines lists by concatenation, starting from the empty list.

Since: base-2.1

Instance details

Defined in GHC.Internal.Base

Methods

mzero :: [a] #

mplus :: [a] -> [a] -> [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 #

Monad m => MonadPlus (CatchT m) # 
Instance details

Defined in Control.Monad.Catch.Pure

Methods

mzero :: CatchT m a #

mplus :: CatchT m a -> CatchT m a -> CatchT m a #

MonadPlus r => MonadPlus (Data r) # 
Instance details

Defined in Generic.Data.Internal.Data

Methods

mzero :: Data r a #

mplus :: Data r a -> Data r a -> Data r a #

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

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

MonadPlus (Proxy :: Type -> Type) #

Since: base-4.9.0.0

Instance details

Defined in GHC.Internal.Data.Proxy

Methods

mzero :: Proxy a #

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

MonadPlus (U1 :: Type -> Type) #

Since: base-4.9.0.0

Instance details

Defined in GHC.Internal.Generics

Methods

mzero :: U1 a #

mplus :: U1 a -> U1 a -> U1 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 #

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 #

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 GHC.Internal.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 GHC.Internal.Data.Semigroup.Internal

Methods

mzero :: Alt f a #

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

MonadPlus f => MonadPlus (Rec1 f) #

Since: base-4.9.0.0

Instance details

Defined in GHC.Internal.Generics

Methods

mzero :: Rec1 f a #

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

(Monoid w, Functor m, MonadPlus m) => MonadPlus (AccumT w m) # 
Instance details

Defined in Control.Monad.Trans.Accum

Methods

mzero :: AccumT w m a #

mplus :: AccumT w m a -> AccumT w m a -> AccumT w 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 (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 #

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 (SelectT r m) # 
Instance details

Defined in Control.Monad.Trans.Select

Methods

mzero :: SelectT r m a #

mplus :: SelectT r m a -> SelectT r m a -> SelectT r 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 #

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 #

(Functor m, MonadPlus m) => MonadPlus (WriterT w m) # 
Instance details

Defined in Control.Monad.Trans.Writer.CPS

Methods

mzero :: WriterT w m a #

mplus :: WriterT w m a -> WriterT w m a -> WriterT w 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 #

(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 m => MonadPlus (Reverse m) #

Derived instance.

Instance details

Defined in Data.Functor.Reverse

Methods

mzero :: Reverse m a #

mplus :: Reverse m a -> Reverse m a -> Reverse m 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 g) => MonadPlus (f :*: g) #

Since: base-4.9.0.0

Instance details

Defined in GHC.Internal.Generics

Methods

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

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

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 #

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

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

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

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

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:

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 #

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 #

MonadTrans BlockT Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

lift :: Monad m => m a -> BlockT m a #

MonadTrans TCMT Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

lift :: Monad m => m a -> TCMT m a #

MonadTrans NamesT Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

lift :: Monad m => m a -> NamesT m a #

MonadTrans ListT Source # 
Instance details

Defined in Agda.Utils.ListT

Methods

lift :: Monad m => m a -> ListT m a #

MonadTrans ChangeT Source # 
Instance details

Defined in Agda.Utils.Update

Methods

lift :: Monad m => m a -> ChangeT m a #

MonadTrans CatchT # 
Instance details

Defined in Control.Monad.Catch.Pure

Methods

lift :: Monad m => m a -> CatchT m a #

MonadTrans InputT # 
Instance details

Defined in System.Console.Haskeline.InputT

Methods

lift :: Monad m => m a -> InputT m a #

MonadTrans MaybeT # 
Instance details

Defined in Control.Monad.Trans.Maybe

Methods

lift :: Monad m => m a -> MaybeT m a #

MonadTrans (STT s) # 
Instance details

Defined in Control.Monad.ST.Trans.Internal

Methods

lift :: Monad m => m a -> STT s m a #

Monoid w => MonadTrans (AccumT w) # 
Instance details

Defined in Control.Monad.Trans.Accum

Methods

lift :: Monad m => m a -> AccumT w m a #

MonadTrans (ExceptT e) # 
Instance details

Defined in Control.Monad.Trans.Except

Methods

lift :: Monad m => m a -> ExceptT e m a #

MonadTrans (IdentityT :: (Type -> Type) -> Type -> Type) # 
Instance details

Defined in Control.Monad.Trans.Identity

Methods

lift :: Monad m => m a -> IdentityT m a #

MonadTrans (ReaderT r) # 
Instance details

Defined in Control.Monad.Trans.Reader

Methods

lift :: Monad m => m a -> ReaderT r m a #

MonadTrans (SelectT r) # 
Instance details

Defined in Control.Monad.Trans.Select

Methods

lift :: Monad m => m a -> SelectT r m a #

MonadTrans (StateT s) # 
Instance details

Defined in Control.Monad.Trans.State.Lazy

Methods

lift :: Monad m => m a -> StateT s m a #

MonadTrans (StateT s) # 
Instance details

Defined in Control.Monad.Trans.State.Strict

Methods

lift :: Monad m => m a -> StateT s m a #

MonadTrans (WriterT w) # 
Instance details

Defined in Control.Monad.Trans.Writer.CPS

Methods

lift :: Monad m => m a -> WriterT w m a #

Monoid w => MonadTrans (WriterT w) # 
Instance details

Defined in Control.Monad.Trans.Writer.Lazy

Methods

lift :: Monad m => m a -> WriterT w m a #

Monoid w => MonadTrans (WriterT w) # 
Instance details

Defined in Control.Monad.Trans.Writer.Strict

Methods

lift :: Monad m => m a -> WriterT w m a #

MonadTrans (ContT r) # 
Instance details

Defined in Control.Monad.Trans.Cont

Methods

lift :: Monad m => m a -> ContT r m a #

MonadTrans (EquivT s c v) # 
Instance details

Defined in Data.Equivalence.Monad

Methods

lift :: Monad m => m a -> EquivT s c v m a #

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 #

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 #

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 #

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

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 #

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