Idris2Doc : Control.Monad.ST

Control.Monad.ST

Provides mutable references as described in Lazy Functional State Threads.

Definitions

dataSTRef : 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 : IORefa->STRefsa
dataST : 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 : IOa->STsa

Hints:
Applicative (STs)
Functor (STs)
Monad (STs)
runST : STsa->a
  Run a `ST` computation.

Totality: total
Visibility: export
newSTRef : a->STs (STRefsa)
  Create a new mutable reference with the given value.

Totality: total
Visibility: export
readSTRef : STRefsa->STsa
  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 : STRefsa->a->STs ()
  Write to a mutable reference.

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

Totality: total
Visibility: export