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