| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Control.Distributed.Session.STChannel
Description
Defines a session typed channel as a wrapper over the typed channel from Cloud Haskell
We define a session typed channel to overcome the limitation of a typed channel that can only send and receive messages of a single type.
Underneath we actually do the same, and make use of unsafeCoerce to coerce a value's type to that described in the session typed.
Session types do not entirely guarantee safety of using unsafeCoerce. One can use the same session typed send port over and over again,
while the correpsonding receive port might progress through the session type resulting in a desync of types between the send and receive port.
It is for this reason recommended to always make use of STChannelT that always progresses the session type of a port after a session typed action.
- data Message = Serializable a => Message a
- data STSendPort l = STSendPort (SendPort Message)
- data STReceivePort l = STReceivePort (ReceivePort Message)
- type STChan s = (STSendPort (RemoveRecv s), STReceivePort (RemoveSend s))
- type STChanBi s r = (STSendPort (RemoveRecv s), STReceivePort (RemoveSend r))
- type UTChan = (SendPort Message, ReceivePort Message)
- newSTChan :: Proxy s -> Process (STChan s)
- newSTChanBi :: Proxy s -> Proxy r -> Process (STChanBi s r)
- newUTChan :: Process UTChan
- toSTChan :: UTChan -> Proxy s -> STChan s
- toSTChanBi :: UTChan -> Proxy s -> Proxy r -> STChanBi s r
- sendProxy :: STSendPort s -> Proxy s
- recvProxy :: STReceivePort s -> Proxy s
- sendSTChan :: Serializable a => STSendPort (Cap ctx (a :!> l)) -> a -> Process (STSendPort (Cap ctx l))
- recvSTChan :: Serializable a => STReceivePort (Cap ctx (a :?> l)) -> Process (a, STReceivePort (Cap ctx l))
- class STSplit m where
- class STRec m where
- data STChannelT m p q a = STChannelT {
- runSTChannelT :: (STSendPort (Left p), STReceivePort (Right p)) -> m (a, (STSendPort (Left q), STReceivePort (Right q)))
- sendSTChanM :: Serializable a => a -> STChannelT Process (Cap ctx (a :!> l) :*: r) (Cap ctx l :*: r) ()
- recvSTChanM :: Serializable a => STChannelT Process (l :*: Cap ctx (a :?> r)) (l :*: Cap ctx r) a
- sel1ChanM :: STChannelT Process (Cap lctx (Sel (l ': ls)) :*: Cap rctx (Sel (r ': rs))) (Cap lctx l :*: Cap rctx r) ()
- sel2ChanM :: STChannelT Process (Cap lctx (Sel (s1 ': (t1 ': xs1))) :*: Cap rctx (Sel (s2 ': (t2 ': xs2)))) (Cap lctx (Sel (t1 ': xs1)) :*: Cap rctx (Sel (t2 ': xs2))) ()
- off1ChanM :: STChannelT Process (Cap lctx (Off (l ': ls)) :*: Cap rctx (Off (r ': rs))) (Cap lctx l :*: Cap rctx r) ()
- off2ChanM :: STChannelT Process (Cap lctx (Off (s1 ': (t1 ': xs1))) :*: Cap rctx (Off (s2 ': (t2 ': xs2)))) (Cap lctx (Off (t1 ': xs1)) :*: Cap rctx (Off (t2 ': xs2))) ()
- recChanM :: STChannelT Process (Cap sctx (R s) :*: Cap rctx (R r)) (Cap (s ': sctx) s :*: Cap (r ': rctx) r) ()
- wkChanM :: STChannelT Process (Cap (t ': sctx) (Wk s) :*: Cap (k ': rctx) (Wk r)) (Cap sctx s :*: Cap rctx r) ()
- varChanM :: STChannelT Process (Cap (s ': sctx) V :*: Cap (r ': rctx) V) (Cap (s ': sctx) s :*: Cap (r ': rctx) r) ()
- epsChanM :: STChannelT Process (Cap ctx Eps :*: Cap ctx Eps) (Cap ctx Eps :*: Cap ctx Eps) ()
Data types
Basic message type that existentially quantifies the content of the message
Constructors
| Serializable a => Message a |
data STSendPort l Source #
Session typed send port as a wrapper over SendPort Message. It is parameterized with a capability/sessiontype.
Constructors
| STSendPort (SendPort Message) |
Instances
data STReceivePort l Source #
Session typed receive port as a wrapper over ReceivePort Message. It is parameterized with a capability/sessiontype.
Constructors
| STReceivePort (ReceivePort Message) |
Instances
Type synonyms
type STChan s = (STSendPort (RemoveRecv s), STReceivePort (RemoveSend s)) Source #
Type synonym for a session typed channel given a single session type
This removes recv session types from the given session type as it is passed to the send port type
Also removes send session types from the given session type as it is passed to the receive port type
type STChanBi s r = (STSendPort (RemoveRecv s), STReceivePort (RemoveSend r)) Source #
Same as STChan, but it is given a session type for the send port type and a separate session type for the receive port type
Create
newSTChan :: Proxy s -> Process (STChan s) Source #
Creates a new session typed channel given a single session type
newSTChanBi :: Proxy s -> Proxy r -> Process (STChanBi s r) Source #
Creates a new session typed channel given separate session types for the send port and receive port
toSTChan :: UTChan -> Proxy s -> STChan s Source #
Converts an unsession typed channel to a session typed channel
toSTChanBi :: UTChan -> Proxy s -> Proxy r -> STChanBi s r Source #
Converts an unsession typed channel to a session typed channel
sendProxy :: STSendPort s -> Proxy s Source #
Converts a session typed send port into a Proxy
recvProxy :: STReceivePort s -> Proxy s Source #
Converts a session typed receive port into a Proxy
Usage
sendSTChan :: Serializable a => STSendPort (Cap ctx (a :!> l)) -> a -> Process (STSendPort (Cap ctx l)) Source #
Sends a message using a session typed send port
recvSTChan :: Serializable a => STReceivePort (Cap ctx (a :?> l)) -> Process (a, STReceivePort (Cap ctx l)) Source #
Receives a message using a session typed receive port
class STSplit m where Source #
Type class that defines combinators for branching on a session typed port
Methods
sel1Chan :: m (Cap ctx (Sel (s ': xs))) -> m (Cap ctx s) Source #
select the first branch of a selection using the given port
sel2Chan :: m (Cap ctx (Sel (s ': (t ': xs)))) -> m (Cap ctx (Sel (t ': xs))) Source #
select the second branch of a selection using the given port
off1Chan :: m (Cap ctx (Off (s ': xs))) -> m (Cap ctx s) Source #
select the first branch of an offering using the given port
off2Chan :: m (Cap ctx (Off (s ': (t ': xs)))) -> m (Cap ctx (Off (t ': xs))) Source #
select the second branch of an offering using the given port
Instances
Type class for recursion on a session typed port
Methods
recChan :: m (Cap ctx (R s)) -> m (Cap (s ': ctx) s) Source #
wkChan :: m (Cap (t ': ctx) (Wk s)) -> m (Cap ctx s) Source #
varChan :: m (Cap (s ': ctx) V) -> m (Cap (s ': ctx) s) Source #
Instances
Channel transformer
data STChannelT m p q a Source #
Indexed monad transformer that is indexed by two products of session types
This monad also acts as a state monad that whose state is defined by a session typed channel and dependent on the indexing of the monad.
Constructors
| STChannelT | |
Fields
| |
sendSTChanM :: Serializable a => a -> STChannelT Process (Cap ctx (a :!> l) :*: r) (Cap ctx l :*: r) () Source #
Send a message
Only the session type of the send port needs to be adjusted
recvSTChanM :: Serializable a => STChannelT Process (l :*: Cap ctx (a :?> r)) (l :*: Cap ctx r) a Source #
receive a message
Only the session type of the receive port needs to be adjusted
sel1ChanM :: STChannelT Process (Cap lctx (Sel (l ': ls)) :*: Cap rctx (Sel (r ': rs))) (Cap lctx l :*: Cap rctx r) () Source #
select the first branch of a selection
Both ports are now adjusted. This is similarly so for the remaining combinators.
sel2ChanM :: STChannelT Process (Cap lctx (Sel (s1 ': (t1 ': xs1))) :*: Cap rctx (Sel (s2 ': (t2 ': xs2)))) (Cap lctx (Sel (t1 ': xs1)) :*: Cap rctx (Sel (t2 ': xs2))) () Source #
select the second branch of a selection
off1ChanM :: STChannelT Process (Cap lctx (Off (l ': ls)) :*: Cap rctx (Off (r ': rs))) (Cap lctx l :*: Cap rctx r) () Source #
select the first branch of an offering
off2ChanM :: STChannelT Process (Cap lctx (Off (s1 ': (t1 ': xs1))) :*: Cap rctx (Off (s2 ': (t2 ': xs2)))) (Cap lctx (Off (t1 ': xs1)) :*: Cap rctx (Off (t2 ': xs2))) () Source #
select the second branch of an offering
recChanM :: STChannelT Process (Cap sctx (R s) :*: Cap rctx (R r)) (Cap (s ': sctx) s :*: Cap (r ': rctx) r) () Source #
delimit scope of recursion
wkChanM :: STChannelT Process (Cap (t ': sctx) (Wk s) :*: Cap (k ': rctx) (Wk r)) (Cap sctx s :*: Cap rctx r) () Source #
weaken scope of recursion