[](https://travis-ci.org/obsidiansystems/prim-uniq)
Unique values and an ad-hoc "unique-tag GADT"
=============================================
This library defines 2 types - `Uniq` and `Tag`.
`Uniq` is a traditional "unique value" type, extended with a state-token type parameter so it works in both `IO` and `ST`.
`Tag` is like `Uniq` with the addition of a phantom type parameter. The type of that parameter is fixed at the time the `Tag` is created, so the uniqueness of the tag means that equality of tag values witnesses equality of their phantom types. In other words, given two `Tag`s, if they are equal then their phantom type parameters are the same - just like pattern matching on a GADT constructor. The `GEq` and `GCompare` classes from the `dependent-sum` package can be used to discover that type equality, allowing `Tag` to be used for a pretty cool semi-dynamic typing scheme. For example (using the `dependent-map` library):
import Data.Unique.Tag
import Data.Dependent.Map
main = do
x <- newTag
y <- newTag
z <- newTag
let m1 = fromList [x :=> 3, y :=> "hello"]
m2 = fromList [x :=> 17, z :=> (True, x)]
-- the type checker would (rightly) reject this line:
-- m3 = singleton y ("foo", "bar")
print (m1 ! x)
print (m1 ! y)
print (m2 ! x)
print (m1 ! snd (m2 ! z))
Which would print:
3
"hello"
17
3