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

Control.Concurrent.Session

Description

This is just a convenience module that reexports everything you're expected to need.

Synopsis

data OfferImpls where OfferImplsNil :: OfferImpls Nil prog progOut progIn finalState finalResult (~||~) :: forall prog prog' progOut progIn outgoing incoming finalState finalResult jumps l. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing 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)))) => SessionChain prog progOut progIn (outgoing, incoming) finalState finalResult -> OfferImpls jumps prog progOut progIn finalState finalResult -> OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog progOut progIn finalState finalResult sjump :: forall l prog prog' progOut progIn outgoing incoming. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing 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)))) => SessionChain prog progOut progIn (Cons (Jump l) Nil, Cons (Jump l) Nil) (outgoing, incoming) () soffer :: forall outgoing incoming finalResult prog prog' progOut progIn jumps. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => OfferImpls jumps prog progOut progIn (outgoing, incoming) finalResult -> SessionChain prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (outgoing, incoming) finalResult sselect :: forall prog prog' progOut progIn label jumps outgoing incoming len jumpTarget. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, 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)))) => label -> SessionChain prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (outgoing, incoming) () ssend :: forall t prog prog' progOut progIn nxt incoming. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => t -> SessionChain prog progOut progIn (Cons t nxt, incoming) (nxt, incoming) () srecv :: forall t prog prog' progOut progIn nxt outgoing. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => SessionChain prog progOut progIn (outgoing, Cons t nxt) (outgoing, nxt) t run :: forall prog prog' progOut progIn init fromO fromI toO toI toO' toI' res res'. (Dual prog prog', Dual prog' prog, ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing 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)))) => prog -> init -> SessionChain prog progOut progIn (fromO, fromI) (toO, toI) res -> SessionChain prog' progIn progOut (fromI, fromO) (toO', toI') res' -> IO (res, res') data End data Send where Send :: t -> Send t SendInt :: Send Int SendBool :: Send Bool SendChar :: Send Char SendStr :: Send String SendDouble :: Send Double data Recv where Recv :: t -> Recv t RecvInt :: Recv Int RecvBool :: Recv Bool RecvChar :: Recv Char RecvStr :: Recv String RecvDouble :: Recv Double data Jump l data Select data Offer jump :: TyNum n => n -> Cons (Jump n) Nil end :: Cons End Nil select :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Select (Cons val nxt)) Nil offer :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Offer (Cons val nxt)) Nil class Dual a b | a -> b, b -> a where dual :: a -> b (~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> Cons a nxt (~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxt class SWellFormedConfig idxA idxB ss testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> Bool data Cons cons :: TyList n => t -> n -> Cons t n data Nil nil :: Nil data E = E data D0 n = D0 n data D1 n = D1 n data D2 n = D2 n data D3 n = D3 n data D4 n = D4 n data D5 n = D5 n data D6 n = D6 n data D7 n = D7 n data D8 n = D8 n data D9 n = D9 n module Control.Concurrent.Session.SMonad emptyMap :: TyMap Nil Nil module Control.Concurrent.Session.Interleaving

Documentation

data OfferImpls where Source

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 progOut progIn finalState finalResult

(~||~) :: forall prog prog' progOut progIn outgoing incoming finalState finalResult jumps l. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing 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)))) => SessionChain prog progOut progIn (outgoing, incoming) finalState finalResult -> OfferImpls jumps prog progOut progIn finalState finalResult -> OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog progOut progIn finalState finalResult Source

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. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing 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)))) => SessionChain prog progOut progIn (Cons (Jump l) Nil, Cons (Jump l) Nil) (outgoing, incoming) () Source

Perform a jump. Now you may think that you should indicate where you want to jump to. But of coures, that's actually specified by the session type so you don't have to specify it at all in the implementation.

soffer :: forall outgoing incoming finalResult prog prog' progOut progIn jumps. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => OfferImpls jumps prog progOut progIn (outgoing, incoming) finalResult -> SessionChain prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (outgoing, incoming) finalResult Source

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 len jumpTarget. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, 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)))) => label -> SessionChain prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) (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.

ssend :: forall t prog prog' progOut progIn nxt incoming. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => t -> SessionChain prog progOut progIn (Cons t nxt, incoming) (nxt, incoming) () Source

Send a value to the other party. Of course, the value must be of the correct type indicated in the session type.

srecv :: forall t prog prog' progOut progIn nxt outgoing. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => SessionChain prog progOut progIn (outgoing, Cons t nxt) (outgoing, nxt) t Source

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.

run :: forall prog prog' progOut progIn init fromO fromI toO toI toO' toI' res res'. (Dual prog prog', Dual prog' prog, ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing 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)))) => prog -> init -> SessionChain prog progOut progIn (fromO, fromI) (toO, toI) res -> SessionChain prog' progIn progOut (fromI, fromO) (toO', toI') 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.

data End Source

Instances Show End STerminal End SNoJumpsBeyond End idx Dual End End

data Send where Source

Constructors Send :: t -> Send t SendInt :: Send Int SendBool :: Send Bool SendChar :: Send Char SendStr :: Send String SendDouble :: Send Double Instances SNonTerminal (Send t) SNoJumpsBeyond (Send t) idx Dual (Recv t) (Send t) Dual (Send t) (Recv t)

data Recv where Source

Constructors Recv :: t -> Recv t RecvInt :: Recv Int RecvBool :: Recv Bool RecvChar :: Recv Char RecvStr :: Recv String RecvDouble :: Recv Double Instances SNonTerminal (Recv t) SNoJumpsBeyond (Recv t) idx Dual (Recv t) (Send t) Dual (Send t) (Recv t)

data Jump l Source

Instances Show l => Show (Jump l) TyNum l => STerminal (Jump l) SmallerThan l idx => SNoJumpsBeyond (Jump l) idx Dual (Jump l) (Jump l)

data Select Source

Instances SListOfJumps (Cons val nxt) => STerminal (Select (Cons val nxt)) SNoJumpsBeyond lol idx => SNoJumpsBeyond (Select lol) idx Dual (Offer lst) (Select lst) Dual (Select lst) (Offer lst)

data Offer Source

Instances SListOfJumps (Cons val nxt) => STerminal (Offer (Cons val nxt)) SNoJumpsBeyond lol idx => SNoJumpsBeyond (Offer lol) idx Dual (Offer lst) (Select lst) Dual (Select lst) (Offer lst)

jump :: TyNum n => n -> Cons (Jump n) Nil Source

end :: Cons End Nil Source

select :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Select (Cons val nxt)) Nil Source

offer :: SListOfJumps (Cons val nxt) => Cons val nxt -> Cons (Offer (Cons val nxt)) Nil Source

class Dual a b | a -> b, b -> a where Source

Methods dual :: a -> b Source Instances Dual Nil Nil Dual End End Dual (Offer lst) (Select lst) Dual (Offer lst) (Select lst) Dual (Select lst) (Offer lst) Dual (Select lst) (Offer lst) Dual (Jump l) (Jump l) Dual (Recv t) (Send t) Dual (Recv t) (Send t) Dual (Send t) (Recv t) Dual (Send t) (Recv t) (TyList nxt, TyList nxt', Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')

(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> Cons a nxt Source

(~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxt Source

class SWellFormedConfig idxA idxB ss Source

testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> Bool Source

data Cons Source

Instances (TyListDrop cnt' nxt lst, Pred cnt cnt') => TyListDrop cnt (Cons val nxt) lst TyListTake (D0 E) (Cons val nxt) Nil (TyListTake cnt' nxt nxt', Pred (D9 r) cnt') => TyListTake (D9 r) (Cons val nxt) (Cons val nxt') (TyListTake cnt' nxt nxt', Pred (D8 r) cnt') => TyListTake (D8 r) (Cons val nxt) (Cons val nxt') (TyListTake cnt' nxt nxt', Pred (D7 r) cnt') => TyListTake (D7 r) (Cons val nxt) (Cons val nxt') (TyListTake cnt' nxt nxt', Pred (D6 r) cnt') => TyListTake (D6 r) (Cons val nxt) (Cons val nxt') (TyListTake cnt' nxt nxt', Pred (D5 r) cnt') => TyListTake (D5 r) (Cons val nxt) (Cons val nxt') (TyListTake cnt' nxt nxt', Pred (D4 r) cnt') => TyListTake (D4 r) (Cons val nxt) (Cons val nxt') (TyListTake cnt' nxt nxt', Pred (D3 r) cnt') => TyListTake (D3 r) (Cons val nxt) (Cons val nxt') (TyListTake cnt' nxt nxt', Pred (D2 r) cnt') => TyListTake (D2 r) (Cons val nxt) (Cons val nxt') (TyListTake cnt' nxt nxt', Pred (D1 r) cnt') => TyListTake (D1 r) (Cons val nxt) (Cons val nxt') TyListDrop (D0 E) (Cons val nxt) (Cons val nxt) (TyListLength n l, Succ l l', Show n, Show t) => Show (Cons t n) TyList nxt => TyList (Cons val nxt) (SValidSessionType nxt, SNonTerminal val) => SValidSessionType (Cons val nxt) STerminal a => SValidSessionType (Cons a Nil) (SValidSessionType val, SListOfSessionTypes nxt) => SListOfSessionTypes (Cons val nxt) (SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt) (TyListLength n len, Succ len len') => TyListLength (Cons t n) len' (OnlyOutgoing nxt nxt', TyList nxt, TyList nxt') => OnlyOutgoing (Cons (Recv t) nxt) nxt' (SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx (TyListReverse' nxt (Cons v acc) n, TyList acc) => TyListReverse' (Cons v nxt) acc n (TyListIndex nxt idx' res, Pred idx idx', SmallerThan idx' len, TyListLength nxt len) => TyListIndex (Cons val nxt) idx res (Succ acc acc', TyListElem' nxt acc' val idx) => TyListElem' (Cons val' nxt) acc val idx TyListElem' (Cons val nxt) idx val idx TyListAppend nxt b nxt' => TyListAppend (Cons val nxt) b (Cons val nxt') TyListIndex (Cons res nxt) (D0 E) res OnlyOutgoing (Cons (Offer jl) Nil) (Cons (Choice jl) Nil) OnlyOutgoing (Cons (Select jl) Nil) (Cons (Choice jl) Nil) OnlyOutgoing (Cons (Jump l) Nil) (Cons (Jump l) Nil) (OnlyOutgoing nxt nxt', TyList nxt, TyList nxt') => OnlyOutgoing (Cons (Send t) nxt) (Cons t nxt') OnlyOutgoing (Cons End Nil) (Cons End Nil) (TyList nxt, TyList nxt', Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt') (ProgramToMVarsOutgoing nxt nxt', OnlyOutgoing val val', TyList nxt, TyList nxt') => ProgramToMVarsOutgoing (Cons val nxt) (Cons (MVar (ProgramCell (Cell val'))) nxt')

cons :: TyList n => t -> n -> Cons t n Source

data Nil Source

Instances Show Nil TyList Nil SListOfSessionTypes Nil SListOfJumps Nil SNoJumpsBeyond Nil idx Dual Nil Nil ProgramToMVarsOutgoing Nil Nil TyListReverse' Nil acc acc TyListDrop cnt Nil Nil TyListAppend Nil b b TyListElem' Nil acc val idx TyListLength Nil (D0 E) TyListTake (D0 E) Nil Nil TyListTake (D0 E) (Cons val nxt) Nil

nil :: Nil Source

data E Source

Constructors E Instances Show E Reverse' E a a IncrementRightToLeft E (D1 E)

data D0 n Source

Constructors D0 n Instances TyListLength Nil (D0 E) Pred m m' => Add m (D0 E) m Show n => Show (D0 n) TypeNumberToInt (D0 E) TyNum n => TyNum (D0 n) TyNum (D0 E) Pred y y' => SmallerThan (D0 E) y StripLeadingZeros a b => StripLeadingZeros (D0 a) b Pred n n' => Add (D0 E) n n Reverse' n (D0 a) r => Reverse' (D0 n) a r TyListTake (D0 E) Nil Nil StripLeadingZeros (D0 E) (D0 E) DecrementRightToLeft (D1 a) (D0 a) DecrementRightToLeft a b => DecrementRightToLeft (D0 a) (D9 b) IncrementRightToLeft a b => IncrementRightToLeft (D9 a) (D0 b) IncrementRightToLeft (D0 a) (D1 a) Add (D0 E) (D0 E) (D0 E) TyListTake (D0 E) (Cons val nxt) Nil TyListDrop (D0 E) (Cons val nxt) (Cons val nxt) TyListIndex (Cons res nxt) (D0 E) res

data D1 n Source

Constructors D1 n Instances IncrementRightToLeft E (D1 E) Show n => Show (D1 n) TyNum n => TyNum (D1 n) TyNum (D1 E) Reverse' n (D1 a) r => Reverse' (D1 n) a r StripLeadingZeros (D1 a) (D1 a) DecrementRightToLeft (D2 a) (D1 a) DecrementRightToLeft (D1 a) (D0 a) IncrementRightToLeft (D1 a) (D2 a) IncrementRightToLeft (D0 a) (D1 a) (TyListTake cnt' nxt nxt', Pred (D1 r) cnt') => TyListTake (D1 r) (Cons val nxt) (Cons val nxt')

data D2 n Source

Constructors D2 n Instances Show n => Show (D2 n) TyNum n => TyNum (D2 n) TyNum (D2 E) Reverse' n (D2 a) r => Reverse' (D2 n) a r StripLeadingZeros (D2 a) (D2 a) DecrementRightToLeft (D3 a) (D2 a) DecrementRightToLeft (D2 a) (D1 a) IncrementRightToLeft (D2 a) (D3 a) IncrementRightToLeft (D1 a) (D2 a) (TyListTake cnt' nxt nxt', Pred (D2 r) cnt') => TyListTake (D2 r) (Cons val nxt) (Cons val nxt')

data D3 n Source

Constructors D3 n Instances Show n => Show (D3 n) TyNum n => TyNum (D3 n) TyNum (D3 E) Reverse' n (D3 a) r => Reverse' (D3 n) a r StripLeadingZeros (D3 a) (D3 a) DecrementRightToLeft (D4 a) (D3 a) DecrementRightToLeft (D3 a) (D2 a) IncrementRightToLeft (D3 a) (D4 a) IncrementRightToLeft (D2 a) (D3 a) (TyListTake cnt' nxt nxt', Pred (D3 r) cnt') => TyListTake (D3 r) (Cons val nxt) (Cons val nxt')

data D4 n Source

Constructors D4 n Instances Show n => Show (D4 n) TyNum n => TyNum (D4 n) TyNum (D4 E) Reverse' n (D4 a) r => Reverse' (D4 n) a r StripLeadingZeros (D4 a) (D4 a) DecrementRightToLeft (D5 a) (D4 a) DecrementRightToLeft (D4 a) (D3 a) IncrementRightToLeft (D4 a) (D5 a) IncrementRightToLeft (D3 a) (D4 a) (TyListTake cnt' nxt nxt', Pred (D4 r) cnt') => TyListTake (D4 r) (Cons val nxt) (Cons val nxt')

data D5 n Source

Constructors D5 n Instances Show n => Show (D5 n) TyNum n => TyNum (D5 n) TyNum (D5 E) Reverse' n (D5 a) r => Reverse' (D5 n) a r StripLeadingZeros (D5 a) (D5 a) DecrementRightToLeft (D6 a) (D5 a) DecrementRightToLeft (D5 a) (D4 a) IncrementRightToLeft (D5 a) (D6 a) IncrementRightToLeft (D4 a) (D5 a) (TyListTake cnt' nxt nxt', Pred (D5 r) cnt') => TyListTake (D5 r) (Cons val nxt) (Cons val nxt')

data D6 n Source

Constructors D6 n Instances Show n => Show (D6 n) TyNum n => TyNum (D6 n) TyNum (D6 E) Reverse' n (D6 a) r => Reverse' (D6 n) a r StripLeadingZeros (D6 a) (D6 a) DecrementRightToLeft (D7 a) (D6 a) DecrementRightToLeft (D6 a) (D5 a) IncrementRightToLeft (D6 a) (D7 a) IncrementRightToLeft (D5 a) (D6 a) (TyListTake cnt' nxt nxt', Pred (D6 r) cnt') => TyListTake (D6 r) (Cons val nxt) (Cons val nxt')

data D7 n Source

Constructors D7 n Instances Show n => Show (D7 n) TyNum n => TyNum (D7 n) TyNum (D7 E) Reverse' n (D7 a) r => Reverse' (D7 n) a r StripLeadingZeros (D7 a) (D7 a) DecrementRightToLeft (D8 a) (D7 a) DecrementRightToLeft (D7 a) (D6 a) IncrementRightToLeft (D7 a) (D8 a) IncrementRightToLeft (D6 a) (D7 a) (TyListTake cnt' nxt nxt', Pred (D7 r) cnt') => TyListTake (D7 r) (Cons val nxt) (Cons val nxt')

data D8 n Source

Constructors D8 n Instances Show n => Show (D8 n) TyNum n => TyNum (D8 n) TyNum (D8 E) Reverse' n (D8 a) r => Reverse' (D8 n) a r StripLeadingZeros (D8 a) (D8 a) DecrementRightToLeft (D9 a) (D8 a) DecrementRightToLeft (D8 a) (D7 a) IncrementRightToLeft (D8 a) (D9 a) IncrementRightToLeft (D7 a) (D8 a) (TyListTake cnt' nxt nxt', Pred (D8 r) cnt') => TyListTake (D8 r) (Cons val nxt) (Cons val nxt')

data D9 n Source

Constructors D9 n Instances Show n => Show (D9 n) TyNum n => TyNum (D9 n) TyNum (D9 E) Reverse' n (D9 a) r => Reverse' (D9 n) a r StripLeadingZeros (D9 a) (D9 a) DecrementRightToLeft (D9 a) (D8 a) DecrementRightToLeft a b => DecrementRightToLeft (D0 a) (D9 b) IncrementRightToLeft a b => IncrementRightToLeft (D9 a) (D0 b) IncrementRightToLeft (D8 a) (D9 a) (TyListTake cnt' nxt nxt', Pred (D9 r) cnt') => TyListTake (D9 r) (Cons val nxt) (Cons val nxt')

module Control.Concurrent.Session.SMonad

emptyMap :: TyMap Nil Nil Source

module Control.Concurrent.Session.Interleaving

Produced by Haddock version 2.3.0