Safe Haskell | None |
---|---|
Language | Haskell2010 |
This library implements the ST2 monad, a type using GDP (ghosts of departed proofs)
to define shared regions of memory between local mutable state threads. This allows
us to define a region of the heap in more minute contours, with each state thread
having explicit access to regions in memory. This is achieved using the function runST2
,
which in effects lets the user run a computation that makes use of two partially-overlapping
memory regions. Within that computation, the user can run sub-computations bound to one or
the other memory region. Furthermore, a sub-computation can move any variable that it owns
into the common overlap via share
.
An example is shown in below, where one sub-computation creates two cells: one private, and the other shared. A second sub-computation has unconstrained access to the shared cell. Yet even though the private reference is also in scope during the second sub-computation, any attempts to access it there will fail to compile.
>>>
:{
stSharingDemo :: Bool stSharingDemo = runST2 $ do -- In the "left" memory region, create and return -- two references; one shared, and one not shared. (secret, ref) <- liftL $ do unshared <- newSTRef 42 shared <- share =<< newSTRef 17 return (unshared, shared) -- In the "right" memory region, mutate the shared -- reference. If we attempt to access the non-shared -- reference here, the program will not compile. liftR $ do let mine = use (symm ref) x <- readSTRef mine writeSTRef mine (x + 1) -- Back in the "left" memory region, verify that the -- unshared reference still holds its original value. liftL $ do check <- readSTRef secret return (check == 42) :}
Synopsis
- newtype ST s a = ST (STRep (Any ~~ s) a)
- type STRep s a = State# s -> (#State# s, a#)
- fixST :: (a -> ST s a) -> ST s a
- liftST :: ST s a -> State# s -> STret s a
- runST :: (forall s. ST s a) -> a
- data STRef s a = STRef (MutVar# s a)
- newSTRef :: a -> ST s (STRef s a)
- readSTRef :: STRef s a -> ST s a
- writeSTRef :: STRef s a -> a -> ST s ()
- type (∩) s s' = Common s s'
- data Common s s'
- share :: STRef s a -> ST s (STRef (Common s s') a)
- liftL :: ST s a -> ST (Common s s') a
- liftR :: ST s' a -> ST (Common s s') a
- use :: STRef (Common s s') a -> STRef s a
- symm :: STRef (Common s s') a -> STRef (Common s' s) a
- runST2 :: (forall s s'. ST (Common s s') a) -> a
- toBaseST :: ST s a -> ST s a
- fromBaseST :: ST s a -> ST s a
- data STret s a
- unsafeInterleaveST :: ST s a -> ST s a
- unsafeDupableInterleaveST :: ST s a -> ST s a
- stToPrim :: PrimMonad m => ST (PrimState m) a -> m a
- unsafePrimToST :: PrimBase m => m a -> ST s a
- unsafeSTToPrim :: PrimBase m => ST s a -> m a
- unsafeInlineST :: ST s a -> a
- stToIO :: ST RealWorld a -> IO a
- ioToST :: IO a -> ST RealWorld a
- data RealWorld
ST2 API
The strict state-transformer monad.
A computation of type
transforms an internal state indexed
by ST
s as
, and returns a value of type a
.
The s
parameter is either
- an uninstantiated type variable (inside invocations of
runST
), or RealWorld
(inside invocations ofstToIO
).
It serves to keep the internal states of different invocations
of runST
separate from each other and from invocations of
stToIO
.
The >>=
and >>
operations are strict in the state (though not in
values stored in the state). For example,
runST
(writeSTRef _|_ v >>= f) = _|_
type STRep s a = State# s -> (#State# s, a#) Source #
Convenience type alias for expressing ST computations more succintly.
fixST :: (a -> ST s a) -> ST s a Source #
Allow the result of a state transformer computation to be used (lazily) inside the computation.
Note that if f
is strict,
.fixST
f = _|_
runST :: (forall s. ST s a) -> a Source #
Return the value computed by a state transformer computation.
The forall
ensures that the internal state used by the ST
computation is inaccessible to the rest of the program.
A value of type STRef s a
is a mutable variable in state thread s
,
containing a value of type a
A type that shows that the state threads s and s' refer to a heap region that overlaps in some way such that s and s' can both access the overlap, while maintaining privacy in their own heap regions.
share :: STRef s a -> ST s (STRef (Common s s') a) Source #
Move a variable that you own into a region with common overlap.
liftL :: ST s a -> ST (Common s s') a Source #
Lift an ST
computation into a context with another heap region
liftR :: ST s' a -> ST (Common s s') a Source #
Lift an ST
computation into a context with another heap region
use :: STRef (Common s s') a -> STRef s a Source #
Given proof that one has access to the heap regions s and s', yield an STRef to the region s.
symm :: STRef (Common s s') a -> STRef (Common s' s) a Source #
Given proof that one has access to the heap regions s and s',
yield an STRef
that swaps the order of the regions.
runST2 :: (forall s s'. ST (Common s s') a) -> a Source #
Return the value computed by a state transformer computation
over a shared heap. The forall
ensures that the internal state(s)
used by the ST
computation is inaccessible to the rest of the program.
Unsafe API
fromBaseST :: ST s a -> ST s a Source #
Convert an ST to an ST2
A simple product type containing both the state thread and value inside of the ST
unsafeInterleaveST :: ST s a -> ST s a Source #
unsafeInterleaveST
allows an ST
computation to be deferred
lazily. When passed a value of type ST a
, the ST
computation will
only be performed when the value of the a
is demanded.
unsafeDupableInterleaveST :: ST s a -> ST s a Source #
unsafeDupableInterleaveST
allows an ST
computation to be deferred
lazily. When passed a value of type ST a
, the ST
computation will
only be performed when the value of the a
is demanded.
The computation may be performed multiple times by different threads,
possibly at the same time. To prevent this, use unsafeInterleaveST
instead.
unsafePrimToST :: PrimBase m => m a -> ST s a Source #
unsafeSTToPrim :: PrimBase m => ST s a -> m a Source #
unsafeInlineST :: ST s a -> a Source #