simple-sessions (empty) → 0.1
raw patch · 11 files changed
+1114/−0 lines, 11 filesdep +basedep +category-extrassetup-changed
Dependencies added: base, category-extras
Files
- Control/Concurrent/SimpleSession/Examples/Implicit.lhs +119/−0
- Control/Concurrent/SimpleSession/Examples/Positional.lhs +220/−0
- Control/Concurrent/SimpleSession/Implicit.lhs +283/−0
- Control/Concurrent/SimpleSession/Positional.lhs +236/−0
- Control/Concurrent/SimpleSession/SessionTypes.lhs +116/−0
- Control/Concurrent/SimpleSession/TChan.lhs +38/−0
- Control/Concurrent/SimpleSession/UChan.lhs +38/−0
- LICENSE +26/−0
- Setup.hs +4/−0
- TODO +2/−0
- simple-sessions.cabal +32/−0
+ Control/Concurrent/SimpleSession/Examples/Implicit.lhs view
@@ -0,0 +1,119 @@+\subsection{Implicit Channel Examples}+\label{sec:examples:implicit}+\ignore{++> {-# OPTIONS -F -pgmF ixdopp #-}+> module Control.Concurrent.SimpleSession.Examples.Implicit where+>+> import Control.Concurrent (forkIO)+>+> import Control.Concurrent.SimpleSession.Implicit++}++In these examples, we use |ixdo| notation for indexed monads,+analogous to |do| notation for monads. This syntax is implemented by a+preprocessor.++\paragraph{A print server.}++As an example, we implement a simple print server.+The client side of the print server protocol is:+\begin{enumerate}+ \item Choose either to finish or to continue.+ \item Send a string.+ \item Go to step 1.+\end{enumerate}++We first implement the server.++> server = enter >>>= \_ -> loop where+> loop = offer close+> (ixdo+> s <- recv+> io (putStrLn s)+> zero+> loop)++GHC's type checker can infer that |server|'s+session type is |Rec (Eps :&: (String :?: Var Z))|.++%include fig-operationtypes.tex++The client reads user input, which it sends to the server for printing.+When the user tells the client to quit, it sends one more string to the+server, tells the server to quit, and closes the channel.++> client = enter >>>= \_ -> loop 0 where+> loop count = ixdo+> s <- io getLine+> case s of+> "q" -> ixdo+> sel2+> send (show count ++ " lines sent")+> zero; sel1; close+> _ -> ixdo+> sel2; send s+> zero; loop (count + 1)++GHC infers the session type+|Rec (Eps :+: (String :!: Var Z))| for+|client|, which is clearly dual to the type inferred for |server| above.++We run a session by creating a new |Rendezvous|, having the server+accept in a new thread, and having the client request in the main thread.++> runPrintSession = do+> rv <- newRendezvous+> forkIO (accept rv server)+> request rv client++\paragraph{An example of subtyping.}+\label{sec:subtyping}++Our implementation provides a form of protocol subtyping.+Consider a reimplementation of Gay and Hole's \citeyearpar{r:gay99}+arithmetic server, which provides two services, addition and negation:++> server1 = offer+> (ixdo a <- recv+> b <- recv+> send (a + b)+> close)+> (ixdo a <- recv+> send (-a)+> close)++The full protocol for |server1| is inferred:++< (Integer :?: Integer :?: Integer :!: Eps) :&:+< (Integer :?: Integer :!: Eps)++A second server implements only the negation service:++> server2 = offer+> close+> (ixdo a <- recv+> send (-a)+> close)++Its protocol is inferred as well:++< Eps :&: (Integer :?: Integer :!: Eps)++A particular client may avail itself of only+one of the offered services:++> client' x = ixdo sel2; send x; y <- recv; close; ireturn y++The client's protocol is inferred as |r :+: (a :!: b :?: Eps)|, which+unifies with the duals of both servers' protocols. Without the+functional dependencies in |Dual|, however, attempting to connect the+client with |server2| leads the type checker to complain that there+is no instance of |Dual| for |r| and |Eps|; connecting |client| with+|server1| also fails to type check. The functional dependency nudges+the type checker towards attempting to unify |r| with the corresponding+part of either server's type, which then succeeds. As a result, the+|client| may be composed with both servers in the same program and+never notices the difference.+
+ Control/Concurrent/SimpleSession/Examples/Positional.lhs view
@@ -0,0 +1,220 @@+\ignore{++> {-# OPTIONS -F -pgmF ixdopp #-}+> {-# LANGUAGE TypeOperators #-}+> module Control.Concurrent.SimpleSession.Examples.Positional where+>+> import Control.Concurrent (threadDelay)+> import Random+>+> import Control.Concurrent.SimpleSession.Positional++}++\subsection{An Example with Multiple Channels}+\label{sec:example:multiple}++As an example, we give an implementation of the Sutherland-Hodgman+\citeyearpar{Sutherland1974Reentrant} reentrant polygon clipping algorithm,+which takes a plane and a series of points representing the+vertices of a polygon,+and produces vertices for the polygon restricted to one side of the plane.+\Citet{Shivers2006Continuations}+present a stream transducer implementation, which we follow. Each+transducer takes one plane to clip by, and two |Rendezvous| objects for+the same protocol. It connects on both, and then receives original points+on one channel and sends clipped points on the other.++We assume that we have types |Plane| and |Point|, a predicate+|above| that indicates whether a given point is on the visible side+of a given plane, and a partial function |intersection| that computes+where the line segment between two points intersects a plane.++GHC infers all the types in this example.++< type SendList a = Rec (Eps :+: (a :!: Var Z))+<+< clipper :: Plane -> Rendezvous (SendList Point)+< -> Rendezvous (SendList Point)+< -> Session x x ()+< clipper plane inrv outrv =+< accept outrv $ \oc ->+< request inrv $ \ic -> ixdo+< let shutdown = ixdo close ic; sel1 oc; close oc+< put pt = dig $ ixdo+< sel2 oc; send oc pt; zero oc+< -- Attempt to get a point; pass it to yes, or+< -- call no if there are no more:+< get no yes = offer ic no $ ixdo+< pt <- recv ic; zero ic; yes pt+< -- If the line crosses the plane, send the intersection point:+< putCross line =+< maybe (ireturn ()) put (line `intersect` plane)+< putIfVisible pt =+< if pt `above` plane then put pt else ireturn ()+< dig (enter oc)+< enter ic+< get shutdown $ \pt0 ->+< let loop pt = ixdo+< putIfVisible pt+< get (putcross (pt, pt0) >>>= \_ -> shutdown)+< (\pt' -> ixdo putcross (pt,pt')+< loop pt')+< in loop pt0++\par+We use |sendlist| to send a list of points to the first+transducer in the pipeline, and we use |recvlist| to accumulate+points produced by the last transducer.++< sendlist :: [a] -> Rendezvous (SendList a)+< -> Session x x ()+< sendlist xs rv = accept rv start where+< start oc = enter oc >>>= \_ -> loop xs where+< loop [] = ixdo sel1 oc; close oc+< loop (x:xs) = ixdo sel2 oc; send oc x+< zero oc; loop xs+<+< recvlist :: Rendezvous (SendList a) -> Session x x [a]+< recvlist rv = request rv start where+< start ic = enter ic >>>= \_ -> loop [] where+< loop acc = offer ic+< (close ic >>>= \_ -> ireturn (reverse acc))+< (recv ic >>>= \x -> zero ic >>>= \_ -> loop (x : acc))++\par+Given a list of planes and a list of points, |clipMany| starts a |clipper|+for each plane in a separate thread. It starts |sendlist| a new thread,+giving it the list of points and connecting it to the first |clipper|.+It then runs |recvlist| in the main thread to gather up the result.++< clipMany :: [Plane] -> [Point] -> IO [Point]+< clipMany planes points = runSession $ ixdo+< rv <- io newRendezvous+< forkSession (sendlist points rv)+< let loop [] rv = recvlist rv+< loop (p:ps) rv = ixdo+< rv' <- io newRendezvous+< forkSession (clipper p rv rv')+< loop ps rv'+< loop planes rv++\ignore{++< bench n m = do+< g1 <- getStdRandom split+< g2 <- getStdRandom split+< let groupPoints (x:y:z:r) = Point x y z : groupPoints r+< groupPlanes (a:b:c:r) = Plane a b c 0 : groupPlanes r+< points = groupPoints [ 10 * (x - 0.5) | x <- randoms g1 ]+< planes = groupPlanes [ 10 * (x - 0.5) | x <- randoms g2 ]+< points <- clipMany (take m planes) (take n points)+< print (length points)+<+< data Point = Point !Double !Double !Double+< data Plane = Plane !Double !Double !Double !Double+<+< instance Show Point where+< showsPrec _ (Point x y z) =+< ('(':) . shows x . (", "++) . shows y . (", "++) . shows z . (')':)+<+< instance Show Plane where+< showsPrec _ (Plane a b c d) =+< shows a . ("x + "++) . shows b . ("y + "++) .+< shows c . ("z + "++) . shows d . (" = 0"++)+< +< above :: Point -> Plane -> Bool+< above (Point x y z) (Plane a b c d)+< = (a * x + b * y + c * z + d) / sqrt (a * a + b * b + c * c) > 0+< +< intersect :: (Point, Point) -> Plane -> Maybe Point+< intersect (p1@(Point x1 y1 z1), p2@(Point x2 y2 z2)) plane@(Plane a b c d)+< = if above p1 plane == above p2 plane+< then Nothing+< else Just (Point x y z) where+< x = x1 + (x2 - x1) * t+< y = y1 + (y2 - y1) * t+< z = z1 + (z2 - z1) * t+< t = (a * x1 + b * y1 + c * z1 + d) /+< (a * (x1 - x2) + b * (y1 - y2) + c * (z1 - z2))++> newPrinter = do+> spec <- newRendezvous+> let printer = ixdo+> clet c = accept spec+> offer c+> (recv c >>>= io . putStrLn >>>= \_ -> close c >>>= \_ -> printer)+> (close c)+> let say s = runSession $+> clet c = request spec in+> ixdo sel1 c; send c s; close c+> let shutdown = runSession $+> clet c = request spec in+> sel2 c >>>= \_ -> close c+> runSession (forkSession printer)+> return (say, shutdown)+>+> logger say c = enter c >>>= \_ -> loop where+> loop =+> offer c+> (ixdo+> msg <- recv c+> io (say ("logger: " ++ msg))+> zero c+> loop)+> (ixdo+> io (say "logger: exiting")+> send c ()+> close c)+>+> echoServer espec lspec = ixdo+> clet lc = request lspec+> enter lc+> let loop = ixdo+> clet ec = accept espec+> offer ec+> (ixdo+> swap+> sel1 lc; send lc "echo server forking"+> zero lc+> dig (forkSession (recv ec >>>= send ec >>>= \_ -> close ec))+> loop)+> (ixdo+> dig $ ixdo+> sel1 lc; send lc "echo server exiting"+> zero lc+> sel2 lc; recv lc+> close lc+> send ec ()+> close ec)+> loop+>+> client delay say espec = ixdo+> clet c = request espec+> s <- io getLine+> case s of+> "q" -> ixdo+> sel2 c+> recv c+> close c+> _ -> ixdo+> forkSession $ ixdo+> sel1 c+> io (threadDelay $ round $ 1000000 * delay)+> send c s+> str <- recv c+> io (say str)+> close c+> client delay say espec+>+> go delay = do+> espec <- newRendezvous+> lspec <- newRendezvous+> (say, shutdown) <- newPrinter+> runSession $+> forkSession (accept lspec $ logger say) >>>= \_ ->+> forkSession (echoServer espec lspec) >>>= \_ ->+> client delay say espec+> shutdown++}
+ Control/Concurrent/SimpleSession/Implicit.lhs view
@@ -0,0 +1,283 @@+\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
+ Control/Concurrent/SimpleSession/Positional.lhs view
@@ -0,0 +1,236 @@+\section{Take $n$: Multiple Channels}+\label{sec:positional}++\ignore{++> {-# LANGUAGE TypeOperators,+> EmptyDataDecls,+> Rank2Types #-}+>+> module Control.Concurrent.SimpleSession.Positional (+> module Control.Concurrent.SimpleSession.SessionTypes,+> module Control.Monad.Indexed,+> Session, Cap, Channel,+> io,+> send, recv, close, sel1, sel2, offer,+> enter, zero, suc,+> dig, swap, forkSession,+> Rendezvous, newRendezvous,+> accept, request, runSession+> ) where+>+> import Control.Concurrent (forkIO)+>+> import Control.Concurrent.SimpleSession.UChan+> import Control.Concurrent.SimpleSession.TChan+> import Control.Monad.Indexed+> import Control.Concurrent.SimpleSession.SessionTypes+>+> newtype Rendezvous r = Rendezvous (TChan UChan)+>+> newRendezvous :: IO (Rendezvous r)+> newRendezvous = newTChan >>= return . Rendezvous+> +> recv :: Channel t -> Session (Cap t e (a :?: r), x) (Cap t e r, x) a+> close :: Channel t -> Session (Cap t e Eps, x) x ()+> sel1 :: Channel t -> Session (Cap t e (r :+: s), x) (Cap t e r, x) ()+> sel2 :: Channel t -> Session (Cap t e (r :+: s), x) (Cap t e s, x) ()+> offer :: Channel t -> Session (Cap t e r, x) u a -> Session (Cap t e s, x) u a -> Session (Cap t e (r:&:s), x) u a+> enter :: Channel t -> Session (Cap t e (Rec r), x) (Cap t (r, e) r, x) ()+> zero :: Channel t -> Session (Cap t (r, e) (Var Z), x) (Cap t (r, e) r, x) ()+> suc :: Session (Cap t (r, e) (Var (S v)), x) (Cap t e (Var v), x) ()+>+> _cast = Session . unSession+> recv (Channel c) = Session (unsafeReadUChan c)+> sel1 c = _cast (send c True)+> sel2 c = _cast (send c False)+> offer c l r = _cast (recv c) >>>= \choice ->+> if choice+> then _cast l+> else _cast r+> close _ = _cast (ireturn ())+> enter _ = _cast (ireturn ())+> zero _ = _cast (ireturn ())+> suc = _cast (ireturn ())++}++Rather than limit ourselves to one implicit channel at a time, it might+be more flexible to work with several channels at once. To extend |Session| to+handle multiple channels, our first step is to separate the channel+itself from the capability to use it for a particular session:++> newtype Channel t = Channel UChan+> data Cap t e r++The parameter |t| is a unique tag that ties a given channel to the+capability to use it. A |Channel t| is an actual value at run time,+while the corresponding |Cap t e r| is relevant only during type-checking.+We allow |Channel t| to be aliased freely because+a channel is unusable without its capability, and we treat capabilities+linearly. As before, the capability also contains a session type+environment |e| and a session type |r| that is closed in |e|.++We now index |Session| by a \emph{stack} of capabilities, while+underneath the hood, it is just the |IO| monad. |Session| is no longer+responsible for maintaining the run-time representation of channels, but+instead it keeps track of the compile-time representation of+capabilities.++> newtype Session s s' a = Session { unSession :: IO a }+>+> instance IxFunctor Session where+> imap = undefined+> instance IxPointed Session where+> ireturn = undefined+> instance IxApplicative Session where+> iap = undefined+> instance IxMonad Session where+> ibind = undefined+>+> io :: IO a -> Session s s a+> io = Session++< instance IxMonad Session where+< ret = Session . return+< m >>>= k = Session (unSession m >>= unSession . k)++\par+A |Session| computation now carries a stack of capability types, and+communication operations manipulate only the top capability on the+stack, leaving the rest of the stack unchanged.+The |send| operation takes a channel+as an argument rather than obtaining it implicitly, and the tag |t| on+the channel must match the tag in the capability.++> send :: Channel t -> a ->+> Session (Cap t e (a :!: r), x)+> (Cap t e r, x) ()+> send (Channel c) a = Session (unsafeWriteUChan c a)++In the type above, |Cap t e (a :!: r)| is the capability on the top+of the stack before the |send|, and |Cap t e r| is the capability+after the |send|. Type variable |x| represents the rest of the+capability stack, which is unaffected by this operation.++The implementations of the remaining operations are similarly unsurprising.+Each differs from the previous section only in obtaining a channel+explicitly from its argument rather than implicitly from the indexed+monad. Their types may be found in Figure~\ref{fig:operationtypes}.+Note that |close| now has the effect of popping the capability for the+closed channel from the top of the stack.++\paragraph{Stack manipulation.}++Channel operations act on the top of the capability stack. Because the+capability for the particular channel we wish to use may not be on the+top of the stack, we may need to use other capabilities than the top+one. The |dig| combinator suffices to+select any capability on the stack. Given a |Session| computation that+transforms a stack |x| to a stack |x'|, |dig| lifts it to a computation+that transforms |(r, x)| to |(r, x')| for any |r|; thus, $n$+applications of |dig| will select the $n$th capability on the stack.+Note that |dig| has no run-time effect, but merely unwraps and rewraps +a |Session| to change the phantom type parameters.++> dig :: Session x x' a -> Session (r, x) (r, x') a+> dig = Session . unSession++In combination with |swap|, we may generate any desired stack permutation.+Since |swap| exchanges the top two capabilities on the stack, |dig| and+|swap| may be combined to exchange any two adjacent capabilities.++> swap :: Session (r, (s, x)) (s, (r, x)) ()+> swap = Session (return ())++\par+One reason we may want to rearrange the stack is to support |forkSession|,+which runs a |Session| computation in a new thread, giving to it+the entire \emph{visible} stack. Thus, to partition the stack+between the current thread and a new thread, we use |dig| and |swap|+until all the capabilities for the new thread are below all the+capabilities for the current thread. Then we call |forkSession|+under sufficiently many |dig|s so that it takes only the desired capabilities+with it.++> forkSession :: Session x () () -> Session x () ()+> forkSession (Session c)+> = Session (forkIO c >> return ())++For example, to keep the top two capabilities on the stack+for the current thread and assign the rest to a new thread |m|, we+would use |dig (dig (forkSession m))|.++\paragraph{Making a connection.}++In the implicit channel case, each |accept| or |request| starts+a single |Session| computation that runs to completion.+Because we now have multiple channels, we may need+to use |accept| and |request| to start new communication+sessions during an ongoing |Session| computation.+Given a |Rendezvous| and a continuation+of matching session type, |accept|+creates a new channel/capability pair. It calls the continuation with+the channel, pushing the corresponding capability on the top of its+stack. The \mbox{rank-2} type in |accept| ensures that the new |Channel t|+and |Cap t () r| cannot be used with any other capability or channel.+In \Section\ref{sec:discussion} we discuss an alternate formulation that+does not require higher-rank polymorphism, but this version here seems+more elegant.++> accept :: Rendezvous r ->+> (forall t. Channel t ->+> Session (Cap t () r, x) y a) ->+> Session x y a+> accept (Rendezvous c) f = Session (do+> nc <- newUChan+> writeTChan c nc+> unSession (f (Channel nc)))++The |request| function behaves similarly, but as before, it+uses the dual session type.++> request :: Dual r r' =>+> Rendezvous r ->+> (forall t. Channel t ->+> Session (Cap t () r', x) y a) ->+> Session x y a+> request (Rendezvous c) f = Session (do+> nc <- readTChan c+> unSession (f (Channel nc)))++We may start a |Session| computation from within the IO monad. The type+of |runSession| ensures that the computation both begins and ends with+no capabilities in the stack.++> runSession :: Session () () a -> IO a+> runSession = unSession++\paragraph{Sending capabilities.}++Now that we have multiple channels, we might wonder whether we can send+capabilities themselves over a channel. Certainly, but since we do+not allow direct access to capabilities, this requires a specialized+pair of functions.++> send_cap :: Channel t ->+> Session (Cap t e (Cap t' e' r' :!: r),+> (Cap t' e' r', x))+> (Cap t e r, x) ()+> send_cap (Channel c)+> = Session (unsafeWriteUChan c ())+>+> recv_cap :: Channel t ->+> Session (Cap t e (Cap t' e' r' :?: r), x)+> (Cap t e r, (Cap t' e' r', x)) ()+> recv_cap (Channel c) = Session (unsafeReadUChan c)++Observe that because capabilities have no run-time existence, the actual+value sent over the channel is |()|. This provides synchronization so+that the receiving process does not perform channel operations+with the capability before the sending process has finished its part.+The phantom type parameters to |Session| change to reflect the+transmission of the capability.++%include PositionalExample.lhs+
+ Control/Concurrent/SimpleSession/SessionTypes.lhs view
@@ -0,0 +1,116 @@+\section{Session Types in Haskell}+\label{sec:session}++\ignore{++> {-# LANGUAGE TypeOperators,+> EmptyDataDecls,+> MultiParamTypeClasses,+> FunctionalDependencies,+> UndecidableInstances #-}+> module Control.Concurrent.SimpleSession.SessionTypes (+> Z, S,+> Eps, (:!:), (:?:), (:+:), (:&:), Rec, Var,+> Dual+> ) where+> +> infixr 3 :!:, :?:+> infix 2 :+:, :&:+>+> data Z+> data S n++}++The central idea of session types \citep{r:gay99} is to parameterize a+channel with some type that represents a protocol, which the type system+then enforces. In Haskell, we may encode a protocol using ordinary+datatypes:++> data (:!:) a r+> data (:?:) a r+> data Eps++These datatypes require no constructors because they will have no+run-time representation.++If |a| is any type, and |r| is a protocol, then+we interpret |a :!: r| as the protocol, ``first send an |a|, and+then continue with |r|.'' Similarly, we interpret |a :?: r| as+the protocol, ``receive+an |a|, and then continue with |r|.'' The type |Eps| represents the empty+protocol of a depleted channel that is not yet closed.++For example, the type |Int :!: Bool :?: Eps| represents the protocol,+``send an |Int|, receive a |Bool|, and close the+channel.''\thinspace\footnote{The type constructors |(:!:)| and+|(:?:)| are declared right associative and with higher precedence than+|(:+:)| and |(:&:)|.}++If the process on one end of a channel speaks a particular protocol,+its correspondant at the other end of the channel must be prepared to+understand it. For example, if one process speaks |Int :!: Bool :?: Eps|,+the other process must implement the dual protocol+|Int :?: Bool :!: Eps|. We encode the duality relation using a type+class with multiple parameters and functional dependencies+\citep{Jones1997Type,Jones2000Type}.++> class Dual r s | r -> s, s -> r++The functional dependencies indicate that duality+is bijective, which helps Haskell to infer+protocols and enables a form of subtyping. Sending and receiving are+dual: if |r| is dual to |s|, then |a :!: r| is dual to |a :?: s|. The+empty session is dual to itself.++> instance Dual r s => Dual (a :!: r) (a :?: s)+> instance Dual r s => Dual (a :?: r) (a :!: s)+> instance Dual Eps Eps++\par+Our session types also represent alternation and recursion. If |r|+and |s| are protocols, then |r :+: s| represents an active choice+between following |r| or |s|. The type |r :&: s| represents+an offer to follow either |r| or |s|, as chosen by the other+process.++> data (:+:) r s+> data (:&:) r s++The two alternation operators are dual:++> instance (Dual r1 s1, Dual r2 s2) =>+> Dual (r1 :+: r2) (s1 :&: s2)+> instance (Dual r1 s1, Dual r2 s2) =>+> Dual (r1 :&: r2) (s1 :+: s2)++\par+Recursion turns out to be slightly more difficult. It is tempting to+use a fixed-point combinator, but this would require constructing a+type of kind $\star \to \star$ for any desired loop body, which+is not generally possible. We need+some other way for a recursive type to refer to itself, so we represent+this binding using de~Bruijn indices.++> data Rec r+> data Var v+> +> instance Dual r s => Dual (Rec r) (Rec s)+> instance Dual (Var v) (Var v)++The type |Rec r| adds a binding for |r| inside |r|; that is, it+implicitly defines a variable bound to the whole of |r| that can be used+\emph{within} |r|. We use |Var v| to refer to the variable bound by+the |v|th |Rec|, counting outward, where |v| is a Peano numeral+written with type constructors |Z| and |S|+(\emph{e.g.,} |Z| or |S (S Z)|). For example, the protocol++< Request :!: Rec (Response :?: (Var Z :&: Eps))++says to send a request and then be prepared to receive one or more+responses. By contrast, a process implementing the protocol++< Request :!: Rec ((Response :?: Var Z) :&: Eps)++must send a request and be prepared to accept any number of responses.+
+ Control/Concurrent/SimpleSession/TChan.lhs view
@@ -0,0 +1,38 @@++\ignore{++> module Control.Concurrent.SimpleSession.TChan (+> TChan, newTChan, writeTChan, readTChan+> ) where+> +> import Control.Concurrent.MVar++}++An |TChan a| is a monomorphic, synchronous channel that can transmit+values of type |a|:++> newtype TChan a++\ignore{++> = CC (MVar (MVar a))+> +> newTChan = newEmptyMVar >>= return . CC+> +> writeTChan (CC cc) v = do+> mv <- takeMVar cc+> putMVar mv v+> +> readTChan (CC cc) = do+> mv <- newEmptyMVar+> putMVar cc mv+> takeMVar mv++}++|TChan| has three operations:++> newTChan :: IO (TChan a)+> writeTChan :: TChan a -> a -> IO ()+> readTChan :: TChan a -> IO a
+ Control/Concurrent/SimpleSession/UChan.lhs view
@@ -0,0 +1,38 @@+\ignore{++> {-# LANGUAGE MagicHash #-}+> module Control.Concurrent.SimpleSession.UChan (+> UChan, newUChan, unsafeReadUChan, unsafeWriteUChan+> ) where+> +> import GHC.Exts+> import Control.Concurrent.SimpleSession.TChan++}++On top of |TChan| we have implemented |UChan|, an untyped,+synchronous channel:++> newtype UChan++\ignore{++> = CC (TChan Int)+> +> unUChan (CC c) = unsafeCoerce# c+> +> newUChan = newTChan >>= return . CC+> unsafeWriteUChan = writeTChan . unUChan+> unsafeReadUChan = readTChan . unUChan++}++Like |TChan|, |UChan| has three operations:++> newUChan :: IO UChan+> unsafeWriteUChan :: UChan -> a -> IO ()+> unsafeReadUChan :: UChan -> IO a++Note that since |UChan| is willing to send or receive a value of \emph{any}+type, it's unsafe unless we find some other way to restrict it.+
+ LICENSE view
@@ -0,0 +1,26 @@+Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++Redistributions of source code must retain the above copyright+notice, this list of conditions and the following disclaimer.++Redistributions in binary form must reproduce the above copyright+notice, this list of conditions and the following disclaimer in the+documentation and/or other materials provided with the distribution.++Neither the name of the Northeastern University; nor the names of its+contributors may be used to endorse or promote products derived from+this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED+TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,4 @@+#!/usr/bin/env runhaskell++import Distribution.Simple+main = defaultMain
+ TODO view
@@ -0,0 +1,2 @@+Haddock.+Name-based capability access.
+ simple-sessions.cabal view
@@ -0,0 +1,32 @@+Name: simple-sessions+Version: 0.1+Cabal-Version: >= 1.2+License: BSD3+License-File: LICENSE+Stability: experimental+Author: Jesse A. Tov <tov@ccs.neu.edu>+Maintainer: tov@ccs.neu.edu+Homepage: http://www.ccs.neu.edu/~tov/session-types+Category: Control+Synopsis: A simple implementation of session types+Build-type: Simple+Description:+ This library is based on the session types implementation+ from "Haskell Session Types with Almost No Class," from the 2008+ Haskell Symposium. For a full-featured session types library,+ see the sessions package.++Extra-Source-Files:+ TODO+ Control/Concurrent/SimpleSession/Examples/Implicit.lhs+ Control/Concurrent/SimpleSession/Examples/Positional.lhs++Library+ Build-Depends: base, category-extras+ Exposed-modules:+ Control.Concurrent.SimpleSession.SessionTypes,+ Control.Concurrent.SimpleSession.Implicit,+ Control.Concurrent.SimpleSession.Positional+ Other-modules:+ Control.Concurrent.SimpleSession.TChan,+ Control.Concurrent.SimpleSession.UChan