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.)
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) Source # | |
Defined in Unsafe.Unique.Tag | |
Show (Uniq RealWorld) Source # | There is only one |
Show (Tag RealWorld a) Source # | |
data (a :: k) :~: (b :: k) where infix 4 #
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 GHC.Internal.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 :: k). 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 GHC.Internal.Data.Type.Equality Methods succ :: (a :~: b) -> a :~: b # pred :: (a :~: b) -> 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] # | |
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 GHC.Internal.Data.Type.Equality |
class GEq (f :: k -> Type) where #
A class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them.
This class is sometimes confused with TestEquality
from base.
TestEquality
only checks type equality.
Consider
>>>
data Tag a where TagInt1 :: Tag Int; TagInt2 :: Tag Int
The correct
instance isTestEquality
Tag
>>>
:{
instance TestEquality Tag where testEquality TagInt1 TagInt1 = Just Refl testEquality TagInt1 TagInt2 = Just Refl testEquality TagInt2 TagInt1 = Just Refl testEquality TagInt2 TagInt2 = Just Refl :}
While we can define
instanceGEq
Tag wheregeq
=testEquality
this will mean we probably want to have
instanceEq
Tag where _==
_ = True
Note: In the future version of some
package (to be released around GHC-9.6 / 9.8) the
forall a. Eq (f a)
constraint will be added as a constraint to GEq
,
with a law relating GEq
and Eq
:
geq
x y = Just Refl ⇒ x == y = True ∀ (x :: f a) (y :: f b) x == y ≡ isJust (geq
x y) ∀ (x, y :: f a)
So, the more useful
instance would differentiate between
different constructors:GEq
Tag
>>>
:{
instance GEq Tag where geq TagInt1 TagInt1 = Just Refl geq TagInt1 TagInt2 = Nothing geq TagInt2 TagInt1 = Nothing geq TagInt2 TagInt2 = Just Refl :}
which is consistent with a derived Eq
instance for Tag
>>>
deriving instance Eq (Tag a)
Note that even if a ~ b
, the
may
be geq
(x :: f a) (y :: f b)Nothing
(when value terms are inequal).
The consistency of GEq
and Eq
is easy to check by exhaustion:
>>>
let checkFwdGEq :: (forall a. Eq (f a), GEq f) => f a -> f b -> Bool; checkFwdGEq x y = case geq x y of Just Refl -> x == y; Nothing -> True
>>>
(checkFwdGEq TagInt1 TagInt1, checkFwdGEq TagInt1 TagInt2, checkFwdGEq TagInt2 TagInt1, checkFwdGEq TagInt2 TagInt2)
(True,True,True,True)
>>>
let checkBwdGEq :: (Eq (f a), GEq f) => f a -> f a -> Bool; checkBwdGEq x y = if x == y then isJust (geq x y) else isNothing (geq x y)
>>>
(checkBwdGEq TagInt1 TagInt1, checkBwdGEq TagInt1 TagInt2, checkBwdGEq TagInt2 TagInt1, checkBwdGEq TagInt2 TagInt2)
(True,True,True,True)
Methods
geq :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #
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 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) | Since: some-1.0.4 |
(GEq a, GEq b) => GEq (a :*: b :: k -> Type) | Since: some-1.0.4 |
(GEq f, GEq g) => GEq (f :+: g :: k -> Type) | Since: some-1.0.4 |
data GOrdering (a :: k) (b :: k) where #
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). 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 :: k). 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 # (<) :: 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 # |
class GEq f => GCompare (f :: k -> Type) where #
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
).
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) | Since: some-1.0.4 |
(GCompare a, GCompare b) => GCompare (a :*: b :: k -> Type) | Since: some-1.0.4 |
(GCompare f, GCompare g) => GCompare (f :+: g :: k -> Type) | Since: some-1.0.4 |