ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.Maybe.Strict

A strict version of the Maybe type.

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

1 type
1 class
21 values

PackageAgda-2.8.0.2
Exports23
LanguageHaskell2010
LicenceMIT
SourceStrict.hs

valuecatMaybes :: [Maybe a] -> [a]

Analogous to L.catMaybes in Data.Maybe.

valuefromJust :: Maybe a -> a

Extracts the element out of a Just and throws an error if the argument is Nothing.

valuefromMaybe :: a -> Maybe a -> a

Given a default value and a Maybe, yield the default value if the Maybe argument is Nothing and extract the value out of the Just otherwise.

valueisJust :: Maybe a -> Bool

Yields True iff the argument is of the form Just _.

valueisNothing :: Maybe a -> Bool

Yields True iff the argument is Nothing.

valuelistToMaybe :: [a] -> Maybe a

Analogous to L.listToMaybe in Data.Maybe.

valuemapMaybe :: (a -> Maybe b) -> [a] -> [b]

Analogous to L.mapMaybe in Data.Maybe.

valuemaybe :: b -> (a -> b) -> Maybe a -> b

Given a default value, a function and a Maybe value, yields the default value if the Maybe value is Nothing and applies the function to the value stored in the Just otherwise.

valuemaybeToList :: Maybe a -> [a]

Analogous to L.maybeToList in Data.Maybe.

datadata Maybe a

The type of strict optional values.

Constructors

Nothing
Just !a

Instances66Functor, Applicative, Foldable, Traversable, Eq1, Ord1, …

Functor MaybeDefined in strict-0.5.1 · Data.Strict.Maybe
Applicative MaybeDefined in Agda-2.8.0.2 · Agda.Utils.Maybe.Strict · orphan
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.
Foldable MaybeDefined in strict-0.5.1 · Data.Strict.Maybe
Traversable MaybeDefined in strict-0.5.1 · Data.Strict.Maybe
Eq1 MaybeDefined in strict-0.5.1 · Data.Strict.Maybe
Ord1 MaybeDefined in strict-0.5.1 · Data.Strict.Maybe
Read1 MaybeDefined in strict-0.5.1 · Data.Strict.Maybe
Show1 MaybeDefined in strict-0.5.1 · Data.Strict.Maybe
NFData IntervalDefined in Agda-2.8.0.2 · Agda.Syntax.Position
NFData PositionDefined in Agda-2.8.0.2 · Agda.Syntax.Position
NFData1 MaybeDefined in strict-0.5.1 · Data.Strict.Maybe
Hashable1 MaybeDefined in strict-0.5.1 · Data.Strict.Maybe
FromJSON1 MaybeDefined in aeson-2.3.2.0 · Data.Aeson.Types.FromJSON
ToJSON RangeDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
ToJSON1 MaybeDefined in aeson-2.3.2.0 · Data.Aeson.Types.ToJSON
Pretty TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleName · orphan
FreshName RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
Sized TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.TopLevelModuleName · orphan
HasRange IntervalDefined in Agda-2.8.0.2 · Agda.Syntax.Position
HasRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
Subst RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
PrettyTCM RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
BeginningOfFile RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
beginningOfFile r is an empty range (a single, empty interval) at the beginning of r's starting position's file. If there is no such position, then an empty range is returned.
BeginningOfFile SrcFileDefined in Agda-2.8.0.2 · Agda.Syntax.Position
EncodeTCM RangeDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
KillRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange RangeDefined in Agda-2.8.0.2 · Agda.Syntax.Position
EmbPrj RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Ranges are always deserialised as noRange.
EmbPrj TopLevelModuleNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Generic1 MaybeDefined in strict-0.5.1 · Data.Strict.Maybe
LensClosure MetaInfo RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensClosure MetaVariable RangeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
Eq a => Eq (Maybe a)Defined in strict-0.5.1 · Data.Strict.Maybe
Data a => Data (Maybe a)Defined in strict-0.5.1 · Data.Strict.Maybe
Ord a => Ord (Maybe a)Defined in strict-0.5.1 · Data.Strict.Maybe
Read a => Read (Maybe a)Defined in strict-0.5.1 · Data.Strict.Maybe
Show a => Show (Maybe a)Defined in strict-0.5.1 · Data.Strict.Maybe
Generic (Maybe a)Defined in strict-0.5.1 · Data.Strict.Maybe
Semigroup a => Semigroup (Maybe a)Defined in strict-0.5.1 · Data.Strict.Maybe
Semigroup a => Monoid (Maybe a)Defined in strict-0.5.1 · Data.Strict.Maybe
NFData a => NFData (Maybe a)Defined in strict-0.5.1 · Data.Strict.Maybe
Binary a => Binary (Maybe a)Defined in strict-0.5.1 · Data.Strict.Maybe
Hashable a => Hashable (Maybe a)Defined in strict-0.5.1 · Data.Strict.Maybe
FromJSON a => FromJSON (Maybe a)Defined in aeson-2.3.2.0 · Data.Aeson.Types.FromJSON
ToJSON a => ToJSON (Maybe a)Defined in aeson-2.3.2.0 · Data.Aeson.Types.ToJSON
Pretty a => Pretty (Interval' (Maybe a))Defined in Agda-2.8.0.2 · Agda.Syntax.Common.Pretty
Pretty a => Pretty (Position' (Maybe a))Defined in Agda-2.8.0.2 · Agda.Syntax.Common.Pretty
Pretty a => Pretty (Range' (Maybe a))Defined in Agda-2.8.0.2 · Agda.Syntax.Common.Pretty
Null (Maybe a)Defined in Agda-2.8.0.2 · Agda.Utils.Maybe.Strict · orphan
HasRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
Simplify t => Simplify (Maybe t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Instantiate t => Instantiate (Maybe t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Normalise t => Normalise (Maybe t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Apply t => Apply (Maybe t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
KillRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
KillRange a => KillRange (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
SetRange (TopLevelModuleName' Range)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
NamesIn a => NamesIn (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Names
InstantiateFull t => InstantiateFull (Maybe t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
EmbPrj a => EmbPrj (Maybe a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Strict (Maybe a) (Maybe a)Defined in strict-0.5.1 · Data.Strict.Classes
FreshName (Range, String)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
type Rep (Maybe a) = D1 ('MetaData "Maybe" "Data.Strict.Maybe" "strict-0.5.1-62OsYISSgdbBs2bAjJkvlf" 'False) (C1 ('MetaCons "Nothing" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Just" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a)))Defined in strict-0.5.1 · Data.Strict.Maybe
type Rep1 Maybe = D1 ('MetaData "Maybe" "Data.Strict.Maybe" "strict-0.5.1-62OsYISSgdbBs2bAjJkvlf" 'False) (C1 ('MetaCons "Nothing" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Just" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) Par1))Defined in strict-0.5.1 · Data.Strict.Maybe
type SubstArg Range = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan

classclass Strict lazy strict | lazy -> strict, strict -> lazy where

Ad hoc conversion between "strict" and "lazy" versions of a structure.

Unfortunately all externally defined instances are doomed to be orphans: https://gitlab.haskell.org/ghc/ghc/-/issues/11999 See also https://qfpl.io/posts/orphans-and-fundeps/index.html for

Methods

toStrict :: lazy -> strict
toLazy :: strict -> lazy

Instances10Strict, …

Strict ByteString ByteStringDefined in strict-0.5.1 · Data.Strict.Classes
Strict Text TextDefined in strict-0.5.1 · Data.Strict.Classes
Strict (Maybe a) (Maybe a)Defined in strict-0.5.1 · Data.Strict.Classes
Strict (ST s a) (ST s a)Defined in strict-0.5.1 · Data.Strict.Classes
Strict (Either a b) (Either a b)Defined in strict-0.5.1 · Data.Strict.Classes
Strict (These a b) (These a b)Defined in strict-0.5.1 · Data.Strict.Classes
Strict (a, b) (Pair a b)Defined in strict-0.5.1 · Data.Strict.Classes
Strict (StateT s m a) (StateT s m a)Defined in strict-0.5.1 · Data.Strict.Classes
Strict (WriterT w m a) (WriterT w m a)Defined in strict-0.5.1 · Data.Strict.Classes
Strict (RWST r w s m a) (RWST r w s m a)Defined in strict-0.5.1 · Data.Strict.Classes

valuecaseMaybe :: Maybe a -> b -> (a -> b) -> b

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

valuecaseMaybeM :: Monad m => m (Maybe a) -> m b -> (a -> m b) -> m b

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

valuefilterMaybe :: (a -> Bool) -> a -> Maybe a

Filtering a singleton list.

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

valueforMaybe :: [a] -> (a -> Maybe b) -> [b]

Version of mapMaybe with different argument ordering.

valuefromMaybeM :: Monad m => m a -> m (Maybe a) -> m a

Monadic version of fromMaybe.

valueifJustM :: Monad m => m (Maybe a) -> (a -> m b) -> m b -> m b

caseMaybeM with flipped branches.

valuelensMaybeLazy

:: Functor f
=> Maybe a -> f (Maybe a)
-> Maybe a
-> f (Maybe a)

valuemaybeM :: Monad m => m b -> (a -> m b) -> m (Maybe a) -> m b

Monadic version of maybe.

valueunionMaybeWith :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a

unionWith for collections of size <= 1.

valueunzipMaybe :: Maybe (a, b) -> (Maybe a, Maybe b)

Unzipping a list of length <= 1.

valuewhenJust :: Monad m => Maybe a -> (a -> m ()) -> m ()

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

valuewhenJustM :: Monad m => m (Maybe a) -> (a -> m ()) -> m ()

caseMaybeM without the Nothing case.

Orphan instances

2 instances

Applicative Maybe
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.
Null (Maybe a)