data STRef : Type -> Type -> Type
A mutable reference, bound to a state thread.
A value of type `STRef s a` contains a mutable `a`, bound to a "thread"
`s`. Any access to the reference must occur in an `ST s` monad with the
same "thread".
Totality: total
Visibility: export
Constructor: MkSTRef : IORef a -> STRef s a
data ST : Type -> Type -> Type
The `ST` monad allows for mutable access to references, but unlike `IO`, it
is "escapable".
The parameter `s` is a "thread" -- it ensures that access to mutable
references created in each thread must occur in that same thread.
Totality: total
Visibility: export
Constructor: MkST : IO a -> ST s a
Hints:
Applicative (ST s)
Functor (ST s)
Monad (ST s)
runST : ST s a -> a
Run a `ST` computation.
Totality: total
Visibility: exportnewSTRef : a -> ST s (STRef s a)
Create a new mutable reference with the given value.
Totality: total
Visibility: exportreadSTRef : STRef s a -> ST s a
Read the value of a mutable reference.
This occurs within `ST s` to prevent `STRef`s from being usable if they are
"leaked" via `runST`.
Totality: total
Visibility: exportwriteSTRef : STRef s a -> a -> ST s ()
Write to a mutable reference.
Totality: total
Visibility: exportmodifySTRef : STRef s a -> (a -> a) -> ST s ()
Apply a function to the contents of a mutable reference.
Totality: total
Visibility: export