-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Session Types for Haskell
--   
--   Session Types for Haskell. Allows the specification of communication
--   protocols and then validation that an implementation does not violate
--   said protocol.
@package sessions
@version 2008.2.23


-- | Type level Integers. These are all base 10.
module Control.Concurrent.Session.Number
data E
E :: E
data D0 n
D0 :: n -> D0 n
data D1 n
D1 :: n -> D1 n
data D2 n
D2 :: n -> D2 n
data D3 n
D3 :: n -> D3 n
data D4 n
D4 :: n -> D4 n
data D5 n
D5 :: n -> D5 n
data D6 n
D6 :: n -> D6 n
data D7 n
D7 :: n -> D7 n
data D8 n
D8 :: n -> D8 n
data D9 n
D9 :: n -> D9 n
class Succ x y | x -> y
tySucc :: (Succ x y) => x -> y
class Pred x y | x -> y
tyPred :: (Pred x y) => x -> y
class Add m n s | m n -> s
tyAdd :: (Add m n s) => m -> n -> s
class SmallerThan x y
class TyNum n

-- | Convert a type-level number to an Int. Of course, we can only go this
--   way...
class TypeNumberToInt ty
tyNumToInt :: (TypeNumberToInt ty) => ty -> Int
instance [overlap ok] (Show n) => Show (D9 n)
instance [overlap ok] (Show n) => Show (D8 n)
instance [overlap ok] (Show n) => Show (D7 n)
instance [overlap ok] (Show n) => Show (D6 n)
instance [overlap ok] (Show n) => Show (D5 n)
instance [overlap ok] (Show n) => Show (D4 n)
instance [overlap ok] (Show n) => Show (D3 n)
instance [overlap ok] (Show n) => Show (D2 n)
instance [overlap ok] (Show n) => Show (D1 n)
instance [overlap ok] (Show n) => Show (D0 n)
instance [overlap ok] Show E
instance [overlap ok] (Pred a b, TypeNumberToInt b) => TypeNumberToInt a
instance [overlap ok] TypeNumberToInt (D0 E)
instance [overlap ok] (TyNum n) => TyNum (D9 n)
instance [overlap ok] (TyNum n) => TyNum (D8 n)
instance [overlap ok] (TyNum n) => TyNum (D7 n)
instance [overlap ok] (TyNum n) => TyNum (D6 n)
instance [overlap ok] (TyNum n) => TyNum (D5 n)
instance [overlap ok] (TyNum n) => TyNum (D4 n)
instance [overlap ok] (TyNum n) => TyNum (D3 n)
instance [overlap ok] (TyNum n) => TyNum (D2 n)
instance [overlap ok] (TyNum n) => TyNum (D1 n)
instance [overlap ok] (TyNum n) => TyNum (D0 n)
instance [overlap ok] TyNum (D9 E)
instance [overlap ok] TyNum (D8 E)
instance [overlap ok] TyNum (D7 E)
instance [overlap ok] TyNum (D6 E)
instance [overlap ok] TyNum (D5 E)
instance [overlap ok] TyNum (D4 E)
instance [overlap ok] TyNum (D3 E)
instance [overlap ok] TyNum (D2 E)
instance [overlap ok] TyNum (D1 E)
instance [overlap ok] TyNum (D0 E)
instance [overlap ok] (Pred x x', Pred y y', SmallerThan x' y') => SmallerThan x y
instance [overlap ok] (Pred y y') => SmallerThan (D0 E) y
instance [overlap ok] (Add m' n' s, Pred m m', Pred n n', Succ s s', Succ s' s'') => Add m n s''
instance [overlap ok] (Pred n n') => Add (D0 E) n n
instance [overlap ok] (Pred m m') => Add m (D0 E) m
instance [overlap ok] Add (D0 E) (D0 E) (D0 E)
instance [overlap ok] (Reverse a a', DecrementRightToLeft a' b', Reverse b' b'', StripLeadingZeros b'' b) => Pred a b
instance [overlap ok] (StripLeadingZeros a b) => StripLeadingZeros (D0 a) b
instance [overlap ok] StripLeadingZeros (D9 a) (D9 a)
instance [overlap ok] StripLeadingZeros (D8 a) (D8 a)
instance [overlap ok] StripLeadingZeros (D7 a) (D7 a)
instance [overlap ok] StripLeadingZeros (D6 a) (D6 a)
instance [overlap ok] StripLeadingZeros (D5 a) (D5 a)
instance [overlap ok] StripLeadingZeros (D4 a) (D4 a)
instance [overlap ok] StripLeadingZeros (D3 a) (D3 a)
instance [overlap ok] StripLeadingZeros (D2 a) (D2 a)
instance [overlap ok] StripLeadingZeros (D1 a) (D1 a)
instance [overlap ok] StripLeadingZeros (D0 E) (D0 E)
instance [overlap ok] (DecrementRightToLeft a b) => DecrementRightToLeft (D0 a) (D9 b)
instance [overlap ok] DecrementRightToLeft (D1 a) (D0 a)
instance [overlap ok] DecrementRightToLeft (D2 a) (D1 a)
instance [overlap ok] DecrementRightToLeft (D3 a) (D2 a)
instance [overlap ok] DecrementRightToLeft (D4 a) (D3 a)
instance [overlap ok] DecrementRightToLeft (D5 a) (D4 a)
instance [overlap ok] DecrementRightToLeft (D6 a) (D5 a)
instance [overlap ok] DecrementRightToLeft (D7 a) (D6 a)
instance [overlap ok] DecrementRightToLeft (D8 a) (D7 a)
instance [overlap ok] DecrementRightToLeft (D9 a) (D8 a)
instance [overlap ok] (Reverse a a', IncrementRightToLeft a' b', Reverse b' b) => Succ a b
instance [overlap ok] (IncrementRightToLeft a b) => IncrementRightToLeft (D9 a) (D0 b)
instance [overlap ok] IncrementRightToLeft (D8 a) (D9 a)
instance [overlap ok] IncrementRightToLeft (D7 a) (D8 a)
instance [overlap ok] IncrementRightToLeft (D6 a) (D7 a)
instance [overlap ok] IncrementRightToLeft (D5 a) (D6 a)
instance [overlap ok] IncrementRightToLeft (D4 a) (D5 a)
instance [overlap ok] IncrementRightToLeft (D3 a) (D4 a)
instance [overlap ok] IncrementRightToLeft (D2 a) (D3 a)
instance [overlap ok] IncrementRightToLeft (D1 a) (D2 a)
instance [overlap ok] IncrementRightToLeft (D0 a) (D1 a)
instance [overlap ok] IncrementRightToLeft E (D1 E)
instance [overlap ok] (Reverse' n (D9 a) r) => Reverse' (D9 n) a r
instance [overlap ok] (Reverse' n (D8 a) r) => Reverse' (D8 n) a r
instance [overlap ok] (Reverse' n (D7 a) r) => Reverse' (D7 n) a r
instance [overlap ok] (Reverse' n (D6 a) r) => Reverse' (D6 n) a r
instance [overlap ok] (Reverse' n (D5 a) r) => Reverse' (D5 n) a r
instance [overlap ok] (Reverse' n (D4 a) r) => Reverse' (D4 n) a r
instance [overlap ok] (Reverse' n (D3 a) r) => Reverse' (D3 n) a r
instance [overlap ok] (Reverse' n (D2 a) r) => Reverse' (D2 n) a r
instance [overlap ok] (Reverse' n (D1 a) r) => Reverse' (D1 n) a r
instance [overlap ok] (Reverse' n (D0 a) r) => Reverse' (D0 n) a r
instance [overlap ok] Reverse' E a a
instance [overlap ok] (Reverse' x E y) => Reverse x y


-- | Heterogeneous lists. This has been done many times, in many different
--   ways. Explicit constructors are hidden deliberately.
module Control.Concurrent.Session.List
data Nil :: *
Nil :: Nil
data Cons :: * -> * -> *
Cons :: t -> n -> Cons t n

-- | Find the length of a list.
class ListLength list length | list -> length
listLength :: (ListLength list length) => list -> length
nil :: Nil
cons :: (TyList n) => t -> n -> (Cons t n)
class TyList l

-- | Index or update a list
class Elem lst idx res | lst idx -> res
tyListElem :: (Elem lst idx res) => lst -> idx -> res
tyListUpdate :: (Elem lst idx res) => lst -> idx -> res -> lst
instance [overlap ok] (Elem nxt idx' res, Pred idx idx', SmallerThan idx' len, ListLength nxt len) => Elem (Cons val nxt) idx res
instance [overlap ok] Elem (Cons res nxt) (D0 E) res
instance [overlap ok] (TyList nxt) => TyList (Cons val nxt)
instance [overlap ok] TyList Nil
instance [overlap ok] (ListLength n l, Succ l l', Show n, Show t) => Show (Cons t n)
instance [overlap ok] Show Nil
instance [overlap ok] (ListLength n len, Succ len len') => ListLength (Cons t n) len'
instance [overlap ok] ListLength Nil (D0 E)


-- | This module is concerned with allowing you to describe a session type.
--   A session type is treated as a table or 2D array, where each row
--   represents a particular session type function which can refer, by
--   index, to the other rows.
--   
--   Basically, what you have here is the ability to describe a program at
--   the type level.
--   
--   Just look at <a>Control.Concurrent.Session.Tests</a> for examples
module Control.Concurrent.Session.SessionType
data End
End :: End
end :: Cons End Nil
data Send :: * -> *
Send :: t -> Send t
SendInt :: Send Int
SendBool :: Send Bool
SendChar :: Send Char
SendStr :: Send String
SendDouble :: Send Double
data Recv :: * -> *
Recv :: t -> Recv t
RecvInt :: Recv Int
RecvBool :: Recv Bool
RecvChar :: Recv Char
RecvStr :: Recv String
RecvDouble :: Recv Double
data Jump l
Jump :: l -> Jump l
jump :: (TyNum n) => n -> Cons (Jump n) Nil
data Select :: * -> *
Select :: lstOfLabels -> Select lstOfLabels
select :: (SListOfJumps (Cons val nxt)) => (Cons val nxt) -> Cons (Select (Cons val nxt)) Nil
data Offer :: * -> *
Offer :: lstOfLabels -> Offer lstOfLabels
offer :: (SListOfJumps (Cons val nxt)) => (Cons val nxt) -> Cons (Offer (Cons val nxt)) Nil
class Dual a b | a -> b, b -> a
dual :: (Dual a b) => a -> b
class SListOfJumps lst
class SListOfSessionTypes lstOfLists
class SNonTerminal a
class STerminal a
class SValidSessionType lst
(~>) :: (TyList nxt, SNonTerminal a, SValidSessionType nxt) => a -> nxt -> (Cons a nxt)
(~|~) :: (TyNum target, TyList nxt) => target -> nxt -> Cons (Cons (Jump target) Nil) nxt
class SNoJumpsBeyond s idx
class SWellFormedConfig idxA idxB ss
testWellformed :: (SWellFormedConfig idxA idxB ss) => ss -> idxA -> idxB -> Bool
data Choice :: * -> *
Choice :: lstOfLabels -> Choice lstOfLabels
class OnlyOutgoing a b | a -> b
onlyOutgoing :: (OnlyOutgoing a b) => a -> b
instance [overlap ok] (Show l) => Show (Jump l)
instance [overlap ok] Show End
instance [overlap ok] (OnlyOutgoing nxt nxt') => OnlyOutgoing (Cons (Send t) nxt) (Cons t nxt')
instance [overlap ok] OnlyOutgoing (Cons (Jump l) Nil) (Cons (Jump l) Nil)
instance [overlap ok] OnlyOutgoing (Cons End Nil) (Cons End Nil)
instance [overlap ok] OnlyOutgoing (Cons (Select jl) Nil) (Cons (Choice jl) Nil)
instance [overlap ok] OnlyOutgoing (Cons (Offer jl) Nil) (Cons (Choice jl) Nil)
instance [overlap ok] (OnlyOutgoing nxt nxt') => OnlyOutgoing (Cons (Recv t) nxt) nxt'
instance [overlap ok] (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
instance [overlap ok] (SNoJumpsBeyond val idx, SNoJumpsBeyond nxt idx) => SNoJumpsBeyond (Cons val nxt) idx
instance [overlap ok] SNoJumpsBeyond Nil idx
instance [overlap ok] (SNoJumpsBeyond lol idx) => SNoJumpsBeyond (Offer lol) idx
instance [overlap ok] (SNoJumpsBeyond lol idx) => SNoJumpsBeyond (Select lol) idx
instance [overlap ok] SNoJumpsBeyond (Recv t) idx
instance [overlap ok] SNoJumpsBeyond (Send t) idx
instance [overlap ok] (SmallerThan l idx) => SNoJumpsBeyond (Jump l) idx
instance [overlap ok] SNoJumpsBeyond End idx
instance [overlap ok] (SValidSessionType nxt, SNonTerminal val) => SValidSessionType (Cons val nxt)
instance [overlap ok] (STerminal a) => SValidSessionType (Cons a Nil)
instance [overlap ok] (SListOfJumps (Cons val nxt)) => STerminal (Offer (Cons val nxt))
instance [overlap ok] (SListOfJumps (Cons val nxt)) => STerminal (Select (Cons val nxt))
instance [overlap ok] (TyNum l) => STerminal (Jump l)
instance [overlap ok] STerminal End
instance [overlap ok] SNonTerminal (Recv t)
instance [overlap ok] SNonTerminal (Send t)
instance [overlap ok] (SValidSessionType val, SListOfSessionTypes nxt) => SListOfSessionTypes (Cons val nxt)
instance [overlap ok] SListOfSessionTypes Nil
instance [overlap ok] (SListOfJumps nxt, TyNum val) => SListOfJumps (Cons (Cons (Jump val) Nil) nxt)
instance [overlap ok] SListOfJumps Nil
instance [overlap ok] (Dual val val', Dual nxt nxt') => Dual (Cons val nxt) (Cons val' nxt')
instance [overlap ok] Dual Nil Nil
instance [overlap ok] Dual (Offer lst) (Select lst)
instance [overlap ok] Dual (Select lst) (Offer lst)
instance [overlap ok] Dual (Recv t) (Send t)
instance [overlap ok] Dual (Send t) (Recv t)
instance [overlap ok] Dual (Jump l) (Jump l)
instance [overlap ok] Dual End End


-- | Super magic Monads.
module Control.Concurrent.Session.SMonad
newtype SChain m x y a
SChain :: (x -> m (a, y)) -> SChain m x y a
runSChain :: SChain m x y a -> x -> m (a, y)

-- | An extension of the typical Monad such that you track additional
--   <tt>from</tt> and <tt>to</tt> parameters. Thus you can think of this
--   like <a>State</a> where the type of the <a>State</a> varies.
class SMonad m :: (* -> * -> * -> *)
(~>>) :: (SMonad m) => m x y a -> m y z b -> m x z b
(~>>=) :: (SMonad m) => m x y a -> (a -> m y z b) -> m x z b
sreturn :: (SMonad m) => a -> m x x a
newtype SStateT s m x y a
SStateT :: (s -> m x y (a, s)) -> SStateT s m x y a
runSStateT :: SStateT s m x y a -> s -> m x y (a, s)
class SMonadTrans t
slift :: (SMonadTrans t, SMonad m) => m x y a -> t m x y a
class (SMonad m) => SMonadIO m
sliftIO :: (SMonadIO m) => IO a -> m x x a
class (SMonad m) => SMonadState s m | m -> s
sget :: (SMonadState s m) => m x x s
sput :: (SMonadState s m) => s -> m x x ()
instance (SMonad m) => SMonadState s (SStateT s m)
instance (MonadIO m) => SMonadIO (SChain m)
instance SMonadTrans (SStateT s)
instance (SMonad m) => SMonad (SStateT s m)
instance (Monad m) => Monad (SChain m x x)
instance (Monad m) => SMonad (SChain m)


-- | Having actually described a session type, you'll now want to implement
--   it! Use the methods of <a>SMonad</a> to chain functions together.
module Control.Concurrent.Session.Runtime

-- | Use OfferImpls to construct the implementations of the branches of an
--   offer. Really, it's just a slightly fancy list.
data OfferImpls :: * -> * -> * -> * -> * -> * -> *
OfferImplsNil :: OfferImpls Nil prog progOut progIn finalState finalResult

-- | Use to construct OfferImpls. This function automatically adds the
--   necessary <a>sjump</a> to the start of each branch implementation.
(~||~) :: (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 (outgoing, incoming) finalState finalResult) -> (OfferImpls jumps prog progOut progIn finalState finalResult) -> (OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog progOut progIn finalState finalResult)
data SessionState :: * -> * -> * -> * -> *

-- | The representation of a computation that performs work using session
--   types. Again, really quite similar to a more-parameterized State
--   monad.
newtype SessionChain prog progOut progIn from to res
SessionChain :: ((SessionState prog progOut progIn from) -> IO (res, SessionState prog progOut progIn to)) -> SessionChain prog progOut progIn from to res
runSessionChain :: SessionChain prog progOut progIn from to res -> (SessionState prog progOut progIn from) -> IO (res, SessionState prog progOut progIn to)

-- | 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.
sjump :: (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) ()

-- | Send a value to the other party. Of course, the value must be of the
--   correct type indicated in the session type.
ssend :: (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => t -> (SessionChain prog progOut progIn) (Cons t nxt, incoming) (nxt, incoming) ()

-- | 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.
srecv :: (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => (SessionChain prog progOut progIn) (outgoing, Cons t nxt) (outgoing, nxt) t

-- | Offer a number of branches. This is basically an external choice - the
--   other party uses <a>sselect</a> 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.
soffer :: (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

-- | Select which branch we're taking at a branch point. Use a type number
--   (<a>Control.Concurrent.Session.Number</a>) to indicate the branch to
--   take.
sselect :: (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) ()

-- | Run! Provide a program and a start point within that program (which is
--   automatically <a>sjump</a>ed 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.
run :: (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')
class ProgramToMVarsOutgoing prog mvars | prog -> mvars
instance (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => SMonadIO (SessionChain prog progOut progIn)
instance (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => SMonad (SessionChain prog progOut progIn)
instance (ProgramToMVarsOutgoing nxt nxt', OnlyOutgoing val val') => ProgramToMVarsOutgoing (Cons val nxt) (Cons (MVar (ProgramCell (Cell val'))) nxt')
instance ProgramToMVarsOutgoing Nil Nil
instance WalkOfferImpls prog progOut progIn finalState finalResult


-- | This is just a convenience module that reexports everything you're
--   expected to need.
module Control.Concurrent.Session

-- | Use OfferImpls to construct the implementations of the branches of an
--   offer. Really, it's just a slightly fancy list.
data OfferImpls :: * -> * -> * -> * -> * -> * -> *
OfferImplsNil :: OfferImpls Nil prog progOut progIn finalState finalResult

-- | Use to construct OfferImpls. This function automatically adds the
--   necessary <a>sjump</a> to the start of each branch implementation.
(~||~) :: (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 (outgoing, incoming) finalState finalResult) -> (OfferImpls jumps prog progOut progIn finalState finalResult) -> (OfferImpls (Cons (Cons (Jump l) Nil) jumps) prog progOut progIn finalState finalResult)

-- | 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.
sjump :: (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) ()

-- | Offer a number of branches. This is basically an external choice - the
--   other party uses <a>sselect</a> 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.
soffer :: (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

-- | Select which branch we're taking at a branch point. Use a type number
--   (<a>Control.Concurrent.Session.Number</a>) to indicate the branch to
--   take.
sselect :: (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) ()

-- | Send a value to the other party. Of course, the value must be of the
--   correct type indicated in the session type.
ssend :: (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => t -> (SessionChain prog progOut progIn) (Cons t nxt, incoming) (nxt, incoming) ()

-- | 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.
srecv :: (Dual prog prog', ProgramToMVarsOutgoing prog progOut, ProgramToMVarsOutgoing prog' progIn) => (SessionChain prog progOut progIn) (outgoing, Cons t nxt) (outgoing, nxt) t

-- | Run! Provide a program and a start point within that program (which is
--   automatically <a>sjump</a>ed 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.
run :: (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 :: * -> *
Send :: t -> Send t
SendInt :: Send Int
SendBool :: Send Bool
SendChar :: Send Char
SendStr :: Send String
SendDouble :: Send Double
data Recv :: * -> *
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
dual :: (Dual a b) => 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 :: E
data D0 n
D0 :: n -> D0 n
data D1 n
D1 :: n -> D1 n
data D2 n
D2 :: n -> D2 n
data D3 n
D3 :: n -> D3 n
data D4 n
D4 :: n -> D4 n
data D5 n
D5 :: n -> D5 n
data D6 n
D6 :: n -> D6 n
data D7 n
D7 :: n -> D7 n
data D8 n
D8 :: n -> D8 n
data D9 n
D9 :: n -> D9 n