prim-uniq: Opaque unique identifiers in primitive state monads

[ data, dependent-types, library, public-domain ] [ Propose Tags ]

Opaque unique identifiers in primitive state monads and a GADT-like type using them as witnesses of type equality.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.1, 0.1.0.1, 0.2
Change log ChangeLog.md
Dependencies base (>=3 && <5), dependent-sum (>=0.7 && <0.8), primitive [details]
License LicenseRef-PublicDomain
Author James Cook <mokus@deepbondi.net>
Maintainer Obsidian Systems, LLC <maintainer@obsidian.systems>
Category Data, Dependent Types
Home page https://github.com/obsidiansystems/prim-uniq
Source repo head: git clone https://github.com/obsidiansystems/prim-uniq
Uploaded by BertramFelgenhauer at 2020-04-15T14:37:09Z
Distributions Arch:0.2, Debian:0.2, LTSHaskell:0.2, NixOS:0.2, Stackage:0.2
Reverse Dependencies 4 direct, 53 indirect [details]
Downloads 6928 total (69 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2020-04-15 [all 1 reports]

Readme for prim-uniq-0.2

[back to package description]

Build Status

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 Tags, 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