Safe Haskell	Trustworthy
Language	Haskell98

Data.Unique.Tag

Synopsis

data Tag s a
newTag :: PrimMonad m => m (Tag (PrimState m) a)
data RealWorld :: Type
type (:=) = ((:~:) :: k -> k -> Type)
class GEq (f :: k -> Type) where
- geq :: f a -> f b -> Maybe (a := b)
data GOrdering (a :: k) (b :: k) :: forall k. k -> k -> Type where
- GLT :: forall k (a :: k) (b :: k). GOrdering a b
- GEQ :: forall k (a :: k) (b :: k). GOrdering a a
- GGT :: forall k (a :: k) (b :: k). GOrdering a b
class GEq f => GCompare (f :: k -> Type) where
- gcompare :: f a -> f b -> GOrdering a b

Documentation

data Tag s a Source #

The Tag type is like an ad-hoc GADT allowing runtime creation of new constructors. Specifically, it is like a GADT "enumeration" with one phantom type.

A Tag constructor can be generated in any primitive monad (but only tags from the same one can be compared). Every tag is equal to itself and to no other. The GOrdering class allows rediscovery of a tag's phantom type, so that Tags and values of type DSum (Tag s) can be tested for equality even when their types are not known to be equal.

Tag uses a Uniq as a witness of type equality, which is sound as long as the Uniq is truly unique and only one Tag is ever constructed from any given Uniq. The type of newTag enforces these conditions. veryUnsafeMkTag provides a way for adventurous (or malicious!) users to assert that they know better than the type system.

Instances

GEq (Tag s :: Type -> Type) Source #
Instance details Defined in Unsafe.Unique.Tag Methods geq :: Tag s a -> Tag s b -> Maybe (a := b) Source #
GCompare (Tag s :: Type -> Type) Source #
Instance details Defined in Unsafe.Unique.Tag Methods gcompare :: Tag s a -> Tag s b -> GOrdering a b Source #
GShow (Tag RealWorld) Source #
Instance details Defined in Unsafe.Unique.Tag Methods gshowsPrec :: Int -> Tag RealWorld a -> ShowS Source #
Eq (Tag s a) Source #
Instance details Defined in Unsafe.Unique.Tag Methods (==) :: Tag s a -> Tag s a -> Bool Source # (/=) :: Tag s a -> Tag s a -> Bool Source #
Ord (Tag s a) Source #
Instance details Defined in Unsafe.Unique.Tag Methods compare :: Tag s a -> Tag s a -> Ordering Source # (<) :: Tag s a -> Tag s a -> Bool Source # (<=) :: Tag s a -> Tag s a -> Bool Source # (>) :: Tag s a -> Tag s a -> Bool Source # (>=) :: Tag s a -> Tag s a -> Bool Source # max :: Tag s a -> Tag s a -> Tag s a Source # min :: Tag s a -> Tag s a -> Tag s a Source #
Show (Tag RealWorld a) Source #
Instance details Defined in Unsafe.Unique.Tag Methods showsPrec :: Int -> Tag RealWorld a -> ShowS Source # show :: Tag RealWorld a -> String Source # showList :: [Tag RealWorld a] -> ShowS Source #

newTag :: PrimMonad m => m (Tag (PrimState m) a) Source #

Create a new tag witnessing a type a. The GEq or GOrdering instance can be used to discover type equality of two occurrences of the same tag.

(I'm not sure whether the recovery is sound if a is instantiated as a polymorphic type, so I'd advise caution if you intend to try it. I suspect it is, but I have not thought through it very deeply and certainly have not proved it.)

data RealWorld :: Type Source #

RealWorld is deeply magical. It is primitive, but it is not unlifted (hence ptrArg). We never manipulate values of type RealWorld; it's only used in the type system, to parameterise State#.

Instances

Show (Uniq RealWorld) Source #	There is only one `RealWorld`, so this instance is sound (unlike the general `unsafeShowsPrecUniq`). Note that there is no particular relationship between `Uniq` values (or the strings `show` turns them into) created in different executions of a program. The value they render to should be considered completely arbitrary, and the Show instance only even exists for convenience when testing code that uses `Uniq`s.
Instance details Defined in Unsafe.Unique.Prim Methods showsPrec :: Int -> Uniq RealWorld -> ShowS Source # show :: Uniq RealWorld -> String Source # showList :: [Uniq RealWorld] -> ShowS Source #
GShow (Tag RealWorld) Source #
Instance details Defined in Unsafe.Unique.Tag Methods gshowsPrec :: Int -> Tag RealWorld a -> ShowS Source #
Show (Tag RealWorld a) Source #
Instance details Defined in Unsafe.Unique.Tag Methods showsPrec :: Int -> Tag RealWorld a -> ShowS Source # show :: Tag RealWorld a -> String Source # showList :: [Tag RealWorld a] -> ShowS Source #

type (:=) = ((:~:) :: k -> k -> Type) Source #

Backwards compatibility alias; as of GHC 7.8, this is the same as `(:~:)`.

class GEq (f :: k -> Type) where Source #

A class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them.

Methods

geq :: f a -> f b -> Maybe (a := b) Source #

Produce a witness of type-equality, if one exists.

A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:

extract :: GEq tag => tag a -> DSum tag -> Maybe a
extract t1 (t2 :=> x) = do
    Refl <- geq t1 t2
    return x

Or in a list comprehension:

extractMany :: GEq tag => tag a -> [DSum tag] -> [a]
extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]

(Making use of the DSum type from Data.Dependent.Sum in both examples)

Instances

GEq ((:=) a :: k -> Type)
Instance details Defined in Data.GADT.Compare Methods geq :: (a := a0) -> (a := b) -> Maybe (a0 := b) Source #
GEq (Tag s :: Type -> Type) Source #
Instance details Defined in Unsafe.Unique.Tag Methods geq :: Tag s a -> Tag s b -> Maybe (a := b) Source #

data GOrdering (a :: k) (b :: k) :: forall k. k -> k -> Type where Source #

A type for the result of comparing GADT constructors; the type parameters of the GADT values being compared are included so that in the case where they are equal their parameter types can be unified.

Constructors

GLT :: forall k (a :: k) (b :: k). GOrdering a b
GEQ :: forall k (a :: k) (b :: k). GOrdering a a
GGT :: forall k (a :: k) (b :: k). GOrdering a b

Instances

GShow (GOrdering a :: k -> Type)
Instance details Defined in Data.GADT.Compare Methods gshowsPrec :: Int -> GOrdering a a0 -> ShowS Source #
GRead (GOrdering a :: k -> Type)
Instance details Defined in Data.GADT.Compare Methods greadsPrec :: Int -> GReadS (GOrdering a) Source #
Eq (GOrdering a b)
Instance details Defined in Data.GADT.Compare Methods (==) :: GOrdering a b -> GOrdering a b -> Bool Source # (/=) :: GOrdering a b -> GOrdering a b -> Bool Source #
Ord (GOrdering a b)
Instance details Defined in Data.GADT.Compare Methods compare :: GOrdering a b -> GOrdering a b -> Ordering Source # (<) :: GOrdering a b -> GOrdering a b -> Bool Source # (<=) :: GOrdering a b -> GOrdering a b -> Bool Source # (>) :: GOrdering a b -> GOrdering a b -> Bool Source # (>=) :: GOrdering a b -> GOrdering a b -> Bool Source # max :: GOrdering a b -> GOrdering a b -> GOrdering a b Source # min :: GOrdering a b -> GOrdering a b -> GOrdering a b Source #
Show (GOrdering a b)
Instance details Defined in Data.GADT.Compare Methods showsPrec :: Int -> GOrdering a b -> ShowS Source # show :: GOrdering a b -> String Source # showList :: [GOrdering a b] -> ShowS Source #

class GEq f => GCompare (f :: k -> Type) where Source #

Type class for comparable GADT-like structures. When 2 things are equal, must return a witness that their parameter types are equal as well (GEQ).

Methods

gcompare :: f a -> f b -> GOrdering a b Source #

Instances

GCompare ((:=) a :: k -> Type)
Instance details Defined in Data.GADT.Compare Methods gcompare :: (a := a0) -> (a := b) -> GOrdering a0 b Source #
GCompare (Tag s :: Type -> Type) Source #
Instance details Defined in Unsafe.Unique.Tag Methods gcompare :: Tag s a -> Tag s b -> GOrdering a b Source #