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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Either

Description

Utilities for the `Either` type.

Synopsis

- whileLeft :: Monad m => (a -> Either b c) -> (a -> b -> m a) -> (a -> c -> m d) -> a -> m d
- caseEitherM :: Monad m => m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
- mapLeft :: (a -> c) -> Either a b -> Either c b
- mapRight :: (b -> d) -> Either a b -> Either a d
- traverseEither :: Functor f => (a -> f c) -> (b -> f d) -> Either a b -> f (Either c d)
- isLeft :: Either a b -> Bool
- isRight :: Either a b -> Bool
- fromLeft :: (b -> a) -> Either a b -> a
- fromRight :: (a -> b) -> Either a b -> b
- fromLeftM :: Monad m => (b -> m a) -> m (Either a b) -> m a
- fromRightM :: Monad m => (a -> m b) -> m (Either a b) -> m b
- maybeLeft :: Either a b -> Maybe a
- maybeRight :: Either a b -> Maybe b
- allLeft :: [Either a b] -> Maybe [a]
- allRight :: [Either a b] -> Maybe [b]
- groupByEither :: [Either a b] -> [Either (List1 a) (List1 b)]
- maybeToEither :: e -> Maybe a -> Either e a
- swapEither :: Either a b -> Either b a

# 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 Source #

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 Source #

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 :: [Either a b] -> [Either (List1 a) (List1 b)] Source #

Groups a list into alternating chunks of `Left` and `Right` values

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

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

swapEither :: Either a b -> Either b a Source #

Swap tags `Left` and `Right`.