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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Maybe.Strict

Contents

- Orphan instances

Description

A strict version of the `Maybe` type.

Import qualified, as in `import qualified Agda.Utils.Maybe.Strict as Strict`

Synopsis

- module Data.Strict.Maybe
- module Data.Strict.Classes
- caseMaybeM :: Monad m => m (Maybe a) -> m b -> (a -> m b) -> m b
- 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
- unionMaybeWith :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
- unzipMaybe :: Maybe (a, b) -> (Maybe a, Maybe b)
- caseMaybe :: Maybe a -> b -> (a -> 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 ()
- lensMaybeLazy :: forall a f. Functor f => (Maybe a -> f (Maybe a)) -> Maybe a -> f (Maybe a)

# Documentation

module Data.Strict.Maybe

module Data.Strict.Classes

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.

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])

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

`unionWith` 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 err f = flip (maybe err) m f

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.

lensMaybeLazy :: forall a f. Functor f => (Maybe a -> f (Maybe a)) -> Maybe a -> f (Maybe a) Source #

# Orphan instances

Applicative Maybe Source # | Note that strict Maybe is an `Applicative` only modulo strictness. The laws only hold in the strict semantics. Eg. `pure f * pure _|_ = _|_`, but according to the laws for `Applicative` it should be `pure (f _|_)`. We ignore this issue here, it applies also to `Foldable` and `Traversable`.
Instance details Methods pure :: a -> Maybe a Source # (<*>) :: Maybe (a -> b) -> Maybe a -> Maybe b Source # liftA2 :: (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c Source # (*>) :: Maybe a -> Maybe b -> Maybe b Source # (<*) :: Maybe a -> Maybe b -> Maybe a Source #
Null (Maybe a) Source # |
Instance details Methods empty :: Maybe a Source # null :: Maybe a -> Bool Source #