0 | module Data.Linear.Unique
 1 |
 2 | import public Data.Linear.Token
 3 | import Data.Linear.Ref1
 4 |
 5 | %default total
 6 |
 7 | ||| A unique identifier in state thread `s`.
 8 | |||
 9 | ||| Every `Token s` generated is guaranteed to be unique.
10 | ||| The API of `Token s` consists of only two capabilities:
11 | ||| generation of tokens via `token1` and `token`, and a total
12 | ||| ordering of tokens of the same state thread.
13 | |||
14 | ||| Unique tokens haven am important application as unique identifiers
15 | ||| and keys in many applications. We could generate such tokens by
16 | ||| threading a pure counter through all computations just as with the
17 | ||| state monad. However, in performance sensitive code this could be
18 | ||| to hight a price to pay. Therefore, the unique tokens presented
19 | ||| here come with far less computational overhead.
20 | |||
21 | ||| Implementation detail: Tokens are all generated from a single
22 | ||| global mutable counter in a thread-safe manner. However, only
23 | ||| tokens of the same state thread can be compared. This makes sure
24 | ||| that from an outside view, referential transparency is upheld.
25 | export
26 | record Token (s : Type) where
27 |   constructor T
28 |   value : Nat
29 |
30 | export %inline
31 | Eq (Token s) where
32 |   T x == T y = x == y
33 |
34 | export %inline
35 | Ord (Token s) where
36 |   compare (T x) (T y) = compare x y
37 |
38 | ||| Note: This prints the inner value of a `Token s`. Using
39 | |||       `show` on tokens therefore breaks referential transparency.
40 | |||       Only use this for testing and debugging.
41 | export %inline
42 | Show (Token s) where
43 |   show (T v) = show v
44 |
45 | ||| Returns the internal natural number of a `Token`.
46 | |||
47 | ||| Note: This is an implementation detail mainly used for testing.
48 | |||       Consider `Token`s to be opaque values with an `Eq` and
49 | |||       `Ord` implementation. Nothing else. Using this function
50 | |||       breaks referential transparency!
51 | export %inline
52 | unsafeVal : Token s -> Nat
53 | unsafeVal = value
54 |
55 | -- Internal mutable token state. This is read and updated
56 | -- via `casupdate1`, which is thread-safe, but currently works
57 | -- only on Chez and JavaScript (and, possibly, Racket).
58 | %noinline
59 | tok_ : Ref s Nat
60 | tok_ = believe_me $ unsafePerformIO $ newref 0
61 |
62 | ||| Generates a new unique token.
63 | |||
64 | ||| This token is unique throughout the lifetime of an application,
65 | ||| as it is generated from a single, global, mutable reference.
66 | ||| Unique token generation is thread-safe.
67 | export
68 | token1 : F1 s (Token s)
69 | token1 t =
70 |   assert_total $
71 |    let v    # t := read1 tok_ t
72 |        True # t := caswrite1 tok_ v (S v) t | _ # t => token1 t
73 |     in T v # t
74 |
75 | ||| Generates a new unique token.
76 | |||
77 | ||| This token is unique throughout the lifetime of an application,
78 | ||| as it is generated from a single, global, mutable reference.
79 | ||| Unique token generation is thread-safe.
80 | export %inline
81 | token : Lift1 s f => f (Token s)
82 | token = lift1 token1
83 |