prim-uniq (empty) → 0.1

raw patch · 6 files changed

+186/−0 lines, 6 filesdep +basedep +dependent-sumdep +primitivesetup-changed

Dependencies added: base, dependent-sum, primitive

Files

• Setup.lhs +5/−0
• prim-uniq.cabal +29/−0
• src/Data/Unique/Prim.hs +6/−0
• src/Data/Unique/Tag.hs +16/−0
• src/Unsafe/Unique/Prim.hs +71/−0
• src/Unsafe/Unique/Tag.hs +59/−0

@@ -0,0 +1,5 @@+#!/usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain+

@@ -0,0 +1,29 @@+name:                   prim-uniq+version:                0.1+stability:              provisional++cabal-version:          >= 1.6+build-type:             Simple++author:                 James Cook <mokus@deepbondi.net>+maintainer:             James Cook <mokus@deepbondi.net>+license:                PublicDomain+homepage:               https://github.com/mokus0/prim-uniq++category:               Data, Dependent Types+synopsis:               Opaque unique identifiers in primitive state monads+description:            Opaque unique identifiers in primitive state monads +                        and a GADT-like type using them as witnesses of type+                        equality.++source-repository head+  type:     git+  location: git://github.com/mokus0/prim-uniq.git++Library+  hs-source-dirs:       src+  exposed-modules:      Data.Unique.Prim+                        Data.Unique.Tag+                        Unsafe.Unique.Prim+                        Unsafe.Unique.Tag+  build-depends:        base >= 3 && <5, dependent-sum, primitive

@@ -0,0 +1,6 @@+module Data.Unique.Prim+    ( Uniq, getUniq, RealWorld+    ) where++import Unsafe.Unique.Prim+import Control.Monad.Primitive (RealWorld)

@@ -0,0 +1,16 @@+module Data.Unique.Tag+    ( Tag+    , newTag+    +    , RealWorld+    +    , (:=)(..)+    , GEq(..)+    +    , GOrdering(..)+    , GCompare(..)+    ) where++import Data.GADT.Compare+import Unsafe.Unique.Tag+import Control.Monad.Primitive (RealWorld)

@@ -0,0 +1,71 @@+{-# LANGUAGE BangPatterns, FlexibleInstances #-}+module Unsafe.Unique.Prim+    ( Uniq, getUniq+    , unsafeMkUniq, unsafeShowsPrecUniq, unsafeShowUniq+    ) where++import Control.Monad.Primitive+import Data.IORef+import System.IO.Unsafe++-- A smaller numeric type could be used, such as Word or Word64, but I+-- want to be able to guarantee uniqueness even over very long execution +-- times.  Smaller types would require either checking for overflow,+-- accepting the possibility of aliasing, or tracking allocation and +-- deallocation, which would be a lot of extra work.  Word64 is almost+-- certainly big enough for practical purposes, though.  Allocating one +-- 'Uniq' every nanosecond, it would take 584 years to start aliasing....+-- So, in the future I may choose to switch to Word64.++-- |A 'Uniq' is a value that can only be constructed under controlled +-- conditions (in IO or ST, basically), and once constructed can only be+-- compared to 'Uniq' values created under the same conditions (in the same+-- monad).  Upon comparison, a 'Uniq' is ONLY ever equal to itself.  Beyond+-- that, no promises regarding ordering are made except that once constructed+-- the order is deterministic and a proper ordering relation (eg, > is +-- transitive and irreflexive, etc.)+newtype Uniq s = Uniq Integer deriving (Eq, Ord)++-- |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 Show (Uniq RealWorld) where+    showsPrec = unsafeShowsPrecUniq++{-# NOINLINE nextUniq #-}+-- | [internal] Assuming the compiler behaves "as expected", this is a single+-- statically-created IORef holding the counter which will be used as the +-- source of new 'Prim' keys (in 'ST' and 'IO').+nextUniq :: IORef Integer+nextUniq = unsafePerformIO (newIORef 0)++-- |Construct a new 'Uniq' that is equal to itself, unequal to every other+-- 'Uniq' constructed in the same monad, and incomparable to every 'Uniq' +-- constructed in any other monad.+getUniq :: PrimMonad m => m (Uniq (PrimState m))+getUniq = unsafePrimToPrim (atomicModifyIORef nextUniq (\(!u) -> let !u' = u+1 in (u', Uniq u)))++-- |For the implementation of 'Uniq' construction in new monads, this operation+-- is exposed.  Users must accept responsibility for ensuring true uniqueness +-- across the lifetime of the resulting 'Uniq' value.  Failure to do so could+-- lead to type unsoundness in code depending on uniqueness as a type witness+-- (eg, "Data.Unique.Tag").+unsafeMkUniq :: Integer -> Uniq s+unsafeMkUniq n = Uniq n++-- |A `Show` instance for @`Uniq` s@ would not be sound, but for debugging+-- purposes we occasionally will want to do it anyway.  Its unsoundness is +-- nicely demonstrated by:+-- +-- > runST (fmap show getUniq) :: String+--+-- Which, despite having type 'String', is not referentially transparent.+unsafeShowsPrecUniq :: Int -> Uniq s -> ShowS+unsafeShowsPrecUniq p (Uniq u) = showsPrec p u++-- |See 'unsafeShowsPrecUniq'.+unsafeShowUniq :: Uniq s -> String+unsafeShowUniq (Uniq u) = show u

@@ -0,0 +1,59 @@+{-# LANGUAGE GADTs, FlexibleInstances #-}+module Unsafe.Unique.Tag+    ( Tag+    , newTag+    , veryUnsafeMkTag+    ) where++import Data.GADT.Compare+import Data.GADT.Show+import Unsafe.Unique.Prim+import Unsafe.Coerce+import Control.Monad.Primitive+import Control.Monad++-- |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.+newtype Tag s a = Tag (Uniq s) deriving (Eq, Ord)+instance Show (Tag RealWorld a) where showsPrec p (Tag u) = showsPrec p u+instance GShow (Tag RealWorld)  where gshowsPrec = showsPrec+instance GEq (Tag s) where+    geq (Tag a) (Tag b)+        | a == b    = Just (unsafeCoerce Refl)+        | otherwise = Nothing+instance GCompare (Tag s) where+    gcompare (Tag a) (Tag b) = case compare a b of+        LT -> GLT+        EQ -> unsafeCoerce (GEQ :: GOrdering () ())+        GT -> GGT++-- |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.)+newTag :: PrimMonad m => m (Tag (PrimState m) a)+newTag = liftM Tag getUniq++-- |Very dangerous! This is essentially a deferred 'unsafeCoerce': by creating+-- a tag with this function, the user accepts responsibility for ensuring +-- uniqueness of the 'Integer' across the lifetime of the 'Tag' (including+-- properly controlling the lifetime of the 'Tag' if necessary +-- by universal quantification when discharging the @s@ phantom type)+veryUnsafeMkTag :: Integer -> Tag s a+veryUnsafeMkTag = Tag . unsafeMkUniq