sessions-2008.7.18: Session Types for HaskellSource codeContentsIndex
Control.Concurrent.Session.Runtime
Description
Having actually described a session type, you'll now want to implement it! Use the methods of SMonad to chain functions together.
Synopsis
data OfferImpls where
OfferImplsNil :: OfferImpls Nil prog prog' finalState finalResult
(~||~) :: forall prog prog' progOut progIn outgoing incoming finalState finalResult jumps l current currentUX. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => SessionChain prog prog' (current, outgoing, incoming) finalState finalResult -> OfferImpls jumps prog prog' finalState finalResult -> OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog prog' finalState finalResult
sjump :: forall l prog prog' progOut progIn outgoing incoming current currentUX. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => SessionChain prog prog' (Cons (Jump l) Nil, Cons (Jump l) Nil, Cons (Jump l) Nil) (current, outgoing, incoming) ()
ssend :: forall t t' sp prog prog' cur nxtCur nxtOut incoming. (CompatibleTypes sp t' t, NextSend cur (Send (sp, t)) nxtCur) => t' -> SessionChain prog prog' (cur, Cons t nxtOut, incoming) (nxtCur, nxtOut, incoming) ()
class CompatibleTypes special a b | special a -> b, special b -> a where
convert :: special -> a -> b
srecv :: forall sp t prog prog' nxt nxt' outgoing. SessionChain prog prog' (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') (nxt, outgoing, nxt') t
srecvTest :: SessionChain prog prog' (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') Bool
srecvTestTimeOut :: forall prog prog' sp t nxt nxt' outgoing. Int -> SessionChain prog prog' (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') Bool
soffer :: forall current outgoing incoming finalResult prog prog' jumps. OfferImpls jumps prog prog' (current, outgoing, incoming) finalResult -> SessionChain prog prog' (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) finalResult
sselect :: forall prog prog' progOut progIn label jumps outgoing incoming current currentUX len jumpTarget. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, TyListLength jumps len, SmallerThanBool label len True, TypeNumberToInt label, TyListIndex jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', TyListIndex progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn jumpTarget (MVar (ProgramCell (Cell incoming))), TyListIndex prog jumpTarget currentUX, Expand prog currentUX current) => label -> SessionChain prog prog' (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) ()
run :: forall prog prog' progOut progIn init fromO fromI toO toI res res' currentUX currentUX' current current' toCur toCur'. (ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), DualT prog ~ prog', Dual prog prog', TyListIndex prog init currentUX, Expand prog currentUX current, TyListIndex prog' init currentUX', Expand prog' currentUX' current') => prog -> init -> SessionChain prog prog' (current, fromO, fromI) (toCur, toO, toI) res -> SessionChain prog' prog (current', fromI, fromO) (toCur', toI, toO) res' -> IO (res, res')
carefullySwapToNextCell :: MVar (ProgramCell a) -> IO (ProgramCell a)
Documentation
data OfferImpls whereSource
Use OfferImpls to construct the implementations of the branches of an offer. Really, it's just a slightly fancy list.
Constructors
OfferImplsNil :: OfferImpls Nil prog prog' finalState finalResult
(~||~) :: forall prog prog' progOut progIn outgoing incoming finalState finalResult jumps l current currentUX. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => SessionChain prog prog' (current, outgoing, incoming) finalState finalResult -> OfferImpls jumps prog prog' finalState finalResult -> OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog prog' finalState finalResultSource
Use to construct OfferImpls. This function automatically adds the necessary sjump to the start of each branch implementation.
sjump :: forall l prog prog' progOut progIn outgoing incoming current currentUX. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, SWellFormedConfig l (D0 E) prog, SWellFormedConfig l (D0 E) prog', TyListIndex progOut l (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn l (MVar (ProgramCell (Cell incoming))), TyListIndex prog l currentUX, Expand prog currentUX current) => SessionChain prog prog' (Cons (Jump l) Nil, Cons (Jump l) Nil, Cons (Jump l) Nil) (current, outgoing, incoming) ()Source
Perform a jump. Now you may think that you should indicate where you want to jump to. But of course, that's actually specified by the session type so you don't have to specify it at all in the implementation.
ssend :: forall t t' sp prog prog' cur nxtCur nxtOut incoming. (CompatibleTypes sp t' t, NextSend cur (Send (sp, t)) nxtCur) => t' -> SessionChain prog prog' (cur, Cons t nxtOut, incoming) (nxtCur, nxtOut, incoming) ()Source
Send a value to the other party. Of course, the value must be of the correct type indicated in the session type.
class CompatibleTypes special a b | special a -> b, special b -> a whereSource
Methods
convert :: special -> a -> bSource
show/hide Instances
CompatibleTypes SpecialNormal t t
CompatibleTypes SpecialSession t t
(TySubList invertedSessionsB invertedSessionsA True, TySubList sessionsToIdxB sessionsToIdxA True, ReducePairStructs (TyMap sessionsToIdxA idxsToPairStructsA) (TyMap sessionsToIdxB idxsToPairStructsB) (TyMap Nil Nil) (TyMap sessionsToIdxB idxsToPairStructsB)) => CompatibleTypes SpecialPid (Pid prog prog' invertedSessionsA sessionsToIdxA idxsToPairStructsA) (Pid prog prog' invertedSessionsB sessionsToIdxB idxsToPairStructsB)
(TySubList invertedSessionsB invertedSessionsA True, TySubList sessionsToIdxB sessionsToIdxA True, ReducePairStructs (TyMap sessionsToIdxA idxsToPairStructsA) (TyMap sessionsToIdxB idxsToPairStructsB) (TyMap Nil Nil) (TyMap sessionsToIdxB idxsToPairStructsB)) => CompatibleTypes SpecialPid (Pid prog prog' invertedSessionsA sessionsToIdxA idxsToPairStructsA) (Pid prog prog' invertedSessionsB sessionsToIdxB idxsToPairStructsB)
srecv :: forall sp t prog prog' nxt nxt' outgoing. SessionChain prog prog' (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') (nxt, outgoing, nxt') tSource
Recieve a value from the other party. This will block as necessary. The type of the value received is specified by the session type. No magic coercion needed.
srecvTest :: SessionChain prog prog' (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') BoolSource
srecvTestTimeOut :: forall prog prog' sp t nxt nxt' outgoing. Int -> SessionChain prog prog' (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') (Cons (Recv (sp, t)) nxt, outgoing, Cons t nxt') BoolSource
soffer :: forall current outgoing incoming finalResult prog prog' jumps. OfferImpls jumps prog prog' (current, outgoing, incoming) finalResult -> SessionChain prog prog' (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) finalResultSource
Offer a number of branches. This is basically an external choice - the other party uses sselect to decide which branch to take. Use OfferImpls in order to construct the list of implementations of branches. Note that every implementation must result in the same final state and emit the same value.
sselect :: forall prog prog' progOut progIn label jumps outgoing incoming current currentUX len jumpTarget. (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, TyListLength jumps len, SmallerThanBool label len True, TypeNumberToInt label, TyListIndex jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', TyListIndex progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), TyListIndex progIn jumpTarget (MVar (ProgramCell (Cell incoming))), TyListIndex prog jumpTarget currentUX, Expand prog currentUX current) => label -> SessionChain prog prog' (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (current, outgoing, incoming) ()Source
Select which branch we're taking at a branch point. Use a type number (Control.Concurrent.Session.Number) to indicate the branch to take.
run :: forall prog prog' progOut progIn init fromO fromI toO toI res res' currentUX currentUX' current current' toCur toCur'. (ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, SWellFormedConfig init (D0 E) prog, SWellFormedConfig init (D0 E) prog', TyListIndex progOut init (MVar (ProgramCell (Cell fromO))), TyListIndex progIn init (MVar (ProgramCell (Cell fromI))), DualT prog ~ prog', Dual prog prog', TyListIndex prog init currentUX, Expand prog currentUX current, TyListIndex prog' init currentUX', Expand prog' currentUX' current') => prog -> init -> SessionChain prog prog' (current, fromO, fromI) (toCur, toO, toI) res -> SessionChain prog' prog (current', fromI, fromO) (toCur', toI, toO) res' -> IO (res, res')Source
Run! Provide a program and a start point within that program (which is automatically sjumped to), the two implementations which must be duals of each other, run them, have them communicate, wait until they both finish and die and then return the results from both of them.
carefullySwapToNextCell :: MVar (ProgramCell a) -> IO (ProgramCell a)Source
Produced by Haddock version 2.4.2