Safe Haskell	Safe
Language	Haskell2010

Data.Some.Church

Synopsis

newtype Some (tag :: k -> Type) = S {
- withSome :: forall r. (forall (a :: k). tag a -> r) -> r
}
mkSome :: forall {k} tag (a :: k). tag a -> Some tag
mapSome :: (forall (x :: k). f x -> g x) -> Some f -> Some g
withSomeM :: forall {k} m tag r. Monad m => m (Some tag) -> (forall (a :: k). tag a -> m r) -> m r
foldSome :: (forall (a :: k). tag a -> b) -> Some tag -> b
traverseSome :: forall {k} m f g. Functor m => (forall (a :: k). f a -> m (g a)) -> Some f -> m (Some g)

Documentation

newtype Some (tag :: k -> Type) 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"
>>> classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> []
>>> instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <-  lex s, r <- classify con ]

With Church-encoding youcan only use a functions:

>>> let y = mkSome TagBool
>>> y
mkSome TagBool

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

or explicitly work with S

>>> let x = S $ \f -> f TagInt
>>> x
mkSome TagInt

>>> case x of S f -> f $ \x' -> case x' of { TagInt -> "I"; TagBool -> "B" } :: String
"I"

The implementation of mapSome is safe.

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

but you can also use:

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

>>> read "Some TagBool" :: Some Tag
mkSome TagBool

>>> read "mkSome TagInt" :: Some Tag
mkSome TagInt

Constructors

S
Fields withSome :: forall r. (forall (a :: k). tag a -> r) -> r Eliminator.

Instances

Instances details

Applicative m => Monoid (Some m) Source #
Instance details Defined in Data.GADT.Internal Methods mempty :: Some m # mappend :: Some m -> Some m -> Some m # mconcat :: [Some m] -> Some m #
Applicative m => Semigroup (Some m) Source #
Instance details Defined in Data.GADT.Internal Methods (<>) :: Some m -> Some m -> Some m # sconcat :: NonEmpty (Some m) -> Some m # stimes :: Integral b => b -> Some m -> Some m #
GRead f => Read (Some f) Source #
Instance details Defined in Data.GADT.Internal Methods readsPrec :: Int -> ReadS (Some f) # readList :: ReadS [Some f] # readPrec :: ReadPrec (Some f) # readListPrec :: ReadPrec [Some f] #
GShow tag => Show (Some tag) Source #
Instance details Defined in Data.GADT.Internal Methods showsPrec :: Int -> Some tag -> ShowS # show :: Some tag -> String # showList :: [Some tag] -> ShowS #
GEq tag => Eq (Some tag) Source #
Instance details Defined in Data.GADT.Internal Methods (==) :: Some tag -> Some tag -> Bool # (/=) :: Some tag -> Some tag -> Bool #
GCompare tag => Ord (Some tag) Source #
Instance details Defined in Data.GADT.Internal 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 #

mkSome :: forall {k} tag (a :: k). tag a -> Some tag Source #

Constructor.

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

Map over argument.

withSomeM :: forall {k} m tag r. Monad m => m (Some tag) -> (forall (a :: k). tag a -> m r) -> m r Source #

Monadic withSome.

Since: 1.0.1

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

flip withSome

traverseSome :: forall {k} m f g. Functor m => (forall (a :: k). f a -> m (g a)) -> Some f -> m (Some g) Source #

Traverse over argument.