some-1.0.1: Existential type: Some

Safe Haskell | Safe
Language | Haskell2010

Data.Some.Church

Synopsis

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

# Documentation

newtype Some tag 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. tag a -> r) -> r

  Eliminator.

#### Instances

Instances details

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
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
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
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

mkSome :: tag a -> Some tag Source #

Constructor.

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

Map over argument.

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

Monadic `withSome`.

Since: 1.0.1

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

    flip withSome

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

Traverse over argument.