Agda.Utils.Monad

Strict ap

Binary bind.

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

Lazy monadic conjunction.

Bracket without failure. Typically used to preserve state.

Generalises the catMaybes function from lists to an arbitrary MonadPlus.

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

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

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

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

The for version of mapMaybeM.

The for version of mapMaybeMM.

Translates Maybe to MonadPlus.

Monadic guard.

Like guard, but raise given error when condition fails.

Monadic if-then-else.

Restore state after computation.

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.

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

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

Lazy monadic disjunction.

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

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

Branch over elements of a monadic Foldable data structure.

Output a single value.

Run a command, catch the exception and return it.

Try a computation, return Nothing if an Error occurs.

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

>>> 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 GHC.Conc.STM transaction, since GHC.Conc.STM transactions can't perform IO directly. Recall that

GHC.Internal.Conc.atomically :: STM a -> IO a

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

GHC.Internal.Conc.atomically :: STM (IO b) -> IO (IO b)
join       :: IO (IO b)  -> IO b

we can compose them as

join . GHC.Internal.Conc.atomically :: STM (IO b) -> IO b

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

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

This function can be used to define `liftA2 = liftM2`, if Monad is already defined for a data type.

Examples

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

>>> liftM2 (+) (Just 1) NothingNothing

>>> liftM2 (+) (+ 3) (* 2) 518

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

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

Strict version of <$>.

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

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

This generalizes the list-based Data.List.filter function.

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

Examples

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

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

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

The zipWithM function generalizes zipWith to arbitrary applicative functors.

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

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

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

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

msum is just like asum, but specialised to MonadPlus.

Examples

Basic usage, using the MonadPlus instance for Maybe:

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

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

Examples

Replace the contents of a Maybe Int with unit:

>>> void NothingNothing

>>> 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 System.IO.IO action:

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

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

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

MonadError analogue to the try function.

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.

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

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

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

Monads that also support choice and failure.

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

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.

An infix synonym for fmap.

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

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

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

Examples

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

>>> show <$> NothingNothing

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

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

>>> show <$> Left 17Left 17

>>> show <$> Right 17Right "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)

Sequential application.

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

Example

Used in combination with (Data.Functor.<$>), (<*>) 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

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

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

>>> 'a' <$ Just 2Just 'a'>>> 'a' <$ NothingNothing