Control.Concurrent.Session
- data OfferImpls where
- OfferImplsNil :: OfferImpls Nil prog progOut progIn finalState finalResult
- (~||~) :: (ProgramToMVarsOutgoing prog' progIn, Dual prog prog', Elem progIn l (MVar (ProgramCell (Cell incoming))), Elem progOut l (MVar (ProgramCell (Cell outgoing))), StripLeadingZeros b''1 y'1, Reverse' b'1 E b''1, DecrementRightToLeft a'1 b'1, Reverse' len'1 E a'1, ListLength st1 len'1, Elem prog' l st1, SmallerThan l len1, SNoJumpsBeyond prog' len1, ListLength prog' len1, SListOfSessionTypes prog', StripLeadingZeros b'' y', Reverse' b' E b'', DecrementRightToLeft a' b', Reverse' len' E a', ListLength st len', Elem prog l st, SmallerThan l len, SNoJumpsBeyond prog len, ListLength prog len, SListOfSessionTypes prog, ProgramToMVarsOutgoing prog progOut) => 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', Elem progOut l (MVar (ProgramCell (Cell outgoing))), Elem progIn l (MVar (ProgramCell (Cell incoming)))) => SessionChain prog progOut progIn (Cons (Jump l) Nil, Cons (Jump l) Nil) (outgoing, incoming) ()
- soffer :: forall finalState finalResult prog prog' progOut progIn jumps. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => OfferImpls jumps prog progOut progIn finalState finalResult -> SessionChain prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) finalState finalResult
- sselect :: forall prog prog' progOut progIn label jumps outgoing incoming len jumpTarget. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, ListLength jumps len, SmallerThan label len, TypeNumberToInt label, Elem jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', Elem progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), Elem 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', Elem progOut init (MVar (ProgramCell (Cell fromO))), Elem 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
- data Recv where
- 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
- newtype SChain m x y a = SChain {
- runSChain :: x -> m (a, y)
- class SMonad m where
- newtype SStateT s m x y a = SStateT {
- runSStateT :: s -> m x y (a, s)
- class SMonadTrans t where
- class SMonad m => SMonadIO m where
- class SMonad m => SMonadState s m | m -> s where
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 progOut progIn finalState finalResult |
(~||~) :: (ProgramToMVarsOutgoing prog' progIn, Dual prog prog', Elem progIn l (MVar (ProgramCell (Cell incoming))), Elem progOut l (MVar (ProgramCell (Cell outgoing))), StripLeadingZeros b''1 y'1, Reverse' b'1 E b''1, DecrementRightToLeft a'1 b'1, Reverse' len'1 E a'1, ListLength st1 len'1, Elem prog' l st1, SmallerThan l len1, SNoJumpsBeyond prog' len1, ListLength prog' len1, SListOfSessionTypes prog', StripLeadingZeros b'' y', Reverse' b' E b'', DecrementRightToLeft a' b', Reverse' len' E a', ListLength st len', Elem prog l st, SmallerThan l len, SNoJumpsBeyond prog len, ListLength prog len, SListOfSessionTypes prog, ProgramToMVarsOutgoing prog progOut) => 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 finalResultSource
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', Elem progOut l (MVar (ProgramCell (Cell outgoing))), Elem 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 finalState finalResult prog prog' progOut progIn jumps. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => OfferImpls jumps prog progOut progIn finalState finalResult -> SessionChain prog progOut progIn (Cons (Choice jumps) Nil, Cons (Choice jumps) Nil) finalState 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 len jumpTarget. (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn, ListLength jumps len, SmallerThan label len, TypeNumberToInt label, Elem jumps label (Cons (Jump jumpTarget) Nil), SWellFormedConfig jumpTarget (D0 E) prog, SWellFormedConfig jumpTarget (D0 E) prog', Elem progOut jumpTarget (MVar (ProgramCell (Cell outgoing))), Elem 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) 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.
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', Elem progOut init (MVar (ProgramCell (Cell fromO))), Elem 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 also then means that all implementations must start with
sjump), 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.
class SWellFormedConfig idxA idxB ss Source
Instances
| (SListOfSessionTypes ss, ListLength ss len, SNoJumpsBeyond ss len, SmallerThan idxA len, Elem ss idxA st, ListLength st len', SmallerThan idxB len') => SWellFormedConfig idxA idxB ss |
testWellformed :: SWellFormedConfig idxA idxB ss => ss -> idxA -> idxB -> BoolSource
Instances
| SListOfJumps (Cons val nxt) => STerminal (Offer (Cons val nxt)) | |
| SListOfJumps (Cons val nxt) => STerminal (Select (Cons val nxt)) | |
| (ListLength 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) | |
| (ListLength n len, Succ len len') => ListLength (Cons t n) len' | |
| OnlyOutgoing nxt nxt' => OnlyOutgoing (Cons (Recv t) nxt) nxt' | |
| (SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx | |
| (Elem nxt idx' res, Pred idx idx', SmallerThan idx' len, ListLength nxt len) => Elem (Cons val nxt) idx res | |
| Elem (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' => OnlyOutgoing (Cons (Send t) nxt) (Cons t nxt') | |
| OnlyOutgoing (Cons End Nil) (Cons End Nil) | |
| (Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt') | |
| (ProgramToMVarsOutgoing nxt nxt', OnlyOutgoing val val') => ProgramToMVarsOutgoing (Cons val nxt) (Cons (MVar (ProgramCell (Cell val'))) nxt') |
Instances
| Show Nil | |
| TyList Nil | |
| SListOfSessionTypes Nil | |
| SListOfJumps Nil | |
| SNoJumpsBeyond Nil idx | |
| Dual Nil Nil | |
| ProgramToMVarsOutgoing Nil Nil | |
| ListLength Nil (D0 E) | |
| STerminal a => SValidSessionType (Cons a Nil) | |
| (SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt) | |
| 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 (Cons End Nil) (Cons End Nil) |
Constructors
| E |
Instances
| Show E | |
| Reverse' E a a | |
| IncrementRightToLeft E (D1 E) | |
| ListLength Nil (D0 E) | |
| Pred m m' => Add m (D0 E) m | |
| TypeNumberToInt (D0 E) | |
| TyNum (D9 E) | |
| TyNum (D8 E) | |
| TyNum (D7 E) | |
| TyNum (D6 E) | |
| TyNum (D5 E) | |
| TyNum (D4 E) | |
| TyNum (D3 E) | |
| TyNum (D2 E) | |
| TyNum (D1 E) | |
| TyNum (D0 E) | |
| Pred y y' => SmallerThan (D0 E) y | |
| Pred n n' => Add (D0 E) n n | |
| StripLeadingZeros (D0 E) (D0 E) | |
| Add (D0 E) (D0 E) (D0 E) | |
| Elem (Cons res nxt) (D0 E) res |
Constructors
| D0 n |
Instances
| ListLength 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 | |
| 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) | |
| Elem (Cons res nxt) (D0 E) res |
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) |
Constructors
| D2 n |
Constructors
| D3 n |
Constructors
| D4 n |
Constructors
| D5 n |
Constructors
| D6 n |
Constructors
| D7 n |
Constructors
| D8 n |
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) |
An extension of the typical Monad such that you track additional
from and to parameters. Thus you can think of this like State
where the type of the State varies.
newtype SStateT s m x y a Source
Constructors
| SStateT | |
Fields
| |
Instances
| SMonad m => SMonadState s (SStateT s m) | |
| SMonadTrans (SStateT s) | |
| SMonad m => SMonad (SStateT s m) |
class SMonadTrans t whereSource
Instances
| SMonadTrans (SStateT s) |