\section{Take 1: One Implicit Channel}
\label{sec:implicit}

\ignore{

> {-# LANGUAGE TypeOperators,
>              EmptyDataDecls,
>              MultiParamTypeClasses,
>              FunctionalDependencies,
>              FlexibleInstances,
>              FlexibleContexts,
>              UndecidableInstances #-}
>
> module Control.Concurrent.SimpleSession.Implicit (
>   module Control.Concurrent.SimpleSession.SessionTypes,
>   module Control.Monad.Indexed,
>   Session, Cap,
>   io,
>   send, recv, close, sel1, sel2, offer,
>   enter, zero, suc, Pop(pop),
>   Rendezvous, newRendezvous,
>   accept, request
> ) where
> 
> import Control.Concurrent.SimpleSession.TChan
> import Control.Concurrent.SimpleSession.UChan
> import Control.Monad.Indexed
> import Control.Concurrent.SimpleSession.SessionTypes

}

Encoding protocols in Haskell is not enough.  We cannot merely provide
channels parameterized by session types and call it a day.  For example,
consider a hypothetical |send| operation:

< send :: Channel (a :!: r) -> a -> IO (Channel r)

While this |send| returns the correct channel for the rest of the
session, it fails to prevent reuse of the |a :!: r| channel,
which would violate the protocol.  One way to avoid this problem is to
require that channels (or at least their sessions) be treated linearly.
In this section, we show how this is done for
processes having access to only one channel, which is left implicit in the
environment; in the next section, we implement multiple
concurrent channels.

We assume a substrate of synchronous channels in both typed and
untyped varieties:

< writeTChan       :: TChan a -> a -> IO ()
< readTChan        :: TChan a -> IO a
<
< unsafeWriteUChan :: UChan -> a -> IO ()
< unsafeReadUChan  :: UChan -> IO a

These channels have dynamic semantics similar to Concurrent ML's
\citep{Reppy1991CML} synchronous channels.  While |TChan|s transmit
only a single type, |UChan|s are indiscriminating about what
they send and receive.  In our implementation, they use |unsafeCoerce#|,
which can lead to undefined
behavior if sent and received types differ.  We must somehow impose our
own type discipline.

We define an abstract type |Session s s' a|, which represents a computation that
evolves a session from state |s| to state |s'| while producing a value of
type |a|.  |Session|'s constructor is not
exported to client code, so that clients of the library
cannot arbitrarily modify the session state.
|Session| is implemented as the composition of the IO monad with
a reader monad carrying a untyped channel.

> newtype Session s s' a =
>   Session { unSession :: UChan -> IO a }

The phantom parameters |s| and |s'| must track more information than
just the current session.  We define a type constructor |Cap| to hold
not only the current session |r|, but another type |e|, which represents
a session type environment:

> data Cap e r

The type |Cap e r| represents the capability to run the protocol |r|.
The session type environment |e| provides context for any
free variables |Var v| in |r|; that is, |r| must be closed in |e|.
We discuss |e| in more detail when we
explain recursion, and the other operations merely thread it through.

We can now give |send| a type and definition that will work:

> send  :: a -> Session (Cap e (a :!: r)) (Cap e r) ()
> send x = Session (\c -> unsafeWriteUChan c x)

Given an |a|, |send| evolves the session from
|a :!: r| to |r|.
In its implementation, |unsafeWriteUChan|
indiscriminately transmits values of any type over an untyped channel.
Thus, if we fail to ensure that the receiving process expects a value of
type |a|, things can go very wrong.  In \Section\ref{sec:theory}, we
argue that this cannot happen.

Predictably, |recv| requires the capability to receive an |a|, which it
then produces:

> recv  :: Session (Cap e (a :?: r)) (Cap e r) a
> recv   = Session unsafeReadUChan

We use |close| to discard an exhausted capability, replacing it
with |()|.
In this implementation, |close| is a run-time no-op.

> close :: Session (Cap e Eps) () ()
> close  = Session (\_ -> return ())

\paragraph{Composing computations.}

We also need a way to compose |Session| computations.  Composing a
session from state $s_1$ to $s_2$ with a session from state $t_1$ to
$t_2$ should be permitted only if $s_2 = t_1$.  This is precisely the
situation that \emph{indexed monads} capture.

%include IxMonad.lhs

The |IxMonad| instance for |Session| is then straightforward.  It
threads the implicit channel through and runs the underlying
computations in the |IO| monad.

> instance IxFunctor Session where
>   imap f = undefined
>
> instance IxPointed Session where
>   ireturn = undefined
>
> instance IxApplicative Session where
>   iap = undefined
>
> instance IxMonad Session where
>   ibind = undefined

< instance IxMonad Session where
<   ret a    = Session (\_ -> return a)
<   m >>>= k = Session (\c -> do a <- unSession m c
<                                unSession (k a) c)

We use |io| to lift an arbitrary |IO| computation into |Session|:

> io    :: IO a -> Session s s a
> io m   = Session (\_ -> m)

Because of |io|, this implementation is actually not linear but affine:
an |IO| action may raise an exception and terminate the |Session|
computation.  Provided that exceptions cannot be caught within a
|Session|, this does not jeopardize safety in the sense that any
messages received will still have the expected representation.  Some
formulations of session types guarantee that a session, once initiated,
will run to completion, but this seems unrealistic for real-world
programs.  Handling exceptions from within a session remains an open
problem.

\paragraph{Alternation.}

The session actions |sel1|, |sel2|, and |offer| implement alternation.
Action |sel1| selects the left side of an ``internal choice'',
thereby replacing a session |r :+: s| with the session |r|; |sel2|
selects the right side.  On the other side of the channel, |offer| combines a
|Session| computation for |r| with a computation for |s| into a
computation that can handle |r :&: s|.  Dynamically, |sel1| sends |True|
over the channel, whereas |sel2| sends |False|, and |offer| dispatches
on the boolean value received.

> sel1  :: Session (Cap e (r :+: s)) (Cap e r) ()
> sel1   = Session (\c -> unsafeWriteUChan c True)
> 
> sel2  :: Session (Cap e (r :+: s)) (Cap e s) ()
> sel2   = Session (\c -> unsafeWriteUChan c False)
> 
> offer :: Session (Cap e r) u a ->
>          Session (Cap e s) u a ->
>          Session (Cap e (r :&: s)) u a
> offer (Session m1) (Session m2)
>        = Session (\c -> do b <- unsafeReadUChan c
>                            if b then m1 c else m2 c)

\paragraph{Recursion.}

Session actions |enter|, |zero|, and |suc| implement recursion.
Consider the recursive session type

< Request :!: Rec ((Response :?: Var Z) :&: Eps)

from above.  After sending a |Request|, we need some way to enter the
body of the |Rec|, and upon reaching |Var Z|, we need some way to repeat
the body of the |Rec|.  We accomplish the former with |enter|, which
strips the |Rec| constructor from |r| and pushes |r| onto the stack |e|:

> enter :: Session (Cap e (Rec r)) (Cap (r, e) r) ()
> enter  = Session (\_ -> return ())

In |e|, we maintain a stack of session types for the body of each enclosing
|Rec|, representing an environment that closes over |r|.  Upon
encountering a variable occurence |Var |$n$, where $n$ is a Peano
numeral, we restore the
$n$th session type from the stack and return the stack to its former
state, using $n$ expressed with |zero| and |suc|:

> zero  :: Session (Cap (r, e) (Var Z))
>                  (Cap (r, e) r) ()
> zero   = Session (\_ -> return ())
>
> suc   :: Session (Cap (r, e) (Var (S v)))
>                  (Cap e (Var v)) ()
> suc    = Session (\_ -> return ())

For example, if the current session is |Var (S (S Z))|, then the operation

< suc >>> suc >>> zero

pops two elements from the stack and
replaces the current session with the body of the third enclosing |Rec|.

It is worth remarking that this duplication of type and code to pop the
stack is not strictly necessary.  If we explicitly
write |suc >>> suc >>> zero|, Haskell's type checker can infer |S (S Z)|.  If,
on the other hand, the type is already known, then a type class can do
the work:\footnote{Note that the definition of the method |pop| is the
same for both instances of |Pop|, which suggests that it could
be provided as a default method.  This would introduce a subtle bug,
however, as it would enable defining new instances of |Pop| with
arbitrary effect.}

> class Pop s s' | s -> s' where pop :: Session s s' ()
> 
> instance Pop (Cap (r, e) (Var Z)) (Cap (r, e) r)
>   where pop = Session (\_ -> return ())
>
> instance Pop (Cap e (Var v)) (Cap e' r') =>
>          Pop (Cap (r, e) (Var (S v))) (Cap e' r')
>   where pop = Session (\_ -> return ())

\paragraph{Putting it all together.}

Finally, we need a way to connect and run sessions.

A |Rendezvous| is a synchronization object that connects the types of
two processes at compile time, and then enables their connection by a
channel at run time.  The |Rendezvous| carries a phantom parameter
indicating the protocol to be spoken on the shared implicit channel,
and is represented by a
homogeneous, typed channel on which the untyped channel for a particular
session will later be exchanged.  Creating a |Rendezvous| is as simple
as creating a new typed channel and wrapping it.

> newtype Rendezvous r = Rendezvous (TChan UChan)
> 
> newRendezvous :: IO (Rendezvous r)
> newRendezvous  = newTChan >>= return . Rendezvous

\par
To accept a connection request, we need a |Rendezvous| object,
and a |Session| computation whose starting session type matches that of
the |Rendezvous|.  The computation must deplete and close its channel.
At run time, |accept| creates a new untyped channel on which
the communication will take place and sends it over the |Rendezvous|
channel.  It then runs the session computation on the new channel.

> accept :: Rendezvous r ->
>           Session (Cap () r) () a -> IO a
> accept (Rendezvous c) (Session f) = do
>   nc <- newUChan
>   writeTChan c nc
>   f nc

\par
To request a connection, the session type of the |Session| computation
must be dual to that of the given |Rendezvous|.  At run time,
|request| receives a new, untyped channel from |accept| over the
|Rendezvous| channel and then runs the computation using the channel.

> request :: Dual r r' => Rendezvous r ->
>            Session (Cap () r') () a -> IO a
> request (Rendezvous c) (Session f)
>          = readTChan c >>= f

%include ImplicitExample.lhs