| 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 Tags and values of type 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.
Instances
| GCompare (Tag s :: Type -> Type) Source # | |
| GEq (Tag s :: Type -> Type) Source # | |
| GShow (Tag RealWorld) Source # | |
Defined in Unsafe.Unique.Tag Methods gshowsPrec :: forall (a :: k). Int -> Tag RealWorld a -> ShowS | |
| Show (Tag RealWorld a) Source # | |
| Eq (Tag s a) Source # | |
| Ord (Tag s a) Source # | |
Defined in Unsafe.Unique.Tag | |
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.)
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
| GShow (Tag RealWorld) | |
Defined in Unsafe.Unique.Tag Methods gshowsPrec :: forall (a :: k). Int -> Tag RealWorld a -> ShowS | |
| Show (Uniq RealWorld) Source # | There is only one |
| Show (Tag RealWorld a) Source # | |
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
Instances
| TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
| 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 | |
| a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0 |
| a ~ b => Enum (a :~: b) | Since: base-4.7.0.0 |
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 |
| Show (a :~: b) | Since: base-4.7.0.0 |
| Eq (a :~: b) | Since: base-4.7.0.0 |
| Ord (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
class GEq (f :: k -> Type) where #
Instances
| GEq SNat | |
| GEq SChar | |
| GEq SSymbol | |
| GEq (Tag s :: Type -> Type) Source # | |
| GEq (TypeRep :: k -> Type) | |
| GEq ((:~:) a :: k -> Type) | |
| (GEq a, GEq b) => GEq (Product a b :: k -> Type) | |
| (GEq a, GEq b) => GEq (Sum a b :: k -> Type) | |
| GEq ((:~~:) a :: k -> Type) | |
| (GEq a, GEq b) => GEq (a :*: b :: k -> Type) | |
| (GEq f, GEq g) => GEq (f :+: g :: k -> Type) | |
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 | |
| Show (GOrdering a b) | |
| Eq (GOrdering a b) | |
| Ord (GOrdering a b) | |
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 #
Instances
| GCompare SNat | |
| GCompare SChar | |
| GCompare SSymbol | |
| GCompare (Tag s :: Type -> Type) Source # | |
| GCompare (TypeRep :: k -> Type) | |
| GCompare ((:~:) a :: k -> Type) | |
| (GCompare a, GCompare b) => GCompare (Product a b :: k -> Type) | |
| (GCompare a, GCompare b) => GCompare (Sum a b :: k -> Type) | |
| GCompare ((:~~:) a :: k -> Type) | |
| (GCompare a, GCompare b) => GCompare (a :*: b :: k -> Type) | |
| (GCompare f, GCompare g) => GCompare (f :+: g :: k -> Type) | |