diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,5 @@ +#!/usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain + diff --git a/prim-uniq.cabal b/prim-uniq.cabal new file mode 100644 --- /dev/null +++ b/prim-uniq.cabal @@ -0,0 +1,29 @@ +name: prim-uniq +version: 0.1 +stability: provisional + +cabal-version: >= 1.6 +build-type: Simple + +author: James Cook +maintainer: James Cook +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 diff --git a/src/Data/Unique/Prim.hs b/src/Data/Unique/Prim.hs new file mode 100644 --- /dev/null +++ b/src/Data/Unique/Prim.hs @@ -0,0 +1,6 @@ +module Data.Unique.Prim + ( Uniq, getUniq, RealWorld + ) where + +import Unsafe.Unique.Prim +import Control.Monad.Primitive (RealWorld) diff --git a/src/Data/Unique/Tag.hs b/src/Data/Unique/Tag.hs new file mode 100644 --- /dev/null +++ b/src/Data/Unique/Tag.hs @@ -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) diff --git a/src/Unsafe/Unique/Prim.hs b/src/Unsafe/Unique/Prim.hs new file mode 100644 --- /dev/null +++ b/src/Unsafe/Unique/Prim.hs @@ -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 diff --git a/src/Unsafe/Unique/Tag.hs b/src/Unsafe/Unique/Tag.hs new file mode 100644 --- /dev/null +++ b/src/Unsafe/Unique/Tag.hs @@ -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