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


-- | Session types distributed
--   
--   This package serves as a wrapper over both the Cloud Haskell library
--   (distributed-process) and the sessiontypes library. It provides an
--   interpreter for evaluating session typed programs to Cloud Haskell
--   programs and exposes several combinators for spawning sessions.
@package sessiontypes-distributed
@version 0.1.0

module Control.Distributed.Session.Visualize

-- | Visualizes the session type of a given <tt>STTerm</tt> You may use
--   this function in the following way
--   
--   <pre>
--   main = visualize st
--   </pre>
--   
--   Then the following command will generate a diagram named
--   "sessiontype.png"
--   
--   <pre>
--   stack exec vis-sessiontype -- -o sessiontype.png -w 400
--   </pre>
--   
--   For more information on how to generate a diagram please visit the
--   <a>diagrams</a> package
visualize :: (MonadSession m, MkDiagram * s) => m (Cap * ctx s) r a -> IO ()

-- | Visualizes a given session type denoted by a Proxy.
visualizeP :: MkDiagram k s => Proxy (ST k) s -> IO ()


-- | Defines a session typed channel as a wrapper over the typed channel
--   from Cloud Haskell
--   
--   We define a session typed channel to overcome the limitation of a
--   typed channel that can only send and receive messages of a single
--   type.
--   
--   Underneath we actually do the same, and make use of
--   <a>unsafeCoerce</a> to coerce a value's type to that described in the
--   session typed.
--   
--   Session types do not entirely guarantee safety of using
--   <a>unsafeCoerce</a>. One can use the same session typed send port over
--   and over again, while the correpsonding receive port might progress
--   through the session type resulting in a desync of types between the
--   send and receive port.
--   
--   It is for this reason recommended to always make use of
--   <a>STChannelT</a> that always progresses the session type of a port
--   after a session typed action.
module Control.Distributed.Session.STChannel

-- | Basic message type that existentially quantifies the content of the
--   message
data Message
Message :: a -> Message

-- | Session typed send port as a wrapper over SendPort Message. It is
--   parameterized with a capability/sessiontype.
data STSendPort (l :: Cap Type)
STSendPort :: (SendPort Message) -> STSendPort

-- | Session typed receive port as a wrapper over ReceivePort Message. It
--   is parameterized with a capability/sessiontype.
data STReceivePort (l :: Cap Type)
STReceivePort :: (ReceivePort Message) -> STReceivePort

-- | Type synonym for a session typed channel given a single session type
--   
--   This removes recv session types from the given session type as it is
--   passed to the send port type
--   
--   Also removes send session types from the given session type as it is
--   passed to the receive port type
type STChan s = (STSendPort (RemoveRecv s), STReceivePort (RemoveSend s))

-- | Same as <a>STChan</a>, but it is given a session type for the send
--   port type and a separate session type for the receive port type
type STChanBi s r = (STSendPort (RemoveRecv s), STReceivePort (RemoveSend r))

-- | Unsession typed typed channel
--   
--   It is essentially just a typed channel that is parameterized with
--   <a>Message</a>.
--   
--   We can carry around this type in <tt>Session</tt>, but not a
--   <a>STChan</a>.
type UTChan = (SendPort Message, ReceivePort Message)

-- | Creates a new session typed channel given a single session type
newSTChan :: Proxy s -> Process (STChan s)

-- | Creates a new session typed channel given separate session types for
--   the send port and receive port
newSTChanBi :: Proxy s -> Proxy r -> Process (STChanBi s r)

-- | Creates an unsession typed channel
newUTChan :: Process UTChan

-- | Converts an unsession typed channel to a session typed channel
toSTChan :: UTChan -> Proxy s -> STChan s

-- | Converts an unsession typed channel to a session typed channel
toSTChanBi :: UTChan -> Proxy s -> Proxy r -> STChanBi s r

-- | Converts a session typed send port into a Proxy
sendProxy :: STSendPort s -> Proxy s

-- | Converts a session typed receive port into a Proxy
recvProxy :: STReceivePort s -> Proxy s

-- | Sends a message using a session typed send port
sendSTChan :: Serializable a => STSendPort (Cap ctx (a :!> l)) -> a -> Process (STSendPort (Cap ctx l))

-- | Receives a message using a session typed receive port
recvSTChan :: Serializable a => STReceivePort (Cap ctx (a :?> l)) -> Process (a, STReceivePort (Cap ctx l))

-- | Type class that defines combinators for branching on a session typed
--   port
class STSplit (m :: Cap Type -> Type)

-- | select the first branch of a selection using the given port
sel1Chan :: STSplit m => m (Cap ctx (Sel (s : xs))) -> m (Cap ctx s)

-- | select the second branch of a selection using the given port
sel2Chan :: STSplit m => m (Cap ctx (Sel (s : (t : xs)))) -> m (Cap ctx (Sel (t : xs)))

-- | select the first branch of an offering using the given port
off1Chan :: STSplit m => m (Cap ctx (Off (s : xs))) -> m (Cap ctx s)

-- | select the second branch of an offering using the given port
off2Chan :: STSplit m => m (Cap ctx (Off (s : (t : xs)))) -> m (Cap ctx (Off (t : xs)))

-- | Type class for recursion on a session typed port
class STRec (m :: Cap Type -> Type)
recChan :: STRec m => m (Cap ctx (R s)) -> m (Cap (s : ctx) s)
wkChan :: STRec m => m (Cap (t : ctx) (Wk s)) -> m (Cap ctx s)
varChan :: STRec m => m (Cap (s : ctx) V) -> m (Cap (s : ctx) s)

-- | Indexed monad transformer that is indexed by two products of session
--   types
--   
--   This monad also acts as a state monad that whose state is defined by a
--   session typed channel and dependent on the indexing of the monad.
data STChannelT m (p :: Prod Type) (q :: Prod Type) a
STChannelT :: ((STSendPort (Left p), STReceivePort (Right p)) -> m (a, (STSendPort (Left q), STReceivePort (Right q)))) -> STChannelT m a
[runSTChannelT] :: STChannelT m a -> ((STSendPort (Left p), STReceivePort (Right p)) -> m (a, (STSendPort (Left q), STReceivePort (Right q))))

-- | Send a message
--   
--   Only the session type of the send port needs to be adjusted
sendSTChanM :: Serializable a => a -> STChannelT Process (Cap ctx (a :!> l) :*: r) (Cap ctx l :*: r) ()

-- | receive a message
--   
--   Only the session type of the receive port needs to be adjusted
recvSTChanM :: Serializable a => STChannelT Process (l :*: (Cap ctx (a :?> r))) (l :*: Cap ctx r) a

-- | select the first branch of a selection
--   
--   Both ports are now adjusted. This is similarly so for the remaining
--   combinators.
sel1ChanM :: STChannelT Process (Cap lctx (Sel (l : ls)) :*: (Cap rctx (Sel (r : rs)))) (Cap lctx l :*: Cap rctx r) ()

-- | select the second branch of a selection
sel2ChanM :: STChannelT Process (Cap lctx (Sel (s1 : (t1 : xs1))) :*: Cap rctx (Sel (s2 : (t2 : xs2)))) (Cap lctx (Sel (t1 : xs1)) :*: Cap rctx (Sel (t2 : xs2))) ()

-- | select the first branch of an offering
off1ChanM :: STChannelT Process (Cap lctx (Off (l : ls)) :*: (Cap rctx (Off (r : rs)))) (Cap lctx l :*: Cap rctx r) ()

-- | select the second branch of an offering
off2ChanM :: STChannelT Process (Cap lctx (Off (s1 : (t1 : xs1))) :*: Cap rctx (Off (s2 : (t2 : xs2)))) (Cap lctx (Off (t1 : xs1)) :*: Cap rctx (Off (t2 : xs2))) ()

-- | delimit scope of recursion
recChanM :: STChannelT Process (Cap sctx (R s) :*: Cap rctx (R r)) (Cap (s : sctx) s :*: Cap (r : rctx) r) ()

-- | weaken scope of recursion
wkChanM :: STChannelT Process (Cap (t : sctx) (Wk s) :*: Cap (k : rctx) (Wk r)) (Cap sctx s :*: Cap rctx r) ()

-- | recursion variable (recurse here)
varChanM :: STChannelT Process ((Cap (s : sctx) V) :*: (Cap (r : rctx) V)) (Cap (s : sctx) s :*: Cap (r : rctx) r) ()

-- | ports are no longer usable
epsChanM :: STChannelT Process (Cap ctx Eps :*: Cap ctx Eps) (Cap ctx Eps :*: Cap ctx Eps) ()
instance Data.Binary.Class.Binary Control.Distributed.Session.STChannel.Message
instance Control.Distributed.Session.STChannel.STSplit Control.Distributed.Session.STChannel.STSendPort
instance Control.Distributed.Session.STChannel.STSplit Control.Distributed.Session.STChannel.STReceivePort
instance Control.Distributed.Session.STChannel.STRec Control.Distributed.Session.STChannel.STSendPort
instance Control.Distributed.Session.STChannel.STRec Control.Distributed.Session.STChannel.STReceivePort
instance GHC.Base.Monad m => Control.SessionTypes.Indexed.IxFunctor (Control.Distributed.Session.STChannel.STChannelT m)
instance GHC.Base.Monad m => Control.SessionTypes.Indexed.IxApplicative (Control.Distributed.Session.STChannel.STChannelT m)
instance GHC.Base.Monad m => Control.SessionTypes.Indexed.IxMonad (Control.Distributed.Session.STChannel.STChannelT m)
instance GHC.Base.Monad m => Control.SessionTypes.Indexed.IxMonadT Control.Distributed.Session.STChannel.STChannelT m


-- | This module defines the <a>Session</a> session typed indexed monad.
module Control.Distributed.Session.Session

-- | <a>Session</a> is defined as a newtype wrapper over a function that
--   takes a `Maybe SessionInfo` and returns an indexed codensity monad
--   transformer over the <a>Process</a> monad.
--   
--   <a>Session</a> is also a reader monad that has a Maybe SessionInfo as
--   its environment. <a>SessionInfo</a> is wrapped in a <a>Maybe</a>,
--   because we also allow a session to be run singularly. In which case
--   there is no other Session to communicate with and therefore is there
--   also no need for a <a>SessionInfo</a>.
--   
--   The function returns the indexed codensity monad and not simply a
--   <a>STTerm</a>, because from benchmarking the codensity monad gave us
--   significant performance improvements for free.
newtype Session s r a
Session :: (Maybe SessionInfo -> IxC Process s r a) -> Session s r a
[runSessionC] :: Session s r a -> Maybe SessionInfo -> IxC Process s r a

-- | The SessionInfo data type tells us information about another
--   <a>Session</a>. Namely, the <a>Session</a> that is in a session with
--   the <a>Session</a> that this specific <a>SessionInfo</a> belongs to.
data SessionInfo
SessionInfo :: ProcessId -> NodeId -> UTChan -> SessionInfo

-- | The <a>ProcessId</a> of the dual <a>Session</a>
[othPid] :: SessionInfo -> ProcessId

-- | The <a>NodeId</a> of the <tt>Node</tt> that the dual <a>Session</a>
--   runs on
[othNode] :: SessionInfo -> NodeId

-- | A send port belonging to the dual <a>Session</a>, such that we can
--   send messages to it. And a receive port of which the dual
--   <a>Session</a> has its send port, such that we can receive messages
--   from the dual <a>Session</a>.
[utchan] :: SessionInfo -> UTChan

-- | Evaluates a session to a <a>STTerm</a>
runSession :: Session s r a -> Maybe SessionInfo -> STTerm Process s r a

-- | Lifts a <a>Process</a> computation
liftP :: Process a -> Session s s a

-- | Lifts a <a>STTerm</a> computation
liftST :: STTerm Process s r a -> Session s r a
instance Control.SessionTypes.Indexed.IxFunctor Control.Distributed.Session.Session.Session
instance Control.SessionTypes.Indexed.IxApplicative Control.Distributed.Session.Session.Session
instance Control.SessionTypes.Indexed.IxMonad Control.Distributed.Session.Session.Session
instance Control.SessionTypes.MonadSession.MonadSession Control.Distributed.Session.Session.Session
instance Control.SessionTypes.Indexed.IxMonadReader (GHC.Base.Maybe Control.Distributed.Session.Session.SessionInfo) Control.Distributed.Session.Session.Session
instance Control.SessionTypes.Indexed.IxMonadIO Control.Distributed.Session.Session.Session


-- | This module provides three functions for normalizing session typed
--   programs.
--   
--   With normalizing we mean that we apply rewrites to a session typed
--   program until we can no longer do so and that do not change the
--   semantics of the program.
--   
--   The motivation for this module is that for two session typed programs
--   to run as a session they must be dual. Sometimes, one of these
--   programs might not have a session type that is dual to the session
--   type of the other program,
--   
--   but we can rewrite the program and therefore also its session type. It
--   is of course important that we do not alter the semantics of the
--   program when rewriting it. For that reason, any rewrite that we may
--   apply must be isomorphic.
--   
--   A rewrite is isomorphic if we have two programs p and p', we can do a
--   rewrite from p to p' and from p' to p.
--   
--   For now two types of rewrites are applied: Elimination of recursive
--   types and flattening of branches.
--   
--   An additional benefit of normalizing is that it may lead to further
--   optimizations.
--   
--   In <a>Control.Distributed.Session.Eval</a> we send an integer for
--   every <a>Sel</a> session type that we encounter. By flattening
--   branching we reduce the number of <a>Sel</a> constructors and
--   therefore also the number of times one needs to communicate an
--   integer.
module Control.Distributed.Session.Normalize

-- | Applies two types of rewrites to a <a>Session</a>.
--   
--   <ul>
--   <li>Elimination of unused recursion</li>
--   <li>Rewrites non-right nested branchings to right nested
--   branchings</li>
--   </ul>
normalize :: Normalize s s' => Session s (Cap '[] Eps) a -> Session s' (Cap '[] Eps) a

-- | Function for eliminating unused recursive types.
--   
--   The function <a>elimRec</a> takes a <a>Session</a> and traverses the
--   underlying <a>STTerm</a>. While doing so, it will attempt to remove
--   <a>STTerm</a> constructors annotated with <a>R</a> or <a>Wk</a> from
--   the program if in doing so does not change the behavior of the
--   program.
--   
--   For example, in the following session type we may remove the inner
--   <a>R</a> and the <a>Wk</a>.
--   
--   <pre>
--   R (R (Wk V))
--   </pre>
--   
--   We have that the outer <a>R</a> matches the recursion variable because
--   of the use of <a>Wk</a>.
--   
--   That means the inner <a>R</a> does not match any recursion variable
--   (the <a>R</a> is unused) and therefore may it and its corresponding
--   constructor be removed from the session.
--   
--   We also remove the <a>Wk</a>, because the session type pushed into the
--   context by the inner <a>R</a> has also been removed.
--   
--   The generated session type is
--   
--   <pre>
--   R V
--   </pre>
elimRec :: ElimRec s s' => Session s (Cap '[] Eps) a -> Session s' (Cap '[] Eps) a

-- | Flattening of branching
--   
--   The function <a>flatten</a> takes a <a>Session</a> and traverses the
--   underlying <a>STTerm</a>. If it finds a branching session type that
--   has a branch starting with another branching of the same type, then it
--   will extract the branches of the inner branching and inserts these
--   into the outer branching. This is similar to flattening a list of
--   lists to a larger list.
--   
--   For example:
--   
--   <pre>
--   Sel '[a,b, Sel '[c,d], e]
--   </pre>
--   
--   becomes
--   
--   <pre>
--   Sel '[a,b,c,d,e]
--   </pre>
--   
--   This only works if the inner branching has the same type as the outer
--   branch (Sel in Sel or Off in Off).
--   
--   Also, for now this rewrite only works if one of the branching of the
--   outer branch starts with a new branching.
--   
--   For example:
--   
--   <pre>
--   Sel '[a,b, Int :!&gt; Sel '[c,d],e]
--   </pre>
--   
--   does not become
--   
--   <pre>
--   Sel '[a,b,Int :!&gt; c, Int :!&gt; d, e]
--   </pre>
--   
--   Although, this is something that will be added in the future.
flatten :: Flatten s s' => Session s (Cap '[] Eps) a -> Session s' (Cap '[] Eps) a


-- | This module exposes two functions for interactively evaluation a
--   session typed program
--   
--   To run a session you must have two participating actors. In our
--   context, the actors are session typed programs.
--   
--   Using this module the user will act as one of the actors in the
--   session by suppling values to a receive
--   
--   and selecting a branch for offerings.
module Control.Distributed.Session.Interactive

-- | For this function the user will act as the dual to the given session.
--   User interaction is only required when the given program does a
--   receive or an offer.
--   
--   A possible interaction goes as follows:
--   
--   <pre>
--   prog = do
--    send 5
--    x &lt;- recv
--    offer (eps x) (eps "")
--   
--   main = interactive prog
--   </pre>
--   
--   <pre>
--   &gt; Enter value of type String: "test"
--   &gt; (L)eft or (R)ight: L
--    "test"
--   </pre>
interactive :: (HasConstraints '[Read, Show, Typeable] s, Show a) => Session s r a -> Process a

-- | Different from <a>interactive</a> is that this function gives the user
--   the choice to abort the session after each session typed action.
--   
--   Furthermore, it also prints additional output describing which session
--   typed action occurred.
interactiveStep :: (HasConstraints '[Read, Show, Typeable] s, Show a) => Session s r a -> Process (Maybe a)


-- | This module defines two interpreters for mapping the Cloud Haskell
--   semantics to the constructors of <a>STTerm</a>.
module Control.Distributed.Session.Eval

-- | This function unpacks a <a>Session</a> to a <a>STTerm</a> using a
--   given <a>SessionInfo</a>.
--   
--   It then evaluates the <a>STTerm</a> by mapping Cloud Haskell semantics
--   to each constructor of <a>STTerm</a>.
--   
--   The function relies on that there exists another session (on a
--   different process) that is also being evaluated (using evalSession)
--   and acts as the dual the session that function is now evaluating.
--   
--   The underlying communication method is a session typed channel
--   (<a>STChannelT</a>). There should be no interference from other
--   processes, unless you go through the effort of sharing the send port.
evalSession :: forall s r a. HasConstraint Serializable s => Session s r a -> SessionInfo -> Process a

-- | Similar to <a>evalSession</a>, except for that it does not evaluate
--   session typed actions.
--   
--   Only returns and lifted computations are evaluated. This also means
--   that there does not need to be a dual session that is evaluated on a
--   different process.
--   
--   It also assumes that <a>SessionInfo</a> is not used. Use
--   <a>evalSessionEq'</a> if this is not the case.
evalSessionEq :: Session s s a -> Process a

-- | Same as <a>evalSessionEq</a>, but you may now provide a
--   <a>SessionInfo</a>.
evalSessionEq' :: Session s s a -> SessionInfo -> Process a


-- | Provides instances for <a>Session</a> of <a>IxMonadThrow</a>,
--   <a>IxMonadCatch</a> and <a>IxMonadMask</a>.
--   
--   These instances should behave no differently from the corresponding
--   <a>MonadThrow</a>, <a>MonadCatch</a> and <a>MonadMask</a> instances
--   for <a>Process</a>. For more documentation please visit
--   <a>Control.Monad.Catch</a>
--   
--   The reason that the instances are placed in a separate module is to
--   avoid a circular dependency of the modules.
--   
--   The instances require evaluation of the sessions, therefore
--   <a>Control.Distributed.Session.Eval</a> should be imported.
--   
--   However that module imports
--   <a>Control.Distributed.Session.Session</a>. Placing these instances in
--   this module would then require importing
--   <a>Control.Distributed.Session.Eval</a> causing a circular dependency.
--   
--   Note that these instances are already exported by
--   <a>Control.Distributed.Session</a>, such that this module should need
--   no explicit import.
module Control.Distributed.Session.Exception
instance Control.SessionTypes.Indexed.IxMonadThrow Control.Distributed.Session.Session.Session s
instance Control.SessionTypes.Indexed.IxMonadCatch Control.Distributed.Session.Session.Session s
instance Control.SessionTypes.Indexed.IxMonadMask Control.Distributed.Session.Session.Session s


-- | This module describes an interpreter for purely evaluating session
--   typed programs
--   
--   that is based on the paper <i>Beauty in the beast</i> by <i>Swierstra,
--   W., &amp; Altenkirch, T.</i>
--   
--   Impurity in a session typed programs mainly comes from three things:
--   receives, branching and lifting.
--   
--   <ul>
--   <li>Using the session type we can easily determine the type of the
--   message that each receive should expect. This information allows us to
--   define a stream of values of different types that provides input for
--   each receive.</li>
--   <li>When evaluating a session we send and receive integers to choose a
--   branch in a selection and offering respectively. If we want to purely
--   evaluate a session typed program, then we must provide some kind of
--   input that makes this choice for us.</li>
--   <li>The current structure of the <a>Lift</a> constructor does not
--   allow us to purely evaluate a <a>Lift</a>. As such a session typed
--   program may not contain a lift for it to be purely evaluated. See
--   <a>runM</a> as an alternative.</li>
--   </ul>
module Control.Distributed.Session.Debug

-- | Purely evaluates a given <a>Session</a> using the input defined by
--   <tt>Stream</tt>.
--   
--   The output is described in terms of the session type actions within
--   the given program
--   
--   An example of how to use this function goes as follows:
--   
--   <pre>
--   prog :: Session ('Cap '[] (Int :!&gt; String :?&gt; Eps)) ('Cap '[] Eps) String
--   prog = send 5 &gt;&gt; recv &gt;&gt;= eps
--   
--   strm = S_Send $ S_Recv "foo" S_Eps
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; run prog strm
--   O_Send 5 $ O_Recv "foo" $ O_Eps "foo"
--   </pre>
run :: HasConstraint Show s => Session s (Cap ctx Eps) a -> Stream s -> Output s a

-- | Instead of describing the session typed actions, it returns a list of
--   the results of all branches of all offerings.
--   
--   <pre>
--   prog = offer (eps 10) (eps 5)
--   strm = S_OffS S_Eps S_Eps
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; runAll prog strm
--   [10,5]
--   </pre>
runAll :: HasConstraint Show s => Session s (Cap ctx Eps) a -> Stream s -> [a]

-- | Same as <a>runAll</a> but applies <a>head</a> to the resulting list
--   
--   <pre>
--   &gt;&gt;&gt; runSingle prog strm
--   10
--   </pre>
runSingle :: HasConstraint Show s => Session s (Cap ctx Eps) a -> Stream s -> a

-- | <a>run</a> cannot deal with lifted computations. This makes it limited
--   to session typed programs without any use of lift.
--   
--   This function allows us to evaluate lifted computations, but as a
--   consequence is no longer entirely pure.
runP :: HasConstraint Show s => Session s (Cap ctx Eps) a -> SessionInfo -> Stream s -> Process (Output s a)

-- | Monadic version of <a>runAll</a>.
runAllP :: HasConstraint Show s => Session s (Cap ctx Eps) a -> SessionInfo -> Stream s -> Process [a]

-- | Monad version of <a>runSingle</a>
runSingleP :: HasConstraint Show s => Session s (Cap ctx Eps) a -> SessionInfo -> Stream s -> Process a

-- | Session typed version of <a>runP</a>
runM :: HasConstraint Show s => Session s (Cap ctx Eps) a -> Stream s -> Session r r (Output s a)

-- | Session typed version of <a>runAllP</a>
runAllM :: HasConstraint Show s => Session s (Cap ctx Eps) a -> Stream s -> Session r r [a]

-- | Session typed version of <a>runSingleP</a>
runSingleM :: HasConstraint Show s => Session s (Cap ctx Eps) a -> Stream s -> Session r r a

-- | We use the <a>Stream</a> data type to supply input for the receives in
--   a session typed programs.
--   
--   We annotate a <a>Stream</a> with a capability for the following three
--   reasons:
--   
--   <ol>
--   <li>Each <a>recv</a> may return a value of a different type.</li>
--   <li>Given reason 1 and that we can have branching, we must also be
--   able to branch in the stream.</li>
--   <li>We can now write a function that recursively generates input for a
--   recursive program</li>
--   </ol>
--   
--   Similar to <a>STTerm</a>, <a>Stream</a> has a constructor for each
--   session type. Each constructor takes an argument that is another
--   <a>Stream</a> type, except for <a>S_Recv</a> that takes an additional
--   argument that will be used as input, and <a>S_Eps</a> that denotes the
--   end of the stream.
--   
--   At first it might be confusing which constructors and in what order
--   these constructors should be placed to form a <a>Stream</a> that can
--   be used as input for some <a>STTerm</a>.
--   
--   This is actually not that difficult at all. A <a>Stream</a> is session
--   typed and that session type must be equal to the session type of the
--   <a>STTerm</a>. As such one merely needs to create a <a>Stream</a> that
--   has the same session type and if you don't the type checker will tell
--   you what it incorrect.
--   
--   There are two things that you need to be aware of when constructor a
--   <a>Stream</a>.
--   
--   <ul>
--   <li>The <a>Stream</a> constructors for offering (S_OffZ and S_OffS)
--   require that you define input for all branches of the offering. This
--   can be quite cumbersome, so we include a <a>S_Off1</a> and
--   <a>S_Off2</a> constructor that behave similarly to <a>S_Sel1</a> and
--   <a>S_Sel2</a>.</li>
--   <li>You are not guaranteed that a <a>Stream</a> can be used for all
--   session typed programs that have the same session type. Specifically
--   when it comes to selection can we not guarantee this. The session type
--   for selection only tells us about which branches could be selected. It
--   does not tell us which branch was selected as this is runtime
--   dependent.</li>
--   </ul>
data Stream (a :: Cap Type) :: Cap Type -> Type
[S_Send] :: Stream (Cap Type ctx ((:!>) Type a1 s))
[S_Recv] :: Stream (Cap Type ctx ((:?>) * a1 s))
[S_Sel1] :: Stream (Cap Type ctx (Sel Type ((:) (ST Type) s xs)))
[S_Sel2] :: Stream (Cap Type ctx (Sel Type ((:) (ST Type) s ((:) (ST Type) t xs))))
[S_OffZ] :: Stream (Cap Type ctx (Off Type ((:) (ST Type) s ([] (ST Type)))))
[S_OffS] :: Stream (Cap Type ctx (Off Type ((:) (ST Type) s ((:) (ST Type) t xs))))
[S_Off1] :: Stream (Cap Type ctx (Off Type ((:) (ST Type) s xs)))
[S_Off2] :: Stream (Cap Type ctx (Off Type ((:) (ST Type) s ((:) (ST Type) t xs))))
[S_Rec] :: Stream (Cap Type ctx (R Type s))
[S_Weaken] :: Stream (Cap Type ((:) (ST Type) t ctx) (Wk Type s))
[S_Var] :: Stream (Cap Type ((:) (ST Type) s ctx) (V Type))
[S_Eps] :: Stream (Cap Type ([] (ST Type)) (Eps Type))

-- | The <a>Output</a> data type describes the session type actions that
--   were done
data Output (a :: Cap Type) b :: Cap Type -> Type -> Type
[O_Send] :: Output (Cap Type ctx ((:!>) * a1 r)) b
[O_Recv] :: Output (Cap Type ctx ((:?>) * a1 r)) b
[O_Sel1] :: Output (Cap Type ctx (Sel Type ((:) (ST Type) s xs))) b
[O_Sel2] :: Output (Cap Type ctx (Sel Type ((:) (ST Type) s xs))) b
[O_OffZ] :: Output (Cap Type ctx (Off Type ((:) (ST Type) s ([] (ST Type))))) b
[O_OffS] :: Output (Cap Type ctx (Off Type ((:) (ST Type) s ((:) (ST Type) t xs)))) b
[O_Off1] :: Output (Cap Type ctx (Off Type ((:) (ST Type) s xs))) b
[O_Off2] :: Output (Cap Type ctx (Off Type ((:) (ST Type) s ((:) (ST Type) t xs)))) b
[O_Rec] :: Output (Cap Type ctx (R Type s)) b
[O_Var] :: Output (Cap Type ((:) (ST Type) s ctx) (V Type)) b
[O_Weaken] :: Output (Cap Type ((:) (ST Type) t ctx) (Wk Type s)) b
[O_Eps] :: Output (Cap Type ctx (Eps Type)) b
[O_Lift] :: Output a b


-- | We cannot create a <a>Closure</a> of a <a>Session</a>, because its
--   type parameters are of a different kind than <a>*</a>.
--   
--   To accomedate for this drawback we define two data types that
--   existentially quantify the type parameters of a <a>Session</a>.
--   
--   We also define a set of static and closure functions for remotely
--   spawning sessions.
module Control.Distributed.Session.Closure

-- | Data type that encapsulates two sessions for the purpose of remotely
--   spawning them
--   
--   The session types of the sessions are existentially quantified, but we
--   still ensure duality and constrain them properly, such that they can
--   be passed to <a>evalSession</a>.
data SpawnSession a b
[SpawnSession] :: (HasConstraintST Serializable s, HasConstraintST Serializable (DualST s), Typeable a, Typeable b) => Session (Cap '[] s) r a -> Session (Cap '[] (DualST s)) r b -> SpawnSession a b

-- | Data type that encapsulates a single session performing no session
--   typed action that can be remotely spawned.
--   
--   We use this data type mostly for convenience in combination with
--   <a>evalSessionEq</a> allowing us to avoid the <a>Serializable</a>
--   constraint.
data SessionWrap a
[SessionWrap] :: Session s s a -> SessionWrap a

-- | RemoteTable that binds all in this module defined static functions to
--   their corresponding evaluation functions.
sessionRemoteTable :: RemoteTable -> RemoteTable

-- | Static function for remotely spawning a single session
--   
--   When remotely spawning any session we must always pass it the
--   <a>ProcessId</a> and <a>NodeId</a> of the spawning process.
--   
--   We must pass a Closure of a <a>SessionWrap</a> instead of just a
--   <a>SessionWrap</a>, because that would require serializing a
--   <a>SessionWrap</a> which is not possible.
--   
--   Furthermore, we must also pass a <a>SerializableDict</a> that shows
--   how to serialize a value of type <tt>a</tt>.
remoteSessionStatic :: Static (SerializableDict a -> Closure (SessionWrap a) -> Process a)

-- | Closure function for remotely spawning a single session
remoteSessionClosure :: Static (SerializableDict a) -> Closure (SessionWrap a) -> Closure (Process a)

-- | Same as <a>remoteSessionStatic</a>, except that we do not need to
--   provide a <a>SerializableDict</a>.
remoteSessionStatic' :: Static (Closure (SessionWrap ()) -> Process ())

-- | Same as <a>remoteSessionClosure</a>, except that we do not need to
--   provide a <a>SerializableDict</a>.
remoteSessionClosure' :: Closure (SessionWrap ()) -> Closure (Process ())

-- | A static function specific to the lifted <a>spawnChannel</a> function
--   that can be found in <a>Control.Distributed.Session.Lifted</a>
spawnChannelStatic :: Static (SerializableDict a -> Closure (ReceivePort a -> SessionWrap ()) -> ReceivePort a -> Process ())

-- | A closure specific to the lifted <a>spawnChannel</a> function that can
--   be found in <a>Control.Distributed.Session.Lifted</a>
spawnChannelClosure :: Static (SerializableDict a) -> Closure (ReceivePort a -> SessionWrap ()) -> Closure (ReceivePort a -> Process ())

-- | Function that evalutes the first argument of a <a>SpawnSession</a> in
--   a local manner.
--   
--   It is local in that we do not create an accompanying closure.
evalLocalSession :: Typeable a => (ProcessId, NodeId, Closure (SpawnSession a ())) -> Process a

-- | Static function for remotely evaluating the second argument of a
--   <a>SpawnSession</a>.
--   
--   This function works dually to <a>evalLocalSession</a>.
remoteSpawnSessionStatic :: Static (SerializableDict a -> (ProcessId, NodeId, Closure (SpawnSession a ())) -> Process ())

-- | Closure for remotely evaluating the second argument of a
--   <a>SpawnSession</a>
remoteSpawnSessionClosure :: Static (SerializableDict a) -> (ProcessId, NodeId, Closure (SpawnSession a ())) -> Closure (Process ())

-- | Same as <a>remoteSpawnSessionStatic</a>, except for that we do not
--   need to provide a <a>SerializableDict</a>.
remoteSpawnSessionStatic' :: Static ((ProcessId, NodeId, Closure (SpawnSession () ())) -> Process ())

-- | Same as <a>remoteSpawnSessionClosure</a>, except for that we do not
--   need to provide a <a>SerializableDict</a>.
remoteSpawnSessionClosure' :: (ProcessId, NodeId, Closure (SpawnSession () ())) -> Closure (Process ())

-- | Static function for remotely evaluating the second argument of a
--   <a>SpawnSession</a>
--   
--   This function is very similar to <a>remoteSpawnSessionStatic'</a>. The
--   difference is that this function assumes that the other session was
--   also remotely spawned.
--   
--   Therefore we require an extra send of the <a>ProcessId</a> of the to
--   be spawned process.
rrSpawnSessionSendStatic :: Static ((ProcessId, NodeId, Closure (SpawnSession () ())) -> Process ())

-- | Closure for remotely evaluating the second argument of a
--   <a>SpawnSession</a>.
rrSpawnSessionSendClosure :: (ProcessId, NodeId, Closure (SpawnSession () ())) -> Closure (Process ())

-- | Closure for remotely evaluating the first argument of a
--   <a>SpawnSession</a>
--   
--   This function acts dual to <a>rrSpawnSessionSend</a> and assumes that
--   it will first receive a <a>ProcessId</a>.
rrSpawnSessionExpectStatic :: Static ((NodeId, Closure (SpawnSession () ())) -> Process ())

-- | Closure for remotely evaluating the first argument of a
--   <a>SpawnSession</a>.
rrSpawnSessionExpectClosure :: (NodeId, Closure (SpawnSession () ())) -> Closure (Process ())


-- | In this module we lift all functions in
--   <a>Control.Distributed.Process</a> that return a function of type
--   Process a to Session s s a.
--   
--   Since the functions in this module work identical to the ones in
--   <a>Control.Distributed.Process</a> we will refer to that module for
--   documentation.
--   
--   There is however some explanation required for functions that take a
--   <tt>Process</tt> as an argument.
--   
--   For the functions that also take a Process a as an argument we derive
--   two functions. One that still takes a Process a and one that takes a
--   Session s s a.
--   
--   There are also functions that take a Closure (Process ()) as an
--   argument. We cannot lift this to be Closure (Session s s ()) as is
--   explained in <a>Control.Distributed.Session.Closure</a>.
--   
--   To accomodate for this drawback we instead have these functions take a
--   Closure (SessionWrap ()) as an argument.
--   
--   Here is an example on how to call <a>call</a>.
--   
--   <pre>
--   {-# LANGUAGE TemplateHaskell #-}
--   import qualified SessionTypes.Indexed as I
--   import Control.Distributed.Session (SessionWrap(..), sessionRemoteTable, call, evalSessionEq)
--   import Control.Distributed.Process (liftIO, Process, RemoteTable, NodeId)
--   import Control.Distributed.Process.Serializable (SerializableDict(..))
--   import Control.Distributed.Process.Closure (remotable, mkStaticClosure, mkStatic)
--   import Control.Distributed.Process.Node
--   import Network.Transport.TCP
--   
--   sessWrap :: SessionWrap Int
--   sessWrap = SessionWrap $ I.return 5
--   
--   sdictInt :: SerializableDict Int
--   sdictInt = SerializableDict
--   
--   remotable ['sdictInt, 'sessWrap]
--   
--   p1 :: NodeId -&gt; Process ()
--   p1 nid = do
--     a &lt;- evalSessionEq (call $(mkStatic 'sdictInt) nid $(mkStaticClosure 'sessWrap))
--     liftIO $ putStrLn $ show a
--   
--   myRemoteTable :: RemoteTable
--   myRemoteTable = Main.__remoteTable $ sessionRemoteTable initRemoteTable
--   
--   main :: IO ()
--   main = do
--     Right t &lt;- createTransport "127.0.0.1" "100000" defaultTCPParameters
--     node &lt;- newLocalNode t myRemoteTable
--     runProcess node $ p1 (localNodeId node)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; main
--   &gt; 5
--   </pre>
--   
--   In p1 we run a session that makes a call and then prints out the
--   result of that call.
--   
--   Note that this is the call function from
--   <a>SessionTyped.Distributed.Process.Lifted</a>. It takes a Static
--   (SerializableDict a) and a Closure (SessionWrap a).
--   
--   To create a static serializable dictionary we first have to define a
--   function that returns a monomorphic serializable dictionary.
--   
--   <pre>
--   sdictInt :: SerializableDict Int
--   sdictInt = SerializableDict
--   </pre>
--   
--   We then pass 'sdictInt to remoteable, which is a top-level Template
--   Haskell splice.
--   
--   <pre>
--   remoteable ['sdictInt]
--   </pre>
--   
--   Now we can create a static serializable dictionary with
--   
--   <pre>
--   $(mkStatic 'sdictInt)
--   </pre>
--   
--   To create a closure for a Session s s we have to wrap it in a
--   <a>SessionWrap</a>.
--   
--   <pre>
--   sessWrap :: SessionWrap Int
--   sessWrap = SessionWrap $ I.return 5
--   </pre>
--   
--   Similarly to sdictInt this needs to be a top level definition such
--   that we can use Template Haskell to derive a Closure
--   
--   <pre>
--   remotable ['sdictInt, 'sessWrap]
--   $(mkStaticClosure 'sessWrap)
--   </pre>
--   
--   Since <a>call</a> makes use of internally defined closures, you also
--   have to include <a>sessionRemoteTable</a>.
--   
--   <pre>
--   myRemoteTable = Main.__remoteTable $ sessionRemoteTable initRemoteTable
--   </pre>
--   
--   The remote tables contains a mapping from labels to evaluation
--   functions that a node uses to evaluate closures.
--   
--   <pre>
--   node &lt;- newLocalNode t myRemoteTable
--   </pre>
module Control.Distributed.Session.Lifted

-- | Unsession typed send
utsend :: Serializable a => ProcessId -> a -> Session s s ()

-- | Unsafe send
usend :: Serializable a => ProcessId -> a -> Session s s ()
expect :: Serializable a => Session s s a
expectTimeout :: Serializable a => Int -> Session s s (Maybe a)
newChan :: Serializable a => Session s s (SendPort a, ReceivePort a)
sendChan :: Serializable a => SendPort a -> a -> Session s s ()
receiveChan :: Serializable a => ReceivePort a -> Session s s a
receiveChanTimeout :: Serializable a => Int -> ReceivePort a -> Session s s (Maybe a)
mergePortsBiased :: Serializable a => [ReceivePort a] -> Session s s (ReceivePort a)
mergePortsRR :: Serializable a => [ReceivePort a] -> Session s s (ReceivePort a)
unsafeSend :: Serializable a => ProcessId -> a -> Session s s ()
unsafeSendChan :: Serializable a => SendPort a -> a -> Session s s ()
unsafeNSend :: Serializable a => String -> a -> Session s s ()
unsafeNSendRemote :: Serializable a => NodeId -> String -> a -> Session s s ()
receiveWait :: [Match b] -> Session s s b
receiveTimeout :: Int -> [Match b] -> Session s s (Maybe b)
unwrapMessage :: Serializable a => Message -> Session s s (Maybe a)
handleMessage :: Serializable a => Message -> (a -> Session s s b) -> Session r r (Maybe b)
handleMessage_ :: Serializable a => Message -> (a -> Session s s ()) -> Session r r ()
handleMessageP :: Serializable a => Message -> (a -> Process b) -> Session s s (Maybe b)
handleMessageP_ :: Serializable a => Message -> (a -> Process ()) -> Session s s ()
handleMessageIf :: Serializable a => Message -> (a -> Bool) -> (a -> Session s s b) -> Session r r (Maybe b)
handleMessageIf_ :: Serializable a => Message -> (a -> Bool) -> (a -> Session s s ()) -> Session r r ()
handleMessageIfP :: Serializable a => Message -> (a -> Bool) -> (a -> Process b) -> Session s s (Maybe b)
handleMessageIfP_ :: Serializable a => Message -> (a -> Bool) -> (a -> Process ()) -> Session s s ()
forward :: Message -> ProcessId -> Session s s ()
uforward :: Message -> ProcessId -> Session s s ()
delegate :: ProcessId -> (Message -> Bool) -> Session s s ()
relay :: ProcessId -> Session s s ()
proxy :: Serializable a => ProcessId -> (a -> Session s s Bool) -> Session r r ()
proxyP :: Serializable a => ProcessId -> (a -> Process Bool) -> Session s s ()
spawn :: NodeId -> Closure (SessionWrap ()) -> Session s s ProcessId
spawnP :: NodeId -> Closure (Process ()) -> Session s s ProcessId
call :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (SessionWrap a) -> Session r r a
callP :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (Process a) -> Session s s a
terminate :: Session s s a
die :: Serializable a => a -> Session s s b
kill :: ProcessId -> String -> Session s s ()
exit :: Serializable a => ProcessId -> a -> Session s s ()
catchExit :: (Show a, Serializable a) => Session s s b -> (ProcessId -> a -> Session r r b) -> Session t t b
catchExitP :: (Show a, Serializable a) => Process b -> (ProcessId -> a -> Process b) -> Session s s b
catchesExit :: Session s s b -> [ProcessId -> Message -> Session r r (Maybe b)] -> Session t t b
catchesExitP :: Process b -> [ProcessId -> Message -> Process (Maybe b)] -> Session s s b
getSelfPid :: Session s s ProcessId
getSelfNode :: Session s s NodeId
getOthPid :: Session s s (Maybe ProcessId)
getOthNode :: Session s s (Maybe NodeId)
getProcessInfo :: ProcessId -> Session s s (Maybe ProcessInfo)
getNodeStats :: NodeId -> Session s s (Either DiedReason NodeStats)
link :: ProcessId -> Session s s ()
linkNode :: NodeId -> Session s s ()
unlink :: ProcessId -> Session s s ()
unlinkNode :: NodeId -> Session s s ()
monitor :: ProcessId -> Session s s MonitorRef
monitorNode :: NodeId -> Session s s MonitorRef
monitorPort :: Serializable a => SendPort a -> Session s s MonitorRef
unmonitor :: MonitorRef -> Session s s ()
withMonitor :: ProcessId -> (MonitorRef -> Session s s a) -> Session r r a
withMonitor_ :: ProcessId -> Session s s a -> Session r r a
withMonitorP :: ProcessId -> (MonitorRef -> Process a) -> Session s s a
withMonitorP_ :: ProcessId -> Process a -> Session s s a
unStatic :: Typeable a => Static a -> Session s s a
unClosure :: Typeable a => Closure a -> Session s s a
say :: String -> Session s s ()
register :: String -> ProcessId -> Session s s ()
unregister :: String -> Session s s ()
whereis :: String -> Session s s (Maybe ProcessId)
nsend :: Serializable a => String -> a -> Session s s ()
registerRemoteAsync :: NodeId -> String -> ProcessId -> Session s s ()
reregisterRemoteAsync :: NodeId -> String -> ProcessId -> Session s s ()
whereisRemoteAsync :: NodeId -> String -> Session s s ()
nsendRemote :: Serializable a => NodeId -> String -> a -> Session s s ()
spawnAsync :: NodeId -> Closure (SessionWrap ()) -> Session r r SpawnRef
spawnAsyncP :: NodeId -> Closure (Process ()) -> Session s s SpawnRef
spawnSupervised :: NodeId -> Closure (SessionWrap ()) -> Session s s (ProcessId, MonitorRef)
spawnSupervisedP :: NodeId -> Closure (Process ()) -> Session s s (ProcessId, MonitorRef)
spawnLink :: NodeId -> Closure (SessionWrap ()) -> Session s s ProcessId
spawnLinkP :: NodeId -> Closure (Process ()) -> Session s s ProcessId
spawnMonitor :: NodeId -> Closure (SessionWrap ()) -> Session s s (ProcessId, MonitorRef)
spawnMonitorP :: NodeId -> Closure (Process ()) -> Session s s (ProcessId, MonitorRef)
spawnChannel :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (ReceivePort a -> SessionWrap ()) -> Session s s (SendPort a)
spawnChannelP :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (ReceivePort a -> Process ()) -> Session s s (SendPort a)
spawnLocal :: Session s s () -> Session r r ProcessId
spawnLocalP :: Process () -> Session s s ProcessId
spawnChannelLocal :: Serializable a => (ReceivePort a -> Session s s ()) -> Session r r (SendPort a)
spawnChannelLocalP :: Serializable a => (ReceivePort a -> Process ()) -> Session s s (SendPort a)
callLocal :: Session s s a -> Session s s a
callLocalP :: Process a -> Session s s a
reconnect :: ProcessId -> Session s s ()
reconnectPort :: SendPort a -> Session s s ()


-- | Defines several combinators for spawning sessions
--   
--   Here we define a session to be two dual <a>Session</a>s that together
--   implement a protocol described by a session type.
--   
--   The following shows an example of how to spawn a session
--   
--   <pre>
--   {-# LANGUAGE TemplateHaskell #-}
--   {-# LANGUAGE DataKinds #-}
--   {-# LANGUAGE TypeOperators #-}
--   
--   import qualified SessionTypes.Indexed as I
--   import Control.Distributed.Session hiding (getSelfPid, expect)
--   import Control.Distributed.Process (liftIO, Process, RemoteTable, NodeId, getSelfPid, ProcessId, expect)
--   import Control.Distributed.Process.Closure (remotable, mkClosure)
--   import Control.Distributed.Process.Node
--   import Network.Transport.TCP
--   
--   sess1 :: Session ('Cap '[] (Int :!&gt; Eps)) ('Cap '[] Eps) ()
--   sess1 = send 5 I.&gt;&gt; eps ()
--   
--   sess2 :: ProcessId -&gt; Session ('Cap '[] (Int :?&gt; Eps)) ('Cap '[] Eps) ()
--   sess2 pid = recv I.&gt;&gt;= x -&gt; utsend pid x I.&gt;&gt;= eps
--   
--   spawnSess :: ProcessId -&gt; SpawnSession () ()
--   spawnSess pid = SpawnSession sess1 (sess2 pid)
--   
--   remotable ['spawnSess]
--   
--   p1 :: NodeId -&gt; Process ()
--   p1 nid = do
--     pid &lt;- getSelfPid
--     spawnRRSessionP nid nid ($(mkClosure 'spawnSess) pid)
--     a &lt;- expect :: Process Int
--     liftIO (putStrLn $ show a)
--   
--   myRemoteTable :: RemoteTable
--   myRemoteTable = Main.__remoteTable $ sessionRemoteTable initRemoteTable
--   
--   main :: IO ()
--   main = do
--     Right t &lt;- createTransport "127.0.0.1" "100000" defaultTCPParameters
--     node &lt;- newLocalNode t myRemoteTable
--     runProcess node $ p1 (localNodeId node)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; main
--   &gt; 5
--   </pre>
--   
--   In p1 we spawn a session that consists of two <a>Session</a>s that are
--   remotely spawned (which happens to be the local node).
--   
--   We do so using the <a>spawnRRSessionP</a> function that we can call
--   within a <a>Process</a>. We pass it the two node identifiers followed
--   by a closure that takes an argument.
--   
--   Sess1 and sess2 implement both sides of the protocol. We can insert
--   these into a <a>SpawnSession</a>, because they are dual to each other.
--   
--   <pre>
--   spawnSess :: ProcessId -&gt; SpawnSession () ()
--   spawnSess pid = SpawnSession sess1 (sess2 pid)
--   </pre>
--   
--   Then to create a closure for <tt>spawnSess</tt> that we can then pass
--   to <a>spawnRRSessionP</a> we first add <tt>spawnSess</tt> to the
--   remotable of the current module.
--   
--   <pre>
--   remotable ['spawnSess]
--   </pre>
--   
--   remotable is a top-level Template Haskell splice that creates a
--   closure function for us.
--   
--   To use this closure function we can simply do
--   
--   <pre>
--   $(mkClosure 'spawnSess) pid
--   </pre>
--   
--   We use <tt>mkClosure</tt> such that we can still pass an argument to
--   spawnSess with the result being of type Closure (SpawnSession () ())
--   
--   It is important that the node that we run p1 on knows how to evaluate
--   a closure of type Closure (SpawnSession () ()). This requires that we
--   compose the initRemoteTable of a node with the remotable of this
--   module.
--   
--   Within <a>spawnRRSessionP</a> we make use of internally defined
--   closures. The library therefore exports <a>sessionRemoteTable</a> that
--   should always be passed to a node if you make use of a function within
--   this library that takes a closure as an argument.
--   
--   <pre>
--   myRemoteTable :: RemoteTable
--   myRemoteTable = Main.__remoteTable $ sessionRemoteTable initRemoteTable
--   </pre>
--   
--   <pre>
--   node &lt;- newLocalNode t myRemoteTable
--   </pre>
module Control.Distributed.Session.Spawn

-- | Calls a local session consisting of two dual <a>Session</a>s.
--   
--   Spawns a new local process for the second <a>Session</a> and runs the
--   first <a>Session</a> on the current process.
--   
--   Returns the result of the first <a>Session</a> and the
--   <a>ProcessId</a> of the second <a>Session</a>.
callLocalSessionP :: (HasConstraint Serializable s, HasConstraint Serializable (Dual s)) => Session s r a -> Session (Dual s) r b -> Process (a, ProcessId)

-- | Sessioned version of <a>callLocalSessionP</a>
callLocalSession :: (HasConstraint Serializable s, HasConstraint Serializable (Dual s)) => Session s r a -> Session (Dual s) r b -> Session k k (a, ProcessId)

-- | Calls a remote session consisting of two dual <a>Session</a>s.
--   
--   Spawns a remote process for the second <a>Session</a> and runs the
--   first <a>Session</a> on the current process.
--   
--   Returns the result of the frist <a>Session</a> and the
--   <a>ProcessId</a> of the second <a>Session</a>.
--   
--   The arguments of this function are described as follows:
--   
--   <ul>
--   <li>Static (SerializableDict a): Describes how to serialize a value of
--   type <tt>a</tt></li>
--   <li>NodeId: The node identifier of the node that the second
--   <a>Session</a> should be spawned to.</li>
--   <li>Closure (SpawnSession a ()): A closure of a wrapper over two dual
--   <a>Session</a>s.</li>
--   </ul>
--   
--   Requires <a>sessionRemoteTable</a>
callRemoteSessionP :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (SpawnSession a ()) -> Process (a, ProcessId)

-- | Sessioned version of <a>callRemoteSession</a>
--   
--   Requires <a>sessionRemoteTable</a>
callRemoteSession :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (SpawnSession a ()) -> Session k k (a, ProcessId)

-- | Same as <a>callRemoteSessionP</a>, but we no longer need to provide a
--   static serializable dictionary, because the result type of the first
--   session is unit.
--   
--   Requires <a>sessionRemoteTable</a>
callRemoteSessionP' :: NodeId -> Closure (SpawnSession () ()) -> Process (ProcessId)

-- | Sessioned version of <a>callRemoteSessionP'</a>
--   
--   Requires <a>sessionRemoteTable</a>
callRemoteSession' :: NodeId -> Closure (SpawnSession () ()) -> Session s s (ProcessId)

-- | Spawns a local session.
--   
--   Both <a>Session</a>s are spawned locally.
--   
--   Returns the <a>ProcessId</a> of both spawned processes.
spawnLLSessionP :: (HasConstraint Serializable s, HasConstraint Serializable (Dual s)) => Session s r a -> Session (Dual s) r b -> Process (ProcessId, ProcessId)

-- | Sessioned version of <a>spawnLLSession</a>
spawnLLSession :: (HasConstraint Serializable s, HasConstraint Serializable (Dual s)) => Session s r a -> Session (Dual s) r b -> Session t t (ProcessId, ProcessId)

-- | Spawns one <a>Session</a> local and spawns another <a>Session</a>
--   remote.
--   
--   Returns the <a>ProcessId</a> of both spawned processes.
--   
--   The arguments are described as follows:
--   
--   <ul>
--   <li>NodeId: The node identifier of the node that the second
--   <a>Session</a> should be spawned to.</li>
--   <li>Closure (SpawnSession () ()): A closure of a wrapper over two dual
--   <a>Session</a>s.</li>
--   </ul>
--   
--   Requires <a>sessionRemoteTable</a>
spawnLRSessionP :: NodeId -> Closure (SpawnSession () ()) -> Process (ProcessId, ProcessId)

-- | Sessioned version of <a>spawnLRSessionP</a>
--   
--   Requires <a>sessionRemoteTable</a>
spawnLRSession :: NodeId -> Closure (SpawnSession () ()) -> Session s s (ProcessId, ProcessId)

-- | Spawns a remote session. Both <a>Session</a> arguments are spawned
--   remote.
--   
--   Returns the <a>ProcessId</a> of both spawned processes.
--   
--   The arguments are described as follows:
--   
--   <ul>
--   <li>NodeId: The node identifier of the node that the first
--   <a>Session</a> should be spawned to.</li>
--   <li>NodeId: The node identifier of the node that the second
--   <a>Session</a> should be spawned to.</li>
--   <li>Closure (SpawnSession () ()): A closure of a wrapper over two dual
--   <a>Session</a>s.</li>
--   </ul>
--   
--   Requires <a>sessionRemoteTable</a>
spawnRRSessionP :: NodeId -> NodeId -> Closure (SpawnSession () ()) -> Process (ProcessId, ProcessId)

-- | Sessioned version of <tt>SpawnRRSession</tt>
--   
--   Requires <a>sessionRemoteTable</a>
spawnRRSession :: NodeId -> NodeId -> Closure (SpawnSession () ()) -> Session s s (ProcessId, ProcessId)


-- | This package defines a wrapper over the sessiontypes library that
--   allows for evaluating session typed programs to Cloud Haskell
--   programs.
--   
--   The goal of this library is to allow a user to define two dual session
--   typed programs, spawn two processes and have these processes evaluate
--   the programs.
--   
--   Session types guarantee that the resulting Cloud Haskell programs
--   correctly implement the protocol and that they are non-deadlocking.
--   
--   We define a session typed program with an indexed monad <a>Session</a>
--   that is both a reader monad and a wrapper over a <a>STTerm</a> that
--   uses <tt>Process</tt> as its underlying monad.
--   
--   This module exports the most important parts of this library:
--   
--   <ul>
--   <li><a>Control.Distributed.Session.Session</a>: Defines the
--   <a>Session</a> monad and <a>SessionInfo</a> that is used as the
--   environment of <a>Session</a>.</li>
--   <li><a>Control.Distributed.Session.Eval</a>: Defines the interpreter
--   for evaluation a <a>Session</a> to a <tt>Process</tt>.</li>
--   <li><a>Control.Distributed.Session.Spawn</a>: Defines several
--   combinators for spawning sessions.</li>
--   <li><a>Control.Distributed.Session.Closure</a>: Module for
--   constructing closures of sessions.</li>
--   <li><a>Control.Distributed.Session.STChannel</a>: Session typed
--   channel that allows for transmitting values of different types.</li>
--   <li><a>Control.Distributed.Session.Lifted</a>: Exports lifted
--   functions from the distributed-process package.</li>
--   </ul>
--   
--   Additionally we defined wrappers for using the interpreters defined in
--   the sessiontypes package on a <a>Session</a>:
--   
--   <ul>
--   <li><a>Control.Distributed.Session.Debug</a></li>
--   <li><a>Control.Distributed.Session.Interactive</a></li>
--   <li><a>Control.Distributed.Session.Normalize</a></li>
--   <li><a>Control.Distributed.Session.Visualize</a></li>
--   </ul>
module Control.Distributed.Session

-- | <a>Session</a> is defined as a newtype wrapper over a function that
--   takes a `Maybe SessionInfo` and returns an indexed codensity monad
--   transformer over the <a>Process</a> monad.
--   
--   <a>Session</a> is also a reader monad that has a Maybe SessionInfo as
--   its environment. <a>SessionInfo</a> is wrapped in a <a>Maybe</a>,
--   because we also allow a session to be run singularly. In which case
--   there is no other Session to communicate with and therefore is there
--   also no need for a <a>SessionInfo</a>.
--   
--   The function returns the indexed codensity monad and not simply a
--   <a>STTerm</a>, because from benchmarking the codensity monad gave us
--   significant performance improvements for free.
newtype Session s r a
Session :: (Maybe SessionInfo -> IxC Process s r a) -> Session s r a
[runSessionC] :: Session s r a -> Maybe SessionInfo -> IxC Process s r a

-- | The SessionInfo data type tells us information about another
--   <a>Session</a>. Namely, the <a>Session</a> that is in a session with
--   the <a>Session</a> that this specific <a>SessionInfo</a> belongs to.
data SessionInfo
SessionInfo :: ProcessId -> NodeId -> UTChan -> SessionInfo

-- | The <a>ProcessId</a> of the dual <a>Session</a>
[othPid] :: SessionInfo -> ProcessId

-- | The <a>NodeId</a> of the <tt>Node</tt> that the dual <a>Session</a>
--   runs on
[othNode] :: SessionInfo -> NodeId

-- | A send port belonging to the dual <a>Session</a>, such that we can
--   send messages to it. And a receive port of which the dual
--   <a>Session</a> has its send port, such that we can receive messages
--   from the dual <a>Session</a>.
[utchan] :: SessionInfo -> UTChan

-- | Evaluates a session to a <a>STTerm</a>
runSession :: Session s r a -> Maybe SessionInfo -> STTerm Process s r a

-- | Lifts a <a>Process</a> computation
liftP :: Process a -> Session s s a

-- | Lifts a <a>STTerm</a> computation
liftST :: STTerm Process s r a -> Session s r a

-- | Calls a local session consisting of two dual <a>Session</a>s.
--   
--   Spawns a new local process for the second <a>Session</a> and runs the
--   first <a>Session</a> on the current process.
--   
--   Returns the result of the first <a>Session</a> and the
--   <a>ProcessId</a> of the second <a>Session</a>.
callLocalSessionP :: (HasConstraint Serializable s, HasConstraint Serializable (Dual s)) => Session s r a -> Session (Dual s) r b -> Process (a, ProcessId)

-- | Sessioned version of <a>callLocalSessionP</a>
callLocalSession :: (HasConstraint Serializable s, HasConstraint Serializable (Dual s)) => Session s r a -> Session (Dual s) r b -> Session k k (a, ProcessId)

-- | Calls a remote session consisting of two dual <a>Session</a>s.
--   
--   Spawns a remote process for the second <a>Session</a> and runs the
--   first <a>Session</a> on the current process.
--   
--   Returns the result of the frist <a>Session</a> and the
--   <a>ProcessId</a> of the second <a>Session</a>.
--   
--   The arguments of this function are described as follows:
--   
--   <ul>
--   <li>Static (SerializableDict a): Describes how to serialize a value of
--   type <tt>a</tt></li>
--   <li>NodeId: The node identifier of the node that the second
--   <a>Session</a> should be spawned to.</li>
--   <li>Closure (SpawnSession a ()): A closure of a wrapper over two dual
--   <a>Session</a>s.</li>
--   </ul>
--   
--   Requires <a>sessionRemoteTable</a>
callRemoteSessionP :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (SpawnSession a ()) -> Process (a, ProcessId)

-- | Sessioned version of <a>callRemoteSession</a>
--   
--   Requires <a>sessionRemoteTable</a>
callRemoteSession :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (SpawnSession a ()) -> Session k k (a, ProcessId)

-- | Same as <a>callRemoteSessionP</a>, but we no longer need to provide a
--   static serializable dictionary, because the result type of the first
--   session is unit.
--   
--   Requires <a>sessionRemoteTable</a>
callRemoteSessionP' :: NodeId -> Closure (SpawnSession () ()) -> Process (ProcessId)

-- | Sessioned version of <a>callRemoteSessionP'</a>
--   
--   Requires <a>sessionRemoteTable</a>
callRemoteSession' :: NodeId -> Closure (SpawnSession () ()) -> Session s s (ProcessId)

-- | Spawns a local session.
--   
--   Both <a>Session</a>s are spawned locally.
--   
--   Returns the <a>ProcessId</a> of both spawned processes.
spawnLLSessionP :: (HasConstraint Serializable s, HasConstraint Serializable (Dual s)) => Session s r a -> Session (Dual s) r b -> Process (ProcessId, ProcessId)

-- | Sessioned version of <a>spawnLLSession</a>
spawnLLSession :: (HasConstraint Serializable s, HasConstraint Serializable (Dual s)) => Session s r a -> Session (Dual s) r b -> Session t t (ProcessId, ProcessId)

-- | Spawns one <a>Session</a> local and spawns another <a>Session</a>
--   remote.
--   
--   Returns the <a>ProcessId</a> of both spawned processes.
--   
--   The arguments are described as follows:
--   
--   <ul>
--   <li>NodeId: The node identifier of the node that the second
--   <a>Session</a> should be spawned to.</li>
--   <li>Closure (SpawnSession () ()): A closure of a wrapper over two dual
--   <a>Session</a>s.</li>
--   </ul>
--   
--   Requires <a>sessionRemoteTable</a>
spawnLRSessionP :: NodeId -> Closure (SpawnSession () ()) -> Process (ProcessId, ProcessId)

-- | Sessioned version of <a>spawnLRSessionP</a>
--   
--   Requires <a>sessionRemoteTable</a>
spawnLRSession :: NodeId -> Closure (SpawnSession () ()) -> Session s s (ProcessId, ProcessId)

-- | Spawns a remote session. Both <a>Session</a> arguments are spawned
--   remote.
--   
--   Returns the <a>ProcessId</a> of both spawned processes.
--   
--   The arguments are described as follows:
--   
--   <ul>
--   <li>NodeId: The node identifier of the node that the first
--   <a>Session</a> should be spawned to.</li>
--   <li>NodeId: The node identifier of the node that the second
--   <a>Session</a> should be spawned to.</li>
--   <li>Closure (SpawnSession () ()): A closure of a wrapper over two dual
--   <a>Session</a>s.</li>
--   </ul>
--   
--   Requires <a>sessionRemoteTable</a>
spawnRRSessionP :: NodeId -> NodeId -> Closure (SpawnSession () ()) -> Process (ProcessId, ProcessId)

-- | Sessioned version of <tt>SpawnRRSession</tt>
--   
--   Requires <a>sessionRemoteTable</a>
spawnRRSession :: NodeId -> NodeId -> Closure (SpawnSession () ()) -> Session s s (ProcessId, ProcessId)

-- | This function unpacks a <a>Session</a> to a <a>STTerm</a> using a
--   given <a>SessionInfo</a>.
--   
--   It then evaluates the <a>STTerm</a> by mapping Cloud Haskell semantics
--   to each constructor of <a>STTerm</a>.
--   
--   The function relies on that there exists another session (on a
--   different process) that is also being evaluated (using evalSession)
--   and acts as the dual the session that function is now evaluating.
--   
--   The underlying communication method is a session typed channel
--   (<a>STChannelT</a>). There should be no interference from other
--   processes, unless you go through the effort of sharing the send port.
evalSession :: forall s r a. HasConstraint Serializable s => Session s r a -> SessionInfo -> Process a

-- | Similar to <a>evalSession</a>, except for that it does not evaluate
--   session typed actions.
--   
--   Only returns and lifted computations are evaluated. This also means
--   that there does not need to be a dual session that is evaluated on a
--   different process.
--   
--   It also assumes that <a>SessionInfo</a> is not used. Use
--   <a>evalSessionEq'</a> if this is not the case.
evalSessionEq :: Session s s a -> Process a

-- | Same as <a>evalSessionEq</a>, but you may now provide a
--   <a>SessionInfo</a>.
evalSessionEq' :: Session s s a -> SessionInfo -> Process a

-- | Data type that encapsulates two sessions for the purpose of remotely
--   spawning them
--   
--   The session types of the sessions are existentially quantified, but we
--   still ensure duality and constrain them properly, such that they can
--   be passed to <a>evalSession</a>.
data SpawnSession a b
[SpawnSession] :: (HasConstraintST Serializable s, HasConstraintST Serializable (DualST s), Typeable a, Typeable b) => Session (Cap '[] s) r a -> Session (Cap '[] (DualST s)) r b -> SpawnSession a b

-- | Data type that encapsulates a single session performing no session
--   typed action that can be remotely spawned.
--   
--   We use this data type mostly for convenience in combination with
--   <a>evalSessionEq</a> allowing us to avoid the <a>Serializable</a>
--   constraint.
data SessionWrap a
[SessionWrap] :: Session s s a -> SessionWrap a

-- | RemoteTable that binds all in this module defined static functions to
--   their corresponding evaluation functions.
sessionRemoteTable :: RemoteTable -> RemoteTable

-- | Static function for remotely spawning a single session
--   
--   When remotely spawning any session we must always pass it the
--   <a>ProcessId</a> and <a>NodeId</a> of the spawning process.
--   
--   We must pass a Closure of a <a>SessionWrap</a> instead of just a
--   <a>SessionWrap</a>, because that would require serializing a
--   <a>SessionWrap</a> which is not possible.
--   
--   Furthermore, we must also pass a <a>SerializableDict</a> that shows
--   how to serialize a value of type <tt>a</tt>.
remoteSessionStatic :: Static (SerializableDict a -> Closure (SessionWrap a) -> Process a)

-- | Closure function for remotely spawning a single session
remoteSessionClosure :: Static (SerializableDict a) -> Closure (SessionWrap a) -> Closure (Process a)

-- | Same as <a>remoteSessionStatic</a>, except that we do not need to
--   provide a <a>SerializableDict</a>.
remoteSessionStatic' :: Static (Closure (SessionWrap ()) -> Process ())

-- | Same as <a>remoteSessionClosure</a>, except that we do not need to
--   provide a <a>SerializableDict</a>.
remoteSessionClosure' :: Closure (SessionWrap ()) -> Closure (Process ())

-- | A static function specific to the lifted <a>spawnChannel</a> function
--   that can be found in <a>Control.Distributed.Session.Lifted</a>
spawnChannelStatic :: Static (SerializableDict a -> Closure (ReceivePort a -> SessionWrap ()) -> ReceivePort a -> Process ())

-- | A closure specific to the lifted <a>spawnChannel</a> function that can
--   be found in <a>Control.Distributed.Session.Lifted</a>
spawnChannelClosure :: Static (SerializableDict a) -> Closure (ReceivePort a -> SessionWrap ()) -> Closure (ReceivePort a -> Process ())

-- | Function that evalutes the first argument of a <a>SpawnSession</a> in
--   a local manner.
--   
--   It is local in that we do not create an accompanying closure.
evalLocalSession :: Typeable a => (ProcessId, NodeId, Closure (SpawnSession a ())) -> Process a

-- | Static function for remotely evaluating the second argument of a
--   <a>SpawnSession</a>.
--   
--   This function works dually to <a>evalLocalSession</a>.
remoteSpawnSessionStatic :: Static (SerializableDict a -> (ProcessId, NodeId, Closure (SpawnSession a ())) -> Process ())

-- | Closure for remotely evaluating the second argument of a
--   <a>SpawnSession</a>
remoteSpawnSessionClosure :: Static (SerializableDict a) -> (ProcessId, NodeId, Closure (SpawnSession a ())) -> Closure (Process ())

-- | Same as <a>remoteSpawnSessionStatic</a>, except for that we do not
--   need to provide a <a>SerializableDict</a>.
remoteSpawnSessionStatic' :: Static ((ProcessId, NodeId, Closure (SpawnSession () ())) -> Process ())

-- | Same as <a>remoteSpawnSessionClosure</a>, except for that we do not
--   need to provide a <a>SerializableDict</a>.
remoteSpawnSessionClosure' :: (ProcessId, NodeId, Closure (SpawnSession () ())) -> Closure (Process ())

-- | Static function for remotely evaluating the second argument of a
--   <a>SpawnSession</a>
--   
--   This function is very similar to <a>remoteSpawnSessionStatic'</a>. The
--   difference is that this function assumes that the other session was
--   also remotely spawned.
--   
--   Therefore we require an extra send of the <a>ProcessId</a> of the to
--   be spawned process.
rrSpawnSessionSendStatic :: Static ((ProcessId, NodeId, Closure (SpawnSession () ())) -> Process ())

-- | Closure for remotely evaluating the second argument of a
--   <a>SpawnSession</a>.
rrSpawnSessionSendClosure :: (ProcessId, NodeId, Closure (SpawnSession () ())) -> Closure (Process ())

-- | Closure for remotely evaluating the first argument of a
--   <a>SpawnSession</a>
--   
--   This function acts dual to <a>rrSpawnSessionSend</a> and assumes that
--   it will first receive a <a>ProcessId</a>.
rrSpawnSessionExpectStatic :: Static ((NodeId, Closure (SpawnSession () ())) -> Process ())

-- | Closure for remotely evaluating the first argument of a
--   <a>SpawnSession</a>.
rrSpawnSessionExpectClosure :: (NodeId, Closure (SpawnSession () ())) -> Closure (Process ())

-- | Basic message type that existentially quantifies the content of the
--   message
data Message
Message :: a -> Message

-- | Session typed send port as a wrapper over SendPort Message. It is
--   parameterized with a capability/sessiontype.
data STSendPort (l :: Cap Type)
STSendPort :: (SendPort Message) -> STSendPort

-- | Session typed receive port as a wrapper over ReceivePort Message. It
--   is parameterized with a capability/sessiontype.
data STReceivePort (l :: Cap Type)
STReceivePort :: (ReceivePort Message) -> STReceivePort

-- | Type synonym for a session typed channel given a single session type
--   
--   This removes recv session types from the given session type as it is
--   passed to the send port type
--   
--   Also removes send session types from the given session type as it is
--   passed to the receive port type
type STChan s = (STSendPort (RemoveRecv s), STReceivePort (RemoveSend s))

-- | Same as <a>STChan</a>, but it is given a session type for the send
--   port type and a separate session type for the receive port type
type STChanBi s r = (STSendPort (RemoveRecv s), STReceivePort (RemoveSend r))

-- | Unsession typed typed channel
--   
--   It is essentially just a typed channel that is parameterized with
--   <a>Message</a>.
--   
--   We can carry around this type in <tt>Session</tt>, but not a
--   <a>STChan</a>.
type UTChan = (SendPort Message, ReceivePort Message)

-- | Creates a new session typed channel given a single session type
newSTChan :: Proxy s -> Process (STChan s)

-- | Creates a new session typed channel given separate session types for
--   the send port and receive port
newSTChanBi :: Proxy s -> Proxy r -> Process (STChanBi s r)

-- | Creates an unsession typed channel
newUTChan :: Process UTChan

-- | Converts an unsession typed channel to a session typed channel
toSTChan :: UTChan -> Proxy s -> STChan s

-- | Converts an unsession typed channel to a session typed channel
toSTChanBi :: UTChan -> Proxy s -> Proxy r -> STChanBi s r

-- | Converts a session typed send port into a Proxy
sendProxy :: STSendPort s -> Proxy s

-- | Converts a session typed receive port into a Proxy
recvProxy :: STReceivePort s -> Proxy s

-- | Sends a message using a session typed send port
sendSTChan :: Serializable a => STSendPort (Cap ctx (a :!> l)) -> a -> Process (STSendPort (Cap ctx l))

-- | Receives a message using a session typed receive port
recvSTChan :: Serializable a => STReceivePort (Cap ctx (a :?> l)) -> Process (a, STReceivePort (Cap ctx l))

-- | Type class that defines combinators for branching on a session typed
--   port
class STSplit (m :: Cap Type -> Type)

-- | select the first branch of a selection using the given port
sel1Chan :: STSplit m => m (Cap ctx (Sel (s : xs))) -> m (Cap ctx s)

-- | select the second branch of a selection using the given port
sel2Chan :: STSplit m => m (Cap ctx (Sel (s : (t : xs)))) -> m (Cap ctx (Sel (t : xs)))

-- | select the first branch of an offering using the given port
off1Chan :: STSplit m => m (Cap ctx (Off (s : xs))) -> m (Cap ctx s)

-- | select the second branch of an offering using the given port
off2Chan :: STSplit m => m (Cap ctx (Off (s : (t : xs)))) -> m (Cap ctx (Off (t : xs)))

-- | Type class for recursion on a session typed port
class STRec (m :: Cap Type -> Type)
recChan :: STRec m => m (Cap ctx (R s)) -> m (Cap (s : ctx) s)
wkChan :: STRec m => m (Cap (t : ctx) (Wk s)) -> m (Cap ctx s)
varChan :: STRec m => m (Cap (s : ctx) V) -> m (Cap (s : ctx) s)

-- | Indexed monad transformer that is indexed by two products of session
--   types
--   
--   This monad also acts as a state monad that whose state is defined by a
--   session typed channel and dependent on the indexing of the monad.
data STChannelT m (p :: Prod Type) (q :: Prod Type) a
STChannelT :: ((STSendPort (Left p), STReceivePort (Right p)) -> m (a, (STSendPort (Left q), STReceivePort (Right q)))) -> STChannelT m a
[runSTChannelT] :: STChannelT m a -> ((STSendPort (Left p), STReceivePort (Right p)) -> m (a, (STSendPort (Left q), STReceivePort (Right q))))

-- | Send a message
--   
--   Only the session type of the send port needs to be adjusted
sendSTChanM :: Serializable a => a -> STChannelT Process (Cap ctx (a :!> l) :*: r) (Cap ctx l :*: r) ()

-- | receive a message
--   
--   Only the session type of the receive port needs to be adjusted
recvSTChanM :: Serializable a => STChannelT Process (l :*: (Cap ctx (a :?> r))) (l :*: Cap ctx r) a

-- | select the first branch of a selection
--   
--   Both ports are now adjusted. This is similarly so for the remaining
--   combinators.
sel1ChanM :: STChannelT Process (Cap lctx (Sel (l : ls)) :*: (Cap rctx (Sel (r : rs)))) (Cap lctx l :*: Cap rctx r) ()

-- | select the second branch of a selection
sel2ChanM :: STChannelT Process (Cap lctx (Sel (s1 : (t1 : xs1))) :*: Cap rctx (Sel (s2 : (t2 : xs2)))) (Cap lctx (Sel (t1 : xs1)) :*: Cap rctx (Sel (t2 : xs2))) ()

-- | select the first branch of an offering
off1ChanM :: STChannelT Process (Cap lctx (Off (l : ls)) :*: (Cap rctx (Off (r : rs)))) (Cap lctx l :*: Cap rctx r) ()

-- | select the second branch of an offering
off2ChanM :: STChannelT Process (Cap lctx (Off (s1 : (t1 : xs1))) :*: Cap rctx (Off (s2 : (t2 : xs2)))) (Cap lctx (Off (t1 : xs1)) :*: Cap rctx (Off (t2 : xs2))) ()

-- | delimit scope of recursion
recChanM :: STChannelT Process (Cap sctx (R s) :*: Cap rctx (R r)) (Cap (s : sctx) s :*: Cap (r : rctx) r) ()

-- | weaken scope of recursion
wkChanM :: STChannelT Process (Cap (t : sctx) (Wk s) :*: Cap (k : rctx) (Wk r)) (Cap sctx s :*: Cap rctx r) ()

-- | recursion variable (recurse here)
varChanM :: STChannelT Process ((Cap (s : sctx) V) :*: (Cap (r : rctx) V)) (Cap (s : sctx) s :*: Cap (r : rctx) r) ()

-- | ports are no longer usable
epsChanM :: STChannelT Process (Cap ctx Eps :*: Cap ctx Eps) (Cap ctx Eps :*: Cap ctx Eps) ()

-- | Unsession typed send
utsend :: Serializable a => ProcessId -> a -> Session s s ()

-- | Unsafe send
usend :: Serializable a => ProcessId -> a -> Session s s ()
expect :: Serializable a => Session s s a
expectTimeout :: Serializable a => Int -> Session s s (Maybe a)
newChan :: Serializable a => Session s s (SendPort a, ReceivePort a)
sendChan :: Serializable a => SendPort a -> a -> Session s s ()
receiveChan :: Serializable a => ReceivePort a -> Session s s a
receiveChanTimeout :: Serializable a => Int -> ReceivePort a -> Session s s (Maybe a)
mergePortsBiased :: Serializable a => [ReceivePort a] -> Session s s (ReceivePort a)
mergePortsRR :: Serializable a => [ReceivePort a] -> Session s s (ReceivePort a)
unsafeSend :: Serializable a => ProcessId -> a -> Session s s ()
unsafeSendChan :: Serializable a => SendPort a -> a -> Session s s ()
unsafeNSend :: Serializable a => String -> a -> Session s s ()
unsafeNSendRemote :: Serializable a => NodeId -> String -> a -> Session s s ()
receiveWait :: [Match b] -> Session s s b
receiveTimeout :: Int -> [Match b] -> Session s s (Maybe b)
unwrapMessage :: Serializable a => Message -> Session s s (Maybe a)
handleMessage :: Serializable a => Message -> (a -> Session s s b) -> Session r r (Maybe b)
handleMessage_ :: Serializable a => Message -> (a -> Session s s ()) -> Session r r ()
handleMessageP :: Serializable a => Message -> (a -> Process b) -> Session s s (Maybe b)
handleMessageP_ :: Serializable a => Message -> (a -> Process ()) -> Session s s ()
handleMessageIf :: Serializable a => Message -> (a -> Bool) -> (a -> Session s s b) -> Session r r (Maybe b)
handleMessageIf_ :: Serializable a => Message -> (a -> Bool) -> (a -> Session s s ()) -> Session r r ()
handleMessageIfP :: Serializable a => Message -> (a -> Bool) -> (a -> Process b) -> Session s s (Maybe b)
handleMessageIfP_ :: Serializable a => Message -> (a -> Bool) -> (a -> Process ()) -> Session s s ()
forward :: Message -> ProcessId -> Session s s ()
uforward :: Message -> ProcessId -> Session s s ()
delegate :: ProcessId -> (Message -> Bool) -> Session s s ()
relay :: ProcessId -> Session s s ()
proxy :: Serializable a => ProcessId -> (a -> Session s s Bool) -> Session r r ()
proxyP :: Serializable a => ProcessId -> (a -> Process Bool) -> Session s s ()
spawn :: NodeId -> Closure (SessionWrap ()) -> Session s s ProcessId
spawnP :: NodeId -> Closure (Process ()) -> Session s s ProcessId
call :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (SessionWrap a) -> Session r r a
callP :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (Process a) -> Session s s a
terminate :: Session s s a
die :: Serializable a => a -> Session s s b
kill :: ProcessId -> String -> Session s s ()
exit :: Serializable a => ProcessId -> a -> Session s s ()
catchExit :: (Show a, Serializable a) => Session s s b -> (ProcessId -> a -> Session r r b) -> Session t t b
catchExitP :: (Show a, Serializable a) => Process b -> (ProcessId -> a -> Process b) -> Session s s b
catchesExit :: Session s s b -> [ProcessId -> Message -> Session r r (Maybe b)] -> Session t t b
catchesExitP :: Process b -> [ProcessId -> Message -> Process (Maybe b)] -> Session s s b
getSelfPid :: Session s s ProcessId
getSelfNode :: Session s s NodeId
getOthPid :: Session s s (Maybe ProcessId)
getOthNode :: Session s s (Maybe NodeId)
getProcessInfo :: ProcessId -> Session s s (Maybe ProcessInfo)
getNodeStats :: NodeId -> Session s s (Either DiedReason NodeStats)
link :: ProcessId -> Session s s ()
linkNode :: NodeId -> Session s s ()
unlink :: ProcessId -> Session s s ()
unlinkNode :: NodeId -> Session s s ()
monitor :: ProcessId -> Session s s MonitorRef
monitorNode :: NodeId -> Session s s MonitorRef
monitorPort :: Serializable a => SendPort a -> Session s s MonitorRef
unmonitor :: MonitorRef -> Session s s ()
withMonitor :: ProcessId -> (MonitorRef -> Session s s a) -> Session r r a
withMonitor_ :: ProcessId -> Session s s a -> Session r r a
withMonitorP :: ProcessId -> (MonitorRef -> Process a) -> Session s s a
withMonitorP_ :: ProcessId -> Process a -> Session s s a
unStatic :: Typeable a => Static a -> Session s s a
unClosure :: Typeable a => Closure a -> Session s s a
say :: String -> Session s s ()
register :: String -> ProcessId -> Session s s ()
unregister :: String -> Session s s ()
whereis :: String -> Session s s (Maybe ProcessId)
nsend :: Serializable a => String -> a -> Session s s ()
registerRemoteAsync :: NodeId -> String -> ProcessId -> Session s s ()
reregisterRemoteAsync :: NodeId -> String -> ProcessId -> Session s s ()
whereisRemoteAsync :: NodeId -> String -> Session s s ()
nsendRemote :: Serializable a => NodeId -> String -> a -> Session s s ()
spawnAsync :: NodeId -> Closure (SessionWrap ()) -> Session r r SpawnRef
spawnAsyncP :: NodeId -> Closure (Process ()) -> Session s s SpawnRef
spawnSupervised :: NodeId -> Closure (SessionWrap ()) -> Session s s (ProcessId, MonitorRef)
spawnSupervisedP :: NodeId -> Closure (Process ()) -> Session s s (ProcessId, MonitorRef)
spawnLink :: NodeId -> Closure (SessionWrap ()) -> Session s s ProcessId
spawnLinkP :: NodeId -> Closure (Process ()) -> Session s s ProcessId
spawnMonitor :: NodeId -> Closure (SessionWrap ()) -> Session s s (ProcessId, MonitorRef)
spawnMonitorP :: NodeId -> Closure (Process ()) -> Session s s (ProcessId, MonitorRef)
spawnChannel :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (ReceivePort a -> SessionWrap ()) -> Session s s (SendPort a)
spawnChannelP :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (ReceivePort a -> Process ()) -> Session s s (SendPort a)
spawnLocal :: Session s s () -> Session r r ProcessId
spawnLocalP :: Process () -> Session s s ProcessId
spawnChannelLocal :: Serializable a => (ReceivePort a -> Session s s ()) -> Session r r (SendPort a)
spawnChannelLocalP :: Serializable a => (ReceivePort a -> Process ()) -> Session s s (SendPort a)
callLocal :: Session s s a -> Session s s a
callLocalP :: Process a -> Session s s a
reconnect :: ProcessId -> Session s s ()
reconnectPort :: SendPort a -> Session s s ()