Safe Haskell | Trustworthy |
---|---|
Language | Haskell98 |
Data.Unique.Tag
Documentation
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 Tag
s and values of type
can be tested for
equality even when their types are not known to be equal.DSum
(Tag
s)
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.
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.)
Instances
Show (Uniq RealWorld) | There is only one |
GShow (Tag RealWorld) | |
Defined in Unsafe.Unique.Tag Methods gshowsPrec :: forall (a :: k). Int -> Tag RealWorld a -> ShowS | |
Show (Tag RealWorld a) | |
data (a :: k) :~: (b :: k) where #
Instances
GCompare ((:~:) a :: k -> Type) | |
GEq ((:~:) a :: k -> Type) | |
GRead ((:~:) a :: k -> Type) | |
Defined in Data.GADT.Internal Methods greadsPrec :: Int -> GReadS ((:~:) a) | |
GShow ((:~:) a :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> (a :~: a0) -> ShowS | |
TestEquality ((:~:) a :: k -> Type) | |
Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) | |
a ~ b => Bounded (a :~: b) | |
Defined in Data.Type.Equality | |
a ~ b => Enum (a :~: b) | |
Defined in Data.Type.Equality | |
Eq (a :~: b) | |
Ord (a :~: b) | |
Defined in Data.Type.Equality | |
a ~ b => Read (a :~: b) | |
Defined in Data.Type.Equality | |
Show (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
GRead (GOrdering a :: k -> Type) | |
Defined in Data.GADT.Internal Methods greadsPrec :: Int -> GReadS (GOrdering a) | |
GShow (GOrdering a :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> GOrdering a a0 -> ShowS | |
Eq (GOrdering a b) | |
Ord (GOrdering a b) | |
Defined in Data.GADT.Internal | |
Show (GOrdering a b) | |
class GEq f => GCompare (f :: k -> Type) where #
Instances
GCompare (TypeRep :: k -> Type) | |
Defined in Data.GADT.Internal | |
GCompare ((:~:) a :: k -> Type) | |
(GCompare a, GCompare b) => GCompare (Sum a b :: k -> Type) | |
Defined in Data.GADT.Internal | |
(GCompare a, GCompare b) => GCompare (Product a b :: k -> Type) | |
Defined in Data.GADT.Internal | |
GCompare (Tag s :: Type -> Type) Source # | |