prim-uniq-0.2: Opaque unique identifiers in primitive state monads
Safe HaskellTrustworthy
LanguageHaskell98

Data.Unique.Tag

Synopsis

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

Instances details
GCompare (Tag s :: Type -> Type) Source # 
Instance details

Defined in Unsafe.Unique.Tag

Methods

gcompare :: forall (a :: k) (b :: k). Tag s a -> Tag s b -> GOrdering a b #

GEq (Tag s :: Type -> Type) Source # 
Instance details

Defined in Unsafe.Unique.Tag

Methods

geq :: forall (a :: k) (b :: k). Tag s a -> Tag s b -> Maybe (a :~: b) #

GShow (Tag RealWorld) Source # 
Instance details

Defined in Unsafe.Unique.Tag

Methods

gshowsPrec :: forall (a :: k). Int -> Tag RealWorld a -> ShowS

Show (Tag RealWorld a) Source # 
Instance details

Defined in Unsafe.Unique.Tag

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 #

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

Instances details
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 Uniqs.

Instance details

Defined in Unsafe.Unique.Prim

GShow (Tag RealWorld) 
Instance details

Defined in Unsafe.Unique.Tag

Methods

gshowsPrec :: forall (a :: k). Int -> Tag RealWorld a -> ShowS

Show (Tag RealWorld a) Source # 
Instance details

Defined in Unsafe.Unique.Tag

data (a :: k) :~: (b :: k) where infix 4 Source #

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

Refl :: forall {k} (a :: k). a :~: a 

Instances

Instances details
TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #

GCompare ((:~:) a :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> GOrdering a0 b #

GEq ((:~:) a :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #

GRead ((:~:) a :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

greadsPrec :: Int -> GReadS ((:~:) a)

GShow ((:~:) a :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec :: forall (a0 :: k0). Int -> (a :~: a0) -> ShowS

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

minBound :: a :~: b Source #

maxBound :: a :~: b Source #

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b Source #

pred :: (a :~: b) -> a :~: b Source #

toEnum :: Int -> a :~: b Source #

fromEnum :: (a :~: b) -> Int Source #

enumFrom :: (a :~: b) -> [a :~: b] Source #

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] Source #

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] Source #

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] Source #

a ~ b => Read (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Show (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS Source #

show :: (a :~: b) -> String Source #

showList :: [a :~: b] -> ShowS Source #

Eq (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool Source #

(/=) :: (a :~: b) -> (a :~: b) -> Bool Source #

Ord (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering Source #

(<) :: (a :~: b) -> (a :~: b) -> Bool Source #

(<=) :: (a :~: b) -> (a :~: b) -> Bool Source #

(>) :: (a :~: b) -> (a :~: b) -> Bool Source #

(>=) :: (a :~: b) -> (a :~: b) -> Bool Source #

max :: (a :~: b) -> (a :~: b) -> a :~: b Source #

min :: (a :~: b) -> (a :~: b) -> a :~: b Source #

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

Methods

geq :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #

Instances

Instances details
GEq (TypeRep :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a :: k0) (b :: k0). TypeRep a -> TypeRep b -> Maybe (a :~: b) #

GEq ((:~:) a :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #

(GEq a, GEq b) => GEq (Product a b :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a0 :: k0) (b0 :: k0). Product a b a0 -> Product a b b0 -> Maybe (a0 :~: b0) #

(GEq a, GEq b) => GEq (Sum a b :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a0 :: k0) (b0 :: k0). Sum a b a0 -> Sum a b b0 -> Maybe (a0 :~: b0) #

GEq (Tag s :: Type -> Type) Source # 
Instance details

Defined in Unsafe.Unique.Tag

Methods

geq :: forall (a :: k) (b :: k). Tag s a -> Tag s b -> Maybe (a :~: b) #

data GOrdering (a :: k) (b :: k) where #

Constructors

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

Instances

Instances details
GRead (GOrdering a :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

greadsPrec :: Int -> GReadS (GOrdering a)

GShow (GOrdering a :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec :: forall (a0 :: k0). Int -> GOrdering a a0 -> ShowS

Show (GOrdering a b) 
Instance details

Defined in Data.GADT.Internal

Eq (GOrdering a b) 
Instance details

Defined in Data.GADT.Internal

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

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 #

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

Methods

gcompare :: forall (a :: k) (b :: k). f a -> f b -> GOrdering a b #

Instances

Instances details
GCompare (TypeRep :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a :: k0) (b :: k0). TypeRep a -> TypeRep b -> GOrdering a b #

GCompare ((:~:) a :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> GOrdering a0 b #

(GCompare a, GCompare b) => GCompare (Product a b :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a0 :: k0) (b0 :: k0). Product a b a0 -> Product a b b0 -> GOrdering a0 b0 #

(GCompare a, GCompare b) => GCompare (Sum a b :: k -> Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a0 :: k0) (b0 :: k0). Sum a b a0 -> Sum a b b0 -> GOrdering a0 b0 #

GCompare (Tag s :: Type -> Type) Source # 
Instance details

Defined in Unsafe.Unique.Tag

Methods

gcompare :: forall (a :: k) (b :: k). Tag s a -> Tag s b -> GOrdering a b #