sessiontypes-distributed-0.1.0: Session types distributed

Safe HaskellNone
LanguageHaskell2010

Control.Distributed.Session.STChannel

Contents

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.

Synopsis

Data types

data Message Source #

Basic message type that existentially quantifies the content of the message

Constructors

Serializable a => Message a 

Instances

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

STRec STSendPort Source # 

Methods

recChan :: STSendPort (Cap Type ctx (R Type s)) -> STSendPort (Cap Type ((ST Type ': s) ctx) s) Source #

wkChan :: STSendPort (Cap Type ((ST Type ': t) ctx) (Wk Type s)) -> STSendPort (Cap Type ctx s) Source #

varChan :: STSendPort (Cap Type ((ST Type ': s) ctx) (V Type)) -> STSendPort (Cap Type ((ST Type ': s) ctx) s) Source #

STSplit STSendPort Source # 

Methods

sel1Chan :: STSendPort (Cap Type ctx (Sel Type ((ST Type ': s) xs))) -> STSendPort (Cap Type ctx s) Source #

sel2Chan :: STSendPort (Cap Type ctx (Sel Type ((ST Type ': s) ((ST Type ': t) xs)))) -> STSendPort (Cap Type ctx (Sel Type ((ST Type ': t) xs))) Source #

off1Chan :: STSendPort (Cap Type ctx (Off Type ((ST Type ': s) xs))) -> STSendPort (Cap Type ctx s) Source #

off2Chan :: STSendPort (Cap Type ctx (Off Type ((ST Type ': s) ((ST Type ': t) xs)))) -> STSendPort (Cap Type ctx (Off Type ((ST Type ': t) xs))) Source #

data STReceivePort l Source #

Session typed receive port as a wrapper over ReceivePort Message. It is parameterized with a capability/sessiontype.

Instances

STRec STReceivePort Source # 

Methods

recChan :: STReceivePort (Cap Type ctx (R Type s)) -> STReceivePort (Cap Type ((ST Type ': s) ctx) s) Source #

wkChan :: STReceivePort (Cap Type ((ST Type ': t) ctx) (Wk Type s)) -> STReceivePort (Cap Type ctx s) Source #

varChan :: STReceivePort (Cap Type ((ST Type ': s) ctx) (V Type)) -> STReceivePort (Cap Type ((ST Type ': s) ctx) s) Source #

STSplit STReceivePort Source # 

Methods

sel1Chan :: STReceivePort (Cap Type ctx (Sel Type ((ST Type ': s) xs))) -> STReceivePort (Cap Type ctx s) Source #

sel2Chan :: STReceivePort (Cap Type ctx (Sel Type ((ST Type ': s) ((ST Type ': t) xs)))) -> STReceivePort (Cap Type ctx (Sel Type ((ST Type ': t) xs))) Source #

off1Chan :: STReceivePort (Cap Type ctx (Off Type ((ST Type ': s) xs))) -> STReceivePort (Cap Type ctx s) Source #

off2Chan :: STReceivePort (Cap Type ctx (Off Type ((ST Type ': s) ((ST Type ': t) xs)))) -> STReceivePort (Cap Type ctx (Off Type ((ST Type ': t) xs))) Source #

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

type UTChan = (SendPort Message, ReceivePort Message) Source #

Unsession typed typed channel

It is essentially just a typed channel that is parameterized with Message.

We can carry around this type in Session, but not a STChan.

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

newUTChan :: Process UTChan Source #

Creates an unsession typed channel

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

Minimal complete definition

sel1Chan, sel2Chan, off1Chan, off2Chan

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

STSplit STReceivePort Source # 

Methods

sel1Chan :: STReceivePort (Cap Type ctx (Sel Type ((ST Type ': s) xs))) -> STReceivePort (Cap Type ctx s) Source #

sel2Chan :: STReceivePort (Cap Type ctx (Sel Type ((ST Type ': s) ((ST Type ': t) xs)))) -> STReceivePort (Cap Type ctx (Sel Type ((ST Type ': t) xs))) Source #

off1Chan :: STReceivePort (Cap Type ctx (Off Type ((ST Type ': s) xs))) -> STReceivePort (Cap Type ctx s) Source #

off2Chan :: STReceivePort (Cap Type ctx (Off Type ((ST Type ': s) ((ST Type ': t) xs)))) -> STReceivePort (Cap Type ctx (Off Type ((ST Type ': t) xs))) Source #

STSplit STSendPort Source # 

Methods

sel1Chan :: STSendPort (Cap Type ctx (Sel Type ((ST Type ': s) xs))) -> STSendPort (Cap Type ctx s) Source #

sel2Chan :: STSendPort (Cap Type ctx (Sel Type ((ST Type ': s) ((ST Type ': t) xs)))) -> STSendPort (Cap Type ctx (Sel Type ((ST Type ': t) xs))) Source #

off1Chan :: STSendPort (Cap Type ctx (Off Type ((ST Type ': s) xs))) -> STSendPort (Cap Type ctx s) Source #

off2Chan :: STSendPort (Cap Type ctx (Off Type ((ST Type ': s) ((ST Type ': t) xs)))) -> STSendPort (Cap Type ctx (Off Type ((ST Type ': t) xs))) Source #

class STRec m where Source #

Type class for recursion on a session typed port

Minimal complete definition

recChan, wkChan, varChan

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

STRec STReceivePort Source # 

Methods

recChan :: STReceivePort (Cap Type ctx (R Type s)) -> STReceivePort (Cap Type ((ST Type ': s) ctx) s) Source #

wkChan :: STReceivePort (Cap Type ((ST Type ': t) ctx) (Wk Type s)) -> STReceivePort (Cap Type ctx s) Source #

varChan :: STReceivePort (Cap Type ((ST Type ': s) ctx) (V Type)) -> STReceivePort (Cap Type ((ST Type ': s) ctx) s) Source #

STRec STSendPort Source # 

Methods

recChan :: STSendPort (Cap Type ctx (R Type s)) -> STSendPort (Cap Type ((ST Type ': s) ctx) s) Source #

wkChan :: STSendPort (Cap Type ((ST Type ': t) ctx) (Wk Type s)) -> STSendPort (Cap Type ctx s) Source #

varChan :: STSendPort (Cap Type ((ST Type ': s) ctx) (V Type)) -> STSendPort (Cap Type ((ST Type ': s) ctx) s) Source #

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 

Instances

Monad m => IxMonadT (Prod Type) STChannelT m Source # 

Methods

lift :: m a -> m m s s a #

Monad m => IxFunctor (Prod Type) (STChannelT m) Source # 

Methods

fmap :: (a -> b) -> f j k a -> f j k b #

Monad m => IxApplicative (Prod Type) (STChannelT m) Source # 

Methods

pure :: a -> f i i a #

(<*>) :: f s r (a -> b) -> f r k a -> f s k b #

Monad m => IxMonad (Prod Type) (STChannelT m) Source # 

Methods

(>>=) :: m s t a -> (a -> m t k b) -> m s k b #

(>>) :: m s t a -> m t k b -> m s k b #

return :: a -> m i i a #

fail :: String -> m i i a #

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

varChanM :: STChannelT Process (Cap (s ': sctx) V :*: Cap (r ': rctx) V) (Cap (s ': sctx) s :*: Cap (r ': rctx) r) () Source #

recursion variable (recurse here)

epsChanM :: STChannelT Process (Cap ctx Eps :*: Cap ctx Eps) (Cap ctx Eps :*: Cap ctx Eps) () Source #

ports are no longer usable