record Token : Type -> Type A unique identifier in state thread `s`.
Every `Token s` generated is guaranteed to be unique.
The API of `Token s` consists of only two capabilities:
generation of tokens via `token1` and `token`, and a total
ordering of tokens of the same state thread.
Unique tokens haven am important application as unique identifiers
and keys in many applications. We could generate such tokens by
threading a pure counter through all computations just as with the
state monad. However, in performance sensitive code this could be
to hight a price to pay. Therefore, the unique tokens presented
here come with far less computational overhead.
Implementation detail: Tokens are all generated from a single
global mutable counter in a thread-safe manner. However, only
tokens of the same state thread can be compared. This makes sure
that from an outside view, referential transparency is upheld.
Totality: total
Visibility: export
Constructor: T : Nat -> Token s
Projection: .value : Token s -> Nat
Hints:
Eq (Token s)Ord (Token s)Show (Token s)
unsafeVal : Token s -> Nat Returns the internal natural number of a `Token`.
Note: This is an implementation detail mainly used for testing.
Consider `Token`s to be opaque values with an `Eq` and
`Ord` implementation. Nothing else. Using this function
breaks referential transparency!
Totality: total
Visibility: exporttoken1 : F1 s (Token s) Generates a new unique token.
This token is unique throughout the lifetime of an application,
as it is generated from a single, global, mutable reference.
Unique token generation is thread-safe.
Totality: total
Visibility: exporttoken : Lift1 s f => f (Token s) Generates a new unique token.
This token is unique throughout the lifetime of an application,
as it is generated from a single, global, mutable reference.
Unique token generation is thread-safe.
Totality: total
Visibility: export