Idris2Doc : Control.Monad.ST

Control.Monad.ST

Provides mutable references as described in Lazy Functional State Threads.

Definitions

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: export
newSTRef : a -> ST s (STRef s a)
  Create a new mutable reference with the given value.

Totality: total
Visibility: export
readSTRef : 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: export
writeSTRef : STRef s a -> a -> ST s ()
  Write to a mutable reference.

Totality: total
Visibility: export
modifySTRef : STRef s a -> (a -> a) -> ST s ()
  Apply a function to the contents of a mutable reference.

Totality: total
Visibility: export