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

Contents

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 #

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

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.

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

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

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

# Orphan instances

 Source # Instance details Methodsfail :: String -> Identity a #