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

Agda.Utils.Maybe

Description

Extend Maybe by common operations for the Maybe type.

Note: since this module is usually imported unqualified, we do not use short names, but all names contain Maybe, Just, or 'Nothing.

Synopsis
  • boolToMaybe :: Bool -> a -> Maybe a
  • caseMaybeM :: Monad m => m (Maybe a) -> m b -> (a -> m b) -> m b
  • whenNothing :: Monoid m => Maybe a -> m -> m
  • fromMaybeM :: Monad m => m a -> m (Maybe a) -> m a
  • forMaybe :: [a] -> (a -> Maybe b) -> [b]
  • filterMaybe :: (a -> Bool) -> a -> Maybe a
  • allJustM :: Monad m => [m (Maybe a)] -> m (Maybe [a])
  • whenNothingM :: Monad m => m (Maybe a) -> m () -> m ()
  • whenJust :: Monad m => Maybe a -> (a -> m ()) -> m ()
  • unionMaybeWith :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
  • unionsMaybeWith :: (a -> a -> a) -> [Maybe a] -> Maybe a
  • unzipMaybe :: Maybe (a, b) -> (Maybe a, Maybe b)
  • caseMaybe :: Maybe a -> b -> (a -> b) -> b
  • ifJust :: Maybe a -> (a -> b) -> b -> b
  • maybeM :: Monad m => m b -> (a -> m b) -> m (Maybe a) -> m b
  • ifJustM :: Monad m => m (Maybe a) -> (a -> m b) -> m b -> m b
  • whenJustM :: Monad m => m (Maybe a) -> (a -> m ()) -> m ()
  • liftMaybe :: Alternative f => Maybe a -> f a
  • spanMaybe :: (a -> Maybe b) -> [a] -> ([b], [a])

Documentation

boolToMaybe :: Bool -> a -> Maybe a Source #

Retain object when tag is True.

caseMaybeM :: Monad m => m (Maybe a) -> m b -> (a -> m b) -> m b Source #

Monadic version of caseMaybe. That is, maybeM with a different argument ordering.

whenNothing :: Monoid m => Maybe a -> m -> m Source #

caseMaybe without the Just case.

fromMaybeM :: Monad m => m a -> m (Maybe a) -> m a Source #

Monadic version of fromMaybe.

forMaybe :: [a] -> (a -> Maybe b) -> [b] Source #

Version of mapMaybe with different argument ordering.

filterMaybe :: (a -> Bool) -> a -> Maybe a Source #

Filtering a singleton list.

filterMaybe p a = listToMaybe (filter p [a])

allJustM :: Monad m => [m (Maybe a)] -> m (Maybe [a]) Source #

Lazy version of allJust . sequence. (allJust = mapM for the Maybe monad.) Only executes monadic effect while isJust.

whenNothingM :: Monad m => m (Maybe a) -> m () -> m () Source #

caseMaybeM without the Just case.

whenJust :: Monad m => Maybe a -> (a -> m ()) -> m () Source #

A more telling name for forM_ for the Maybe collection type. Or: caseMaybe without the Nothing case.

unionMaybeWith :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a Source #

unionWith for collections of size <= 1.

unionsMaybeWith :: (a -> a -> a) -> [Maybe a] -> Maybe a Source #

unionsWith for collections of size <= 1.

unzipMaybe :: Maybe (a, b) -> (Maybe a, Maybe b) Source #

Unzipping a list of length <= 1.

caseMaybe :: Maybe a -> b -> (a -> b) -> b Source #

Version of maybe with different argument ordering. Often, we want to case on a Maybe, do something interesting in the Just case, but only a default action in the Nothing case. Then, the argument ordering of caseMaybe is preferable.

caseMaybe m d f = flip (maybe d) m f

ifJust :: Maybe a -> (a -> b) -> b -> b Source #

caseMaybe with flipped branches.

maybeM :: Monad m => m b -> (a -> m b) -> m (Maybe a) -> m b Source #

Monadic version of maybe.

ifJustM :: Monad m => m (Maybe a) -> (a -> m b) -> m b -> m b Source #

caseMaybeM with flipped branches.

whenJustM :: Monad m => m (Maybe a) -> (a -> m ()) -> m () Source #

caseMaybeM without the Nothing case.

liftMaybe :: Alternative f => Maybe a -> f a Source #

Lift a maybe to an Alternative.

spanMaybe :: (a -> Maybe b) -> [a] -> ([b], [a]) Source #

Like span, takes the prefix of a list satisfying a predicate. Returns the run of Justs until the first Nothing, and the tail of the list.