Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




A strict version of the Maybe type.

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

Copyright : (c) 2006-2007 Roman Leshchinskiy (c) 2013 Simon Meier License : BSD-style (see the file LICENSE)

Copyright : (c) 2014 Andreas Abel



toStrict :: Maybe a -> Maybe a Source

toLazy :: Maybe a -> Maybe a Source

listToMaybe :: [a] -> Maybe a Source

Analogous to listToMaybe in Data.Maybe.

maybeToList :: Maybe a -> [a] Source

Analogous to maybeToList in Data.Maybe.

catMaybes :: [Maybe a] -> [a] Source

Analogous to catMaybes in Data.Maybe.

mapMaybe :: (a -> Maybe b) -> [a] -> [b] Source

Analogous to mapMaybe in Data.Maybe.

Collection operations.

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.

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

Filtering a singleton list.

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

Conditionals and loops.

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

Version of mapMaybe with different argument ordering.

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

Monads and Maybe.

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

Monadic version of maybe.

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

Monadic version of fromMaybe.

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.

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

caseMaybeM with flipped branches.

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.

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

caseMaybeM without the Nothing case.