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

Eq (Tag s a) Source # 
Instance details

Defined in Unsafe.Unique.Tag

Methods

(==) :: Tag s a -> Tag s a -> Bool

(/=) :: Tag s a -> Tag s a -> Bool

Ord (Tag s a) Source # 
Instance details

Defined in Unsafe.Unique.Tag

Methods

compare :: Tag s a -> Tag s a -> Ordering

(<) :: Tag s a -> Tag s a -> Bool

(<=) :: Tag s a -> Tag s a -> Bool

(>) :: Tag s a -> Tag s a -> Bool

(>=) :: Tag s a -> Tag s a -> Bool

max :: Tag s a -> Tag s a -> Tag s a

min :: Tag s a -> Tag s a -> Tag s a

Show (Tag RealWorld a) Source # 
Instance details

Defined in Unsafe.Unique.Tag

Methods

showsPrec :: Int -> Tag RealWorld a -> ShowS

show :: Tag RealWorld a -> String

showList :: [Tag RealWorld a] -> ShowS

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 #

Instances

Instances details
Show (Uniq RealWorld)

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

Methods

showsPrec :: Int -> Uniq RealWorld -> ShowS

show :: Uniq RealWorld -> String

showList :: [Uniq RealWorld] -> ShowS

GShow (Tag RealWorld) 
Instance details

Defined in Unsafe.Unique.Tag

Methods

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

Show (Tag RealWorld a) 
Instance details

Defined in Unsafe.Unique.Tag

Methods

showsPrec :: Int -> Tag RealWorld a -> ShowS

show :: Tag RealWorld a -> String

showList :: [Tag RealWorld a] -> ShowS

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

Constructors

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

Instances

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

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

Defined in Data.Type.Equality

Methods

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

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

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

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

Defined in Data.Type.Equality

Methods

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

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

toEnum :: Int -> a :~: b

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

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

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

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

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

Eq (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

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

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

Ord (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

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

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

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

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

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

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

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

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

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

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

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

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

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

Eq (GOrdering a b) 
Instance details

Defined in Data.GADT.Internal

Methods

(==) :: GOrdering a b -> GOrdering a b -> Bool

(/=) :: GOrdering a b -> GOrdering a b -> Bool

Ord (GOrdering a b) 
Instance details

Defined in Data.GADT.Internal

Methods

compare :: GOrdering a b -> GOrdering a b -> Ordering

(<) :: GOrdering a b -> GOrdering a b -> Bool

(<=) :: GOrdering a b -> GOrdering a b -> Bool

(>) :: GOrdering a b -> GOrdering a b -> Bool

(>=) :: GOrdering a b -> GOrdering a b -> Bool

max :: GOrdering a b -> GOrdering a b -> GOrdering a b

min :: GOrdering a b -> GOrdering a b -> GOrdering a b

Show (GOrdering a b) 
Instance details

Defined in Data.GADT.Internal

Methods

showsPrec :: Int -> GOrdering a b -> ShowS

show :: GOrdering a b -> String

showList :: [GOrdering a b] -> ShowS

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