Agda.Utils.Monad

Monadic if-then-else.

Like guard, but raise given error when condition fails.

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

Try a computation, return Nothing if an Error occurs.

Bracket without failure. Typically used to preserve state.

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

Output a single value.

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

Binary bind.

Strict ap

Monadic guard.

Lazy monadic conjunction.

Lazy monadic disjunction.

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

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

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.

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

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

The for version of mapMaybeM.

The for version of mapMaybeMM.

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 @partition :: (a -> Bool) -> [a] -> ([a],[a])

Translates Maybe to MonadPlus.

Generalises the catMaybes function from lists to an arbitrary MonadPlus.

Branch over elements of a monadic Foldable data structure.

Run a command, catch the exception and return it.

Restore state after computation.

Conditional execution of Applicative expressions. For example,

Examples

when debug (putStrLn "Debugging")

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

>>> putStr "pi:" >> when False (print 3.14159)pi:

The reverse of when.

Examples

>>> do x <- getLine       unless (x == "hi") (putStrLn "hi!")comingupwithexamplesisdifficulthi!

>>> unless (pi > exp 1) NothingJust ()

Monads that also support choice and failure.

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

Strict version of Data.Functor.<$>.

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