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

Safe Haskell | None
Language | Haskell2010

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 :: Monad m => Maybe a -> m () -> m ()
- whenJust :: Monad m => Maybe a -> (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 ()
- 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])
- module Data.Maybe

# 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 :: Monad m => Maybe a -> m () -> m () Source #

Pendent to `whenJust`.

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.

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.

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 `Just`s until the first `Nothing`, and the tail of the list.

module Data.Maybe