Agda.Utils.Maybe

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

Retain object when tag is True.

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

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

Filtering a singleton list.

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

Version of mapMaybe with different argument ordering.

Monadic version of fromMaybe.

caseMaybe with flipped branches.

caseMaybeM with flipped branches.

Lift a maybe to an Alternative.

Monadic version of maybe.

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.

unionWith for collections of size <= 1.

unionsWith for collections of size <= 1.

Unzipping a list of length <= 1.

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

caseMaybeM without the Nothing case.

Pendent to whenJust.

caseMaybeM without the Just case.

The catMaybes function takes a list of Maybes and returns a list of all the Just values.

Examples

Basic usage:

>>> catMaybes [Just 1, Nothing, Just 3][1,3]

When constructing a list of Maybe values, catMaybes can be used to return all of the "success" results (if the list is the result of a map, then mapMaybe would be more appropriate):

>>> import GHC.Internal.Text.Read ( readMaybe )>>> [readMaybe x :: Maybe Int | x <- ["1", "Foo", "3"] ][Just 1,Nothing,Just 3]>>> catMaybes $ [readMaybe x :: Maybe Int | x <- ["1", "Foo", "3"] ][1,3]

The fromJust function extracts the element out of a Just and throws an error if its argument is Nothing.

Examples

Basic usage:

>>> fromJust (Just 1)1

>>> 2 * (fromJust (Just 10))20

>>> 2 * (fromJust Nothing)*** Exception: Maybe.fromJust: Nothing...

WARNING: This function is partial. You can use case-matching instead.

The fromMaybe function takes a default value and a Maybe value. If the Maybe is Nothing, it returns the default value; otherwise, it returns the value contained in the Maybe.

Examples

Basic usage:

>>> fromMaybe "" (Just "Hello, World!")"Hello, World!"

>>> fromMaybe "" Nothing""

Read an integer from a string using readMaybe. If we fail to parse an integer, we want to return 0 by default:

>>> import GHC.Internal.Text.Read ( readMaybe )>>> fromMaybe 0 (readMaybe "5")5>>> fromMaybe 0 (readMaybe "")0

isJust x returns True when x is of the form Just _ and False otherwise.

Examples

Basic usage:

>>> isJust (Just 3)True

>>> isJust (Just ())True

>>> isJust NothingFalse

Only the outer constructor is taken into consideration:

>>> isJust (Just Nothing)True

isNothing x returns True when x is Nothing and False otherwise.

Examples

Basic usage:

>>> isNothing (Just 3)False

>>> isNothing (Just ())False

>>> isNothing NothingTrue

Only the outer constructor is taken into consideration:

>>> isNothing (Just Nothing)False

The listToMaybe function returns Nothing on an empty list or Just a where a is the first element of the list.

Examples

Basic usage:

>>> listToMaybe []Nothing

>>> listToMaybe [9]Just 9

>>> listToMaybe [1,2,3]Just 1

Composing maybeToList with listToMaybe should be the identity on singleton/empty lists:

>>> maybeToList $ listToMaybe [5][5]>>> maybeToList $ listToMaybe [][]

But not on lists with more than one element:

>>> maybeToList $ listToMaybe [1,2,3][1]

The mapMaybe function is a version of map which can throw out elements. In particular, the functional argument returns something of type Maybe b. If this is Nothing, no element is added on to the result list. If it is Just b, then b is included in the result list.

Examples

Using mapMaybe f x is a shortcut for catMaybes $ map f x in most cases:

>>> import GHC.Internal.Text.Read ( readMaybe )>>> let readMaybeInt = readMaybe :: String -> Maybe Int>>> mapMaybe readMaybeInt ["1", "Foo", "3"][1,3]>>> catMaybes $ map readMaybeInt ["1", "Foo", "3"][1,3]

If we map the Just constructor, the entire list should be returned:

>>> mapMaybe Just [1,2,3][1,2,3]

The maybe function takes a default value, a function, and a Maybe value. If the Maybe value is Nothing, the function returns the default value. Otherwise, it applies the function to the value inside the Just and returns the result.

Examples

Basic usage:

>>> maybe False odd (Just 3)True

>>> maybe False odd NothingFalse

Read an integer from a string using readMaybe. If we succeed, return twice the integer; that is, apply (*2) to it. If instead we fail to parse an integer, return 0 by default:

>>> import GHC.Internal.Text.Read ( readMaybe )>>> maybe 0 (*2) (readMaybe "5")10>>> maybe 0 (*2) (readMaybe "")0

Apply show to a Maybe Int. If we have Just n, we want to show the underlying Int n. But if we have Nothing, we return the empty string instead of (for example) "Nothing":

>>> maybe "" show (Just 5)"5">>> maybe "" show Nothing""

The maybeToList function returns an empty list when given Nothing or a singleton list when given Just.

Examples

Basic usage:

>>> maybeToList (Just 7)[7]

>>> maybeToList Nothing[]

One can use maybeToList to avoid pattern matching when combined with a function that (safely) works on lists:

>>> import GHC.Internal.Text.Read ( readMaybe )>>> sum $ maybeToList (readMaybe "3")3>>> sum $ maybeToList (readMaybe "")0

The Maybe type encapsulates an optional value. A value of type Maybe a either contains a value of type a (represented as Just a), or it is empty (represented as Nothing). Using Maybe is a good way to deal with errors or exceptional cases without resorting to drastic measures such as error.

The Maybe type is also a monad. It is a simple kind of error monad, where all errors are represented by Nothing. A richer error monad can be built using the Either type.