- data Tag s a
- newTag :: PrimMonad m => m (Tag (PrimState m) a)
- data RealWorld
- data a := b where
- class GEq f where
- data GOrdering a b where
- class GEq f => GCompare f where
Tag type is like an ad-hoc GADT allowing runtime creation of new
constructors. Specifically, it is like a GADT "enumeration" with one
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,
Tags and values of type
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
Uniq is truly unique and only one
Tag is ever constructed from
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.
(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
RealWorld is deeply magical. It is primitive, but it is not
ptrArg). We never manipulate values of type
RealWorld; it's only used in the type system, to parameterise
|Show (Uniq RealWorld)|
There is only one
|GShow (Tag RealWorld)|
|Show (Tag RealWorld a)|
data a := b where
A GADT witnessing equality of two types. Its only inhabitant is
class GEq f where
A class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them.
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)
data GOrdering a b 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.
Type class for orderable GADT-like structures. When 2 things are equal,
must return a witness that their parameter types are equal as well (GEQ).
|Type class for comparable GADT-like structures. When 2 things are equal,
must return a witness that their parameter types are equal as well (