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

Agda.Utils.Either

Description

Utilities for the Either type.

Synopsis

Documentation

whileLeft :: Monad m => (a -> Either b c) -> (a -> b -> m a) -> (a -> c -> m d) -> a -> m d Source #

Loop while we have an exception.

caseEitherM :: Monad m => m (Either a b) -> (a -> m c) -> (b -> m c) -> m c Source #

Monadic version of either with a different argument ordering.

mapLeft :: (a -> c) -> Either a b -> Either c b Source #

'Either _ b' is a functor.

mapRight :: (b -> d) -> Either a b -> Either a d Source #

'Either a' is a functor.

traverseEither :: Functor f => (a -> f c) -> (b -> f d) -> Either a b -> f (Either c d) Source #

Either is bitraversable. Note: From base >= 4.10.0.0 already present in Bitraversable.

isLeft :: Either a b -> Bool #

Return True if the given value is a Left-value, False otherwise.

Examples

Expand

Basic usage:

>>> isLeft (Left "foo")
True
>>> isLeft (Right 3)
False


Assuming a Left value signifies some sort of error, we can use isLeft to write a very simple error-reporting function that does absolutely nothing in the case of success, and outputs "ERROR" if any error occurred.

This example shows how isLeft might be used to avoid pattern matching when one does not care about the value contained in the constructor:

>>> import Control.Monad ( when )
>>> let report e = when (isLeft e) $putStrLn "ERROR" >>> report (Right 1) >>> report (Left "parse error") ERROR  Since: base-4.7.0.0 isRight :: Either a b -> Bool # Return True if the given value is a Right-value, False otherwise. Examples Expand Basic usage: >>> isRight (Left "foo") False >>> isRight (Right 3) True  Assuming a Left value signifies some sort of error, we can use isRight to write a very simple reporting function that only outputs "SUCCESS" when a computation has succeeded. This example shows how isRight might be used to avoid pattern matching when one does not care about the value contained in the constructor: >>> import Control.Monad ( when ) >>> let report e = when (isRight e)$ putStrLn "SUCCESS"
>>> report (Left "parse error")
>>> report (Right 1)
SUCCESS


Since: base-4.7.0.0

fromLeft :: (b -> a) -> Either a b -> a Source #

Analogue of fromMaybe.

fromRight :: (a -> b) -> Either a b -> b Source #

Analogue of fromMaybe.

fromLeftM :: Monad m => (b -> m a) -> m (Either a b) -> m a Source #

Analogue of fromMaybeM.

fromRightM :: Monad m => (a -> m b) -> m (Either a b) -> m b Source #

Analogue of fromMaybeM.

maybeLeft :: Either a b -> Maybe a Source #

Safe projection from Left.

maybeLeft (Left a) = Just a
maybeLeft Right{}  = Nothing

maybeRight :: Either a b -> Maybe b Source #

Safe projection from Right.

maybeRight (Right b) = Just b
maybeRight Left{}    = Nothing

allLeft :: [Either a b] -> Maybe [a] Source #

Returns Just input_with_tags_stripped if all elements are to the Left, and otherwise Nothing.

allRight :: [Either a b] -> Maybe [b] Source #

Returns Just input_with_tags_stripped if all elements are to the right, and otherwise Nothing.

 allRight xs ==
if all isRight xs then
Just (map ((Right x) -> x) xs)
else
Nothing


groupByEither :: forall a b. [Either a b] -> [Either [a] [b]] Source #

Groups a list into alternating chunks of Left and Right values

maybeToEither :: Maybe a -> Either () a Source #

Convert Maybe to Either ().