Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

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 :: forall a b. [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 #

isRight :: Either a b -> Bool #

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 (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.