prim-uniq-0.2: Opaque unique identifiers in primitive state monads

Safe Haskell | Trustworthy
Language | Haskell98

Data.Unique.Tag

Synopsis

- data Tag s a
- newTag :: PrimMonad m => m (Tag (PrimState m) a)
- data RealWorld
- data (a :: k) :~: (b :: k) where
  - Refl :: forall {k} (a :: k). a :~: a
- class GEq (f :: k -> Type) where
  - geq :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
- data GOrdering (a :: k) (b :: k) where
  - 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
- class GEq f => GCompare (f :: k -> Type) where
  - gcompare :: forall (a :: k) (b :: k). f a -> f b -> GOrdering a b

# 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 `Tag`s 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 :: Tag s a -> Tag s b -> GOrdering a b #
GEq (Tag s :: Type -> Type) Source # |
Instance details Defined in Unsafe.Unique.Tag Methods geq :: Tag s a -> Tag s b -> Maybe (a :~: b) #
GShow (Tag RealWorld) Source # |
Instance details Defined in Unsafe.Unique.Tag Methods gshowsPrec :: Int -> Tag RealWorld a -> ShowS
Show (Tag RealWorld a) Source # |
Instance details Defined in Unsafe.Unique.Tag Methods showsPrec :: Int -> Tag RealWorld a -> ShowS Source # show :: Tag RealWorld a -> String Source # showList :: [Tag RealWorld a] -> ShowS Source #
Eq (Tag s a) Source # |
Instance details Defined in Unsafe.Unique.Tag Methods (==) :: Tag s a -> Tag s a -> Bool Source # (/=) :: Tag s a -> Tag s a -> Bool Source #
Ord (Tag s a) Source # |
Instance details Defined in Unsafe.Unique.Tag Methods compare :: Tag s a -> Tag s a -> Ordering Source # (<) :: Tag s a -> Tag s a -> Bool Source # (<=) :: Tag s a -> Tag s a -> Bool Source # (>) :: Tag s a -> Tag s a -> Bool Source # (>=) :: Tag s a -> Tag s a -> Bool Source # max :: Tag s a -> Tag s a -> Tag s a Source # min :: Tag s a -> Tag s a -> Tag s a Source #

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

`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

Instances details

GShow (Tag RealWorld) |
Instance details Defined in Unsafe.Unique.Tag Methods gshowsPrec :: Int -> Tag RealWorld a -> ShowS

Show (Uniq RealWorld) Source #

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 `Uniq`s.

Instance details Defined in Unsafe.Unique.Prim Methods showsPrec :: Int -> Uniq RealWorld -> ShowS Source # show :: Uniq RealWorld -> String Source # showList :: [Uniq RealWorld] -> ShowS Source #
Show (Tag RealWorld a) Source # |
Instance details Defined in Unsafe.Unique.Tag Methods showsPrec :: Int -> Tag RealWorld a -> ShowS Source # show :: Tag RealWorld a -> String Source # showList :: [Tag RealWorld a] -> ShowS 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

Constructors

Refl :: forall {k} (a :: k). a :~: a |

#### Instances

Instances details

TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #
GCompare ((:~:) a :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> GOrdering a0 b #
GEq ((:~:) a :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k) (b :: k). (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 :: k). Int -> (a :~: a0) -> ShowS
a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods minBound :: a :~: b Source # maxBound :: a :~: b Source #
a ~ b => Enum (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.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
Instance details Defined in GHC.Internal.Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) Source # readList :: ReadS [a :~: b] Source # readPrec :: ReadPrec (a :~: b) Source # readListPrec :: ReadPrec [a :~: b] Source #
Show (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS Source # show :: (a :~: b) -> String Source # showList :: [a :~: b] -> ShowS Source #
Eq (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool Source # (/=) :: (a :~: b) -> (a :~: b) -> Bool Source #
Ord (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

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

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

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

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

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

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

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

class GEq (f :: k -> Type) where #

Methods

geq :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #

#### Instances

Instances details

GEq SNat |
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) #
GEq SChar |
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b) #
GEq SSymbol |
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b) #
GEq (Tag s :: Type -> Type) Source # |
Instance details Defined in Unsafe.Unique.Tag Methods geq :: Tag s a -> Tag s b -> Maybe (a :~: b) #
GEq (TypeRep :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b) #
GEq ((:~:) a :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
(GEq a, GEq b) => GEq (Product a b :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k) (b0 :: k). Product a b a0 -> Product a b b0 -> Maybe (a0 :~: b0) #
(GEq a, GEq b) => GEq (Sum a b :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k) (b0 :: k). Sum a b a0 -> Sum a b b0 -> Maybe (a0 :~: b0) #
GEq ((:~~:) a :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) #
(GEq a, GEq b) => GEq (a :*: b :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k) (b0 :: k). (a :*: b) a0 -> (a :*: b) b0 -> Maybe (a0 :~: b0) #
(GEq f, GEq g) => GEq (f :+: g :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a :: k) (b :: k). (f :+: g) a -> (f :+: g) 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 :: k). Int -> GOrdering a a0 -> ShowS
Show (GOrdering a b) |
Instance details Defined in Data.GADT.Internal Methods showsPrec :: Int -> GOrdering a b -> ShowS Source # show :: GOrdering a b -> String Source # showList :: [GOrdering a b] -> ShowS Source #
Eq (GOrdering a b) |
Instance details Defined in Data.GADT.Internal Methods (==) :: GOrdering a b -> GOrdering a b -> Bool Source # (/=) :: GOrdering a b -> GOrdering a b -> Bool Source #
Ord (GOrdering a b) |

Instance details

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 #

Methods

gcompare :: forall (a :: k) (b :: k). f a -> f b -> GOrdering a b #

#### Instances

Instances details

GCompare SNat |
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> GOrdering a b #
GCompare SChar |
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> GOrdering a b #
GCompare SSymbol |
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> GOrdering a b #
GCompare (Tag s :: Type -> Type) Source # |
Instance details Defined in Unsafe.Unique.Tag Methods gcompare :: Tag s a -> Tag s b -> GOrdering a b #
GCompare (TypeRep :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> GOrdering a b #
GCompare ((:~:) a :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> GOrdering a0 b #
(GCompare a, GCompare b) => GCompare (Product a b :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k) (b0 :: k). Product a b a0 -> Product a b b0 -> GOrdering a0 b0 #
(GCompare a, GCompare b) => GCompare (Sum a b :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k) (b0 :: k). Sum a b a0 -> Sum a b b0 -> GOrdering a0 b0 #
GCompare ((:~~:) a :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> GOrdering a0 b #
(GCompare a, GCompare b) => GCompare (a :*: b :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k) (b0 :: k). (a :*: b) a0 -> (a :*: b) b0 -> GOrdering a0 b0 #
(GCompare f, GCompare g) => GCompare (f :+: g :: k -> Type) |
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a :: k) (b :: k). (f :+: g) a -> (f :+: g) b -> GOrdering a b #