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

Control.Concurrent.Session.SessionTypeMonad

Documentation

data TypeState where Source

Constructors TypeState :: nxtLabel -> declareable -> useable -> st -> TypeState nxtLabel declareable useable st

newtype SessionType f t r Source

Constructors SessionType buildSessionType :: f -> (r, t) Instances SMonad SessionType BuildBranches (BranchesList resLst labs (TypeState nxtLabel' declareable' useable' st') to finalTo) (SessionType (TypeState nxtLabel' declareable' useable' st') finalTo ((,) resLst labs)) => BuildBranches (BranchesList (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs) (TypeState nxtLabel declareable useable st) ((,) (TypeState nxtLabel' declareable' useable' st') to) finalTo) (SessionType (TypeState nxtLabel declareable useable st) finalTo ((,) (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs))) BuildBranches (BranchesList Nil Nil (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st)) (SessionType (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) ((,) Nil Nil))

newLabel :: (Succ nxtLabel nxtLabel', TyListConsSet nxtLabel declareable declareable', TyListConsSet nxtLabel useable useable') => SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable' useable' st) nxtLabel Source

declareLabel :: (TyListMember declareable label True, TyListElem declareable label idx, TyListDelete declareable idx declareable', TyList st) => label -> SessionType (TypeState nxtLabel declareable' useable (Cons (label, Nil) st)) (TypeState nxtLabel' declareable'' useable' st') a -> SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable'' useable' st') a Source

(.=) :: (TyListMember declareable label True, TyListElem declareable label idx, TyListDelete declareable idx declareable', TyList st) => label -> SessionType (TypeState nxtLabel declareable' useable (Cons (label, Nil) st)) (TypeState nxtLabel' declareable'' useable' st') a -> SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable'' useable' st') a Source

send :: (TyList f, TyList fs) => t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (Send (SpecialNormal, t)) f) fs)) () Source

recv :: (TyList f, TyList fs) => t -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (Recv (SpecialNormal, t)) f) fs)) () Source

sendPid :: (TyList f, TyList fs, TyListSortNums lst lst') => lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (SendPid False lst') f) fs)) () Source

recvPid :: (TyList f, TyList fs, TyListSortNums lst lst') => lst -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, Cons (RecvPid False lst') f) fs)) () Source

sendSession :: (TyList f, TyList fs, TyList fs', TyListReverse frag fragRev, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil), TyListDrop (D1 E) fragRev fragTailRev, TyListReverse fragTailRev fragTail, TyListAppend fragTail fs fs') => SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil)) (TypeState nxtLabel' declareable' useable' frag) res -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel' declareable' useable' (Cons (label, Cons (SendSession False fragHead) f) fs')) res Source

recvSession :: (TyList f, TyList fs, TyList fs', TyListReverse frag fragRev, TyListTake (D1 E) fragRev (Cons (label, fragHead) Nil), TyListDrop (D1 E) fragRev fragTailRev, TyListReverse fragTailRev fragTail, TyListAppend fragTail fs fs') => SessionType (TypeState nxtLabel declareable useable (Cons (label, Nil) Nil)) (TypeState nxtLabel' declareable' useable' frag) res -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel' declareable' useable' (Cons (label, Cons (RecvSession False fragHead) f) fs')) res Source

end :: (TyListReverse (Cons End f) f', TyList f, TyList fs) => SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f') fs)) () Source

jump :: (TyListReverse (Cons (Jump jt) f) f', TyList f, TyList fs, TyListMember useable jt True) => jt -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f') fs)) () Source

data BranchesList where Source

Constructors BLNil :: BranchesList Nil Nil z z z BLCons :: SessionType (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable' useable' st') (resLst -> Cons res resLst, labs -> Cons (Cons (Jump nxtLabel) Nil) labs) -> BranchesList resLst labs (TypeState nxtLabel' declareable' useable' st') to finalTo -> BranchesList (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs) (TypeState nxtLabel declareable useable st) (TypeState nxtLabel' declareable' useable' st', to) finalTo Instances BuildBranches (BranchesList resLst labs (TypeState nxtLabel' declareable' useable' st') to finalTo) (SessionType (TypeState nxtLabel' declareable' useable' st') finalTo ((,) resLst labs)) => BuildBranches (BranchesList (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs) (TypeState nxtLabel declareable useable st) ((,) (TypeState nxtLabel' declareable' useable' st') to) finalTo) (SessionType (TypeState nxtLabel declareable useable st) finalTo ((,) (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs))) BuildBranches (BranchesList Nil Nil (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st)) (SessionType (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) ((,) Nil Nil))

(~|~) :: (Succ label nxtLabel, TyListConsSet label declareable declareable', TyListElem declareable' label idx, TyListDelete declareable' idx declareable'', TyListConsSet label useable useable', TyList st, TyListMember declareable' label True, TyList labs, TyList resLst) => SessionType (TypeState nxtLabel declareable'' useable' (Cons (label, Nil) st)) (TypeState nxtLabel' declareable''' useable'' st') res -> BranchesList resLst labs (TypeState nxtLabel' declareable''' useable'' st') to finalTo -> BranchesList (Cons res resLst) (Cons (Cons (Jump label) Nil) labs) (TypeState label declareable useable st) (TypeState nxtLabel' declareable''' useable'' st', to) finalTo Source

class BuildBranches bl st where Source

Methods buildBranches :: bl -> st Source Instances BuildBranches (BranchesList resLst labs (TypeState nxtLabel' declareable' useable' st') to finalTo) (SessionType (TypeState nxtLabel' declareable' useable' st') finalTo ((,) resLst labs)) => BuildBranches (BranchesList (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs) (TypeState nxtLabel declareable useable st) ((,) (TypeState nxtLabel' declareable' useable' st') to) finalTo) (SessionType (TypeState nxtLabel declareable useable st) finalTo ((,) (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs))) BuildBranches (BranchesList resLst labs (TypeState nxtLabel' declareable' useable' st') to finalTo) (SessionType (TypeState nxtLabel' declareable' useable' st') finalTo ((,) resLst labs)) => BuildBranches (BranchesList (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs) (TypeState nxtLabel declareable useable st) ((,) (TypeState nxtLabel' declareable' useable' st') to) finalTo) (SessionType (TypeState nxtLabel declareable useable st) finalTo ((,) (Cons res resLst) (Cons (Cons (Jump nxtLabel) Nil) labs))) BuildBranches (BranchesList Nil Nil (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st)) (SessionType (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) ((,) Nil Nil)) BuildBranches (BranchesList Nil Nil (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st)) (SessionType (TypeState nxtLabel declareLabel useable st) (TypeState nxtLabel declareLabel useable st) ((,) Nil Nil))

select :: forall f f' fs listOfRes listOfJumps label nxtLabel declareable useable to finalTo. (TyListReverse (Cons (Select listOfJumps) f) f', TyList f, TyList fs, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) (SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))) => BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfRes Source

offer :: forall f f' fs listOfRes listOfJumps label nxtLabel declareable useable to finalTo. (TyListReverse (Cons (Offer listOfJumps) f) f', TyList f, TyList fs, BuildBranches (BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo) (SessionType (TypeState nxtLabel declareable useable (Cons (label, f') fs)) finalTo (listOfRes, listOfJumps))) => BranchesList listOfRes listOfJumps (TypeState nxtLabel declareable useable (Cons (label, f') fs)) to finalTo -> SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) finalTo listOfRes Source

currentLabel :: SessionType (TypeState nxtLabel declareable useable (Cons (label, f) fs)) (TypeState nxtLabel declareable useable (Cons (label, f) fs)) label Source

makeSessionType :: (TyListSortNums st st', TyListSnd st' st'') => SessionType (TypeState (D0 E) Nil Nil Nil) (TypeState nxtLabel Nil useable st) res -> (st'', res) Source

class TyListSnd lstA lstB | lstA -> lstB where Source

Methods tyListSnd :: lstA -> lstB Source Instances TyListSnd Nil Nil (TyListSnd nxt nxt', TyList nxt, TyList nxt') => TyListSnd (Cons ((,) a b) nxt) (Cons b nxt')

dual :: True Source

notDual :: False Source

Produced by Haddock version 2.4.2