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

Control.Concurrent.Session.Pid

Description

Defines what a Pid is and provides functionality to create new sessions channels to a given pid. Obviously this is safe/ in some way - in particular, a Pid carries about with it the set of Session Types it is willing to use. This means that you can't try to start any old Session Type with any given Pid. However, it doesn't mean that given an acceptable Session Type, the other thread will ever actually get around to agreeing to create the new session / channel with you.

Synopsis

makePid :: InternalPid prog prog' invertedSessionsO sessionsToIdxO idxsToPairStructsO -> invertedSessionsN -> TyMap sessionsToIdxN idxsToPairStructsN -> (InternalPid prog prog' invertedSessionsO sessionsToIdxO idxsToPairStructsO, InternalPid prog prog' invertedSessionsN sessionsToIdxN idxsToPairStructsN) rootPid :: (Dual prog prog', DualT prog ~ prog') => TyMap sessionsToIdx idxsToPairStructs -> invertedSessions -> prog -> InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs iPidToPid :: InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs -> Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs myPid :: InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) from from (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) class BuildPidTyMap prog stlst tymap | prog stlst -> tymap where type BuildPidTyMapT prog stlst buildPidTyMap :: prog -> stlst -> IO tymap class BuildInvertedSessionsSet stlist set | stlist -> set where type BuildInvertedSessionsSetT stlist buildInvertedSessionsSet :: stlist -> set class CreateSession invert init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem where createSession :: init -> invert -> Pid prog prog' invertedSessionsThem sessionsToIdxThem idxsToPairStructsThem -> InterleavedChain (InternalPid prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfThem class PidEq a b where (=~=) :: a -> b -> Bool data MultiReceiveList where MultiReceiveNil :: MultiReceiveList Nil prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res (~|||~) :: (MapLookup (TyMap keyToIdx idxToValue) ch (SessionState progS progS' (Cons cur nxt, fromO, Cons inc nxt')), RecvOrOffer cur inc nxt nxt') => (ch, InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res) -> MultiReceiveList chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res -> MultiReceiveList (Cons ch chs) prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res class MultiReceive lst chain | lst -> chain where multiReceive :: lst -> chain class PlainMultiReceive idxs pid mp mp' result where plainMultiReceive :: idxs -> [InterleavedChain pid mp mp' result] -> InterleavedChain pid mp mp' result class CombinedMultiRecv chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' idxs result where combinedMultiRecv :: MultiReceiveList chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' result -> idxs -> [InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result] -> InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result

Documentation

makePid :: InternalPid prog prog' invertedSessionsO sessionsToIdxO idxsToPairStructsO -> invertedSessionsN -> TyMap sessionsToIdxN idxsToPairStructsN -> (InternalPid prog prog' invertedSessionsO sessionsToIdxO idxsToPairStructsO, InternalPid prog prog' invertedSessionsN sessionsToIdxN idxsToPairStructsN) Source

rootPid :: (Dual prog prog', DualT prog ~ prog') => TyMap sessionsToIdx idxsToPairStructs -> invertedSessions -> prog -> InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs Source

iPidToPid :: InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs -> Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs Source

myPid :: InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) from from (Pid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) Source

class BuildPidTyMap prog stlst tymap | prog stlst -> tymap where Source

Associated Types type BuildPidTyMapT prog stlst Source Methods buildPidTyMap :: prog -> stlst -> IO tymap Source

class BuildInvertedSessionsSet stlist set | stlist -> set where Source

Associated Types type BuildInvertedSessionsSetT stlist Source Methods buildInvertedSessionsSet :: stlist -> set Source Instances BuildInvertedSessionsSet Nil Nil BuildInvertedSessionsSet nxt set => BuildInvertedSessionsSet (Cons ((,) init False) nxt) set (BuildInvertedSessionsSet nxt set, TyList set) => BuildInvertedSessionsSet (Cons ((,) init True) nxt) (Cons init set)

class CreateSession invert init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem where Source

Provides the ability to make a new session / channel with the given Pid. Supply the index to the Session Type, whether or not you're locally inverting (dualing) the Session Type, and the Pid, and so long as the Pid supports the dual of your local Session Type, this will block until the Pid gets around to servicing you. Thus this is a synchronous operation and both Pids must know of each other to create a new session / channel between them. Methods createSession :: init -> invert -> Pid prog prog' invertedSessionsThem sessionsToIdxThem idxsToPairStructsThem -> InterleavedChain (InternalPid prog prog' invertedSessionsMe sessionsToIdxMe idxsToPairStructsMe) (TyMap keyToIdxMe idxToValueMe) (TyMap keyToIdxMe' idxToValueMe') idxOfThem Source Instances (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))), TyListIndex prog init current', Expand prog current' current, MapLookup (TyMap sessionsToIdxMe idxsToPairStructsMe) init (MVar (Map ((,) RawPid RawPid) (MVar (PairStruct init prog prog' ((,,) (Cons (Jump init) Nil) (Cons (Jump init) Nil) (Cons (Jump init) Nil)))))), TyListMember invertedSessionsThem init True, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog prog' ((,,) current fromO fromI)) (TyMap keyToIdxMe' idxToValueMe')) => CreateSession False init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem (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, Expand prog currentUX current, TyListIndex prog' init currentUX', Expand prog' currentUX' current', MapLookup (TyMap sessionsToIdxThem idxsToPairStructsThem) init (MVar (Map ((,) RawPid RawPid) (MVar (PairStruct init prog prog' ((,,) (Cons (Jump init) Nil) (Cons (Jump init) Nil) (Cons (Jump init) Nil)))))), TyListMember invertedSessionsMe init True, MapSize (TyMap keyToIdxMe idxToValueMe) idxOfThem, MapInsert (TyMap keyToIdxMe idxToValueMe) idxOfThem (SessionState prog' prog ((,,) current' fromI fromO)) (TyMap keyToIdxMe' idxToValueMe')) => CreateSession True init prog prog' sessionsToIdxMe sessionsToIdxThem idxsToPairStructsMe idxsToPairStructsThem keyToIdxMe idxToValueMe keyToIdxMe' idxToValueMe' idxOfThem invertedSessionsMe invertedSessionsThem

class PidEq a b where Source

Provides a way to compare two Pids. Of course, if the Pids have different type params, then they are definitely different, but it's still convenient to be able to do something like (==) on them. Methods (=~=) :: a -> b -> Bool Source Instances PidEq (Pid progA progA' invertedSessionsA sessionsToIdxA idxsToPairStructsA) (Pid progB progB' invertedSessionsB sessionsToIdxB idxsToPairStructsB)

data MultiReceiveList where Source

Constructors MultiReceiveNil :: MultiReceiveList Nil prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res Instances (TyListLength chs len, SmallerThanBool (D0 E) len True, SetIncomingNotify (TyMap keyToIdx idxToValue) chs, TypeNumberToInt len) => MultiReceive (MultiReceiveList chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res) (InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res)

(~|||~) :: (MapLookup (TyMap keyToIdx idxToValue) ch (SessionState progS progS' (Cons cur nxt, fromO, Cons inc nxt')), RecvOrOffer cur inc nxt nxt') => (ch, InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res) -> MultiReceiveList chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res -> MultiReceiveList (Cons ch chs) prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res Source

class MultiReceive lst chain | lst -> chain where Source

Methods multiReceive :: lst -> chain Source Instances MultiReceive ([] ((,) (SessionState prog'' prog''' from) (InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result))) (InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result) MultiReceive ([] ((,) (SessionState prog'' prog''' from) (InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result))) (InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result) (TyListLength chs len, SmallerThanBool (D0 E) len True, SetIncomingNotify (TyMap keyToIdx idxToValue) chs, TypeNumberToInt len) => MultiReceive (MultiReceiveList chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res) (InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res) (TyListLength chs len, SmallerThanBool (D0 E) len True, SetIncomingNotify (TyMap keyToIdx idxToValue) chs, TypeNumberToInt len) => MultiReceive (MultiReceiveList chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' res) (InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') res)

class PlainMultiReceive idxs pid mp mp' result where Source

Methods plainMultiReceive :: idxs -> [InterleavedChain pid mp mp' result] -> InterleavedChain pid mp mp' result Source Instances (MapSelectToList (TyMap keyToIdx idxToValue) idxs sessions, TyListToList sessions ([] (SessionState prog'' prog''' from)), MultiReceive ([] ((,) (SessionState prog'' prog''' from) (InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result))) (InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result)) => PlainMultiReceive idxs (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result (MapSelectToList (TyMap keyToIdx idxToValue) idxs sessions, TyListToList sessions ([] (SessionState prog'' prog''' from)), MultiReceive ([] ((,) (SessionState prog'' prog''' from) (InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result))) (InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result)) => PlainMultiReceive idxs (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result

class CombinedMultiRecv chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' idxs result where Source

Methods combinedMultiRecv :: MultiReceiveList chs prog prog' invertedSessions sessionsToIdx idxsToPairStructs keyToIdx idxToValue keyToIdx' idxToValue' result -> idxs -> [InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result] -> InterleavedChain (InternalPid prog prog' invertedSessions sessionsToIdx idxsToPairStructs) (TyMap keyToIdx idxToValue) (TyMap keyToIdx' idxToValue') result Source

Produced by Haddock version 2.4.2