dependent-sum-0.6: Dependent sum type

Safe HaskellTrustworthy
LanguageHaskell98

Data.Some

Synopsis

Documentation

data Some tag where Source #

Existential. This is type is useful to hide GADTs' parameters.

>>> data Tag :: * -> * where TagInt :: Tag Int; TagBool :: Tag Bool
>>> instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"

You can either use PatternSynonyms

>>> let x = Some TagInt
>>> x
Some TagInt
>>> case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String
"I"

or you can use functions

>>> let y = mkSome TagBool
>>> y
Some TagBool
>>> withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String
"B"

The implementation of mapSome is safe.

>>> let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool
>>> mapSome f y
Some TagBool

but you can also use:

>>> withSome y (mkSome . f)
Some TagBool

Bundled Patterns

pattern Some :: tag a -> Some tag 
pattern This :: tag a -> Some tag

Deprecated: Use Some instead

Instances
GEq tag => Eq (Some tag) Source # 
Instance details

Defined in Data.Some

Methods

(==) :: Some tag -> Some tag -> Bool #

(/=) :: Some tag -> Some tag -> Bool #

GCompare tag => Ord (Some tag) Source # 
Instance details

Defined in Data.Some

Methods

compare :: Some tag -> Some tag -> Ordering #

(<) :: Some tag -> Some tag -> Bool #

(<=) :: Some tag -> Some tag -> Bool #

(>) :: Some tag -> Some tag -> Bool #

(>=) :: Some tag -> Some tag -> Bool #

max :: Some tag -> Some tag -> Some tag #

min :: Some tag -> Some tag -> Some tag #

GRead f => Read (Some f) Source # 
Instance details

Defined in Data.Some

GShow tag => Show (Some tag) Source # 
Instance details

Defined in Data.Some

Methods

showsPrec :: Int -> Some tag -> ShowS #

show :: Some tag -> String #

showList :: [Some tag] -> ShowS #

mkSome :: tag a -> Some tag Source #

Constructor.

withSome :: Some tag -> (forall a. tag a -> b) -> b Source #

Eliminator.

mapSome :: (forall t. f t -> g t) -> Some f -> Some g Source #