sessions-2008.3.25: Session Types for Haskell Source code Contents Index

Control.Concurrent.Session.Interleaving

Description

A single thread should be able to have multiple concurrent conversations with other threads. So this module places InterleavedChain as an instance of SMonad, and equipts it with the capability to manage and modify a mapping of channels to other threads. Note there is some danger in here. Deadlocks can start to appear if you're silly or deliberately mean. However, this is starting to get towards the Actor / Erlang model of message passing.

Synopsis

withChannel :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, fromO, fromI)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current', toO, toI)) (TyMap keyToIdx idxToValue')) => idx -> SessionChain prog prog' (current, fromO, fromI) (current', toO, toI) res -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') res class Fork invert init sessionsList prog prog' sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild current current' currentUX currentUX' where fork :: init -> invert -> sessionsList -> (D0 E -> Pid prog sessionsToIdxMe idxsToPairStructsMe -> InterleavedChain (InternalPid prog sessionsToIdxThem idxsToPairStructsThem) (TyMap keyToIdxChild' idxToValueChild') (TyMap keyToIdxChild'' idxToValueChild'') ()) -> InterleavedChain (InternalPid prog sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') (idxOfChild, Pid prog sessionsToIdxThem idxsToPairStructsThem) runInterleaved :: (BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdx idxsToPairStructs), TyListSortNums sessionsList sessionsListSorted) => sessionsList -> prog -> InterleavedChain (InternalPid prog sessionsToIdx idxsToPairStructs) (TyMap Nil Nil) (TyMap keyToIdx idxToValue) res -> IO res sjumpCh :: (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 current', ExpandPids prog current' current, MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Jump l) Nil, Cons (Jump l) Nil, Cons (Jump l) Nil)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, outgoing, incoming)) (TyMap keyToIdx idxToValue')) => idx -> InterleavedChain (InternalPid prog sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') () ssendCh :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Send t) nxt, Cons t nxt', incoming)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (nxt, nxt', incoming)) (TyMap keyToIdx idxToValue')) => idx -> t -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') () srecvCh :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Recv t) nxt, outgoing, Cons t nxt')), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (nxt, outgoing, nxt')) (TyMap keyToIdx idxToValue')) => idx -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') t sofferCh :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, outgoing, incoming)) (TyMap keyToIdx idxToValue')) => idx -> OfferImpls jumps prog prog' (current, outgoing, incoming) finalResult -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') finalResult sselectCh :: (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, outgoing, incoming)) (TyMap keyToIdx idxToValue'), TyListLength jumps len, SmallerThan label len, 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, ExpandPids prog currentUX current) => idx -> label -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') ()

Documentation

withChannel :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, fromO, fromI)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current', toO, toI)) (TyMap keyToIdx idxToValue')) => idx -> SessionChain prog prog' (current, fromO, fromI) (current', toO, toI) res -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') res Source

Perform the given actions on the given channel. Note that the value emitted by the actions will be passed out.

class Fork invert init sessionsList prog prog' sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild current current' currentUX currentUX' where Source

Think of this as spawn or fork - it creates a child thread which must be prepared to communicate with you. You get a channel set up to the child which is emitted by this function. The child is first told about the channel back to you and your Pid. The child can go off and do what ever it wants, including creating additional channels. The child starts off knowing with only one open channel which is to the parent. Methods fork :: init -> invert -> sessionsList -> (D0 E -> Pid prog sessionsToIdxMe idxsToPairStructsMe -> InterleavedChain (InternalPid prog sessionsToIdxThem idxsToPairStructsThem) (TyMap keyToIdxChild' idxToValueChild') (TyMap keyToIdxChild'' idxToValueChild'') ()) -> InterleavedChain (InternalPid prog sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') (idxOfChild, Pid prog sessionsToIdxThem idxsToPairStructsThem) Source Instances (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing 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))), TyListIndex prog init currentUX, TyListIndex prog' init currentUX', ExpandPids prog currentUX current, ExpandPids prog' currentUX' current', BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdxThem idxsToPairStructsThem), TyListSortNums sessionsList sessionsListSorted, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild (SessionState prog prog' ((,,) current fromO fromI)) (TyMap keyToIdxMe' idxToValueMe'), MapInsert (TyMap Nil Nil) (D0 E) (SessionState prog' prog ((,,) current' fromI fromO)) (TyMap keyToIdxChild' idxToValueChild'), Dual prog prog') => Fork False init sessionsList prog prog' sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild current current' currentUX currentUX' (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing 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))), TyListIndex prog init currentUX, TyListIndex prog' init currentUX', ExpandPids prog currentUX current, ExpandPids prog' currentUX' current', BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdxThem idxsToPairStructsThem), TyListSortNums sessionsList sessionsListSorted, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfChild, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfChild (SessionState prog' prog ((,,) current' fromI fromO)) (TyMap keyToIdxMe' idxToValueMe'), MapInsert (TyMap Nil Nil) (D0 E) (SessionState prog prog' ((,,) current fromO fromI)) (TyMap keyToIdxChild' idxToValueChild'), Dual prog prog') => Fork True init sessionsList prog prog' sessionsToIdxThem idxsToPairStructsThem sessionsToIdxMe idxsToPairStructsMe fromO fromI progOut progIn keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' keyToIdxChild' idxToValueChild' keyToIdxChild'' idxToValueChild'' idxOfChild current current' currentUX currentUX'

runInterleaved :: (BuildPidTyMap prog sessionsListSorted (TyMap sessionsToIdx idxsToPairStructs), TyListSortNums sessionsList sessionsListSorted) => sessionsList -> prog -> InterleavedChain (InternalPid prog sessionsToIdx idxsToPairStructs) (TyMap Nil Nil) (TyMap keyToIdx idxToValue) res -> IO res Source

Run the root. Use this to start up a family from a single root.

sjumpCh :: (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 current', ExpandPids prog current' current, MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Jump l) Nil, Cons (Jump l) Nil, Cons (Jump l) Nil)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, outgoing, incoming)) (TyMap keyToIdx idxToValue')) => idx -> InterleavedChain (InternalPid prog sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') () Source

Convenience combination of withChannel and sjump

ssendCh :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Send t) nxt, Cons t nxt', incoming)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (nxt, nxt', incoming)) (TyMap keyToIdx idxToValue')) => idx -> t -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') () Source

Convenience combination of withChannel and ssend

srecvCh :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Recv t) nxt, outgoing, Cons t nxt')), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (nxt, outgoing, nxt')) (TyMap keyToIdx idxToValue')) => idx -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') t Source

Convenience combination of withChannel and srecv

sofferCh :: (MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Offer jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, outgoing, incoming)) (TyMap keyToIdx idxToValue')) => idx -> OfferImpls jumps prog prog' (current, outgoing, incoming) finalResult -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') finalResult Source

Convenience combination of withChannel and soffer

sselectCh :: (ProgramToMVarsOutgoingT prog prog ~ progOut, ProgramToMVarsOutgoingT prog' prog' ~ progIn, ProgramToMVarsOutgoing prog prog progOut, ProgramToMVarsOutgoing prog' prog' progIn, MapLookup (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (Cons (Select jumps) Nil, Cons (Choice jumps) Nil, Cons (Choice jumps) Nil)), MapUpdate (TyMap keyToIdx idxToValue) idx (SessionState prog prog' (current, outgoing, incoming)) (TyMap keyToIdx idxToValue'), TyListLength jumps len, SmallerThan label len, 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, ExpandPids prog currentUX current) => idx -> label -> InterleavedChain (InternalPid pidProg sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx idxToValue') () Source

Convenience combination of withChannel and sselectCh

Produced by Haddock version 2.3.0