Agda.Utils.Either

Utilities for the Either type.

Documentation

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

Loop while we have an exception.

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

Monadic version of either with a different argument ordering.

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

'Either _ b' is a functor.

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

'Either a' is a functor.

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

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

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

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

Analogue of fromMaybe.

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

Analogue of fromMaybe.

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

Analogue of fromMaybeM.

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

Analogue of fromMaybeM.

maybeLeft :: Either a b -> Maybe a

Safe projection from Left.

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

maybeRight :: Either a b -> Maybe b

Safe projection from Right.

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

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

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

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

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 (List1 a) (List1 b)]

Groups a list into alternating chunks of Left and Right values

maybeToEither :: e -> Maybe a -> Either e a

Convert Maybe to Either e, given an error e for the Nothing case.

swapEither :: Either a b -> Either b a

Swap tags Left and Right.