| Safe Haskell | None |
|---|
Control.Concurrent.SimpleSession.Implicit
- module Control.Concurrent.SimpleSession.SessionTypes
- module Control.Monad.Indexed
- data Session s s' a
- data Cap e r
- io :: IO a -> Session s s a
- send :: a -> Session (Cap e (a :!: r)) (Cap e r) ()
- recv :: Session (Cap e (a :?: r)) (Cap e r) a
- close :: Session (Cap e Eps) () ()
- sel1 :: Session (Cap e (r :+: s)) (Cap e r) ()
- sel2 :: Session (Cap e (r :+: s)) (Cap e s) ()
- offer :: Session (Cap e r) u a -> Session (Cap e s) u a -> Session (Cap e (r :&: s)) u a
- enter :: Session (Cap e (Rec r)) (Cap (r, e) r) ()
- zero :: Session (Cap (r, e) (Var Z)) (Cap (r, e) r) ()
- suc :: Session (Cap (r, e) (Var (S v))) (Cap e (Var v)) ()
- class Pop s s' | s -> s' where
- data Rendezvous r
- newRendezvous :: IO (Rendezvous r)
- accept :: Rendezvous r -> Session (Cap () r) () a -> IO a
- request :: Dual r r' => Rendezvous r -> Session (Cap () r') () a -> IO a
Documentation
module Control.Monad.Indexed
Session| is implemented as the composition of the IO monad with a reader monad carrying a untyped channel.
recv :: Session (Cap e (a :?: r)) (Cap e r) aSource
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 Sectionref{sec:theory}, we argue that this cannot happen.
Predictably, |recv| requires the capability to receive an |a|, which it then produces:
sel1 :: Session (Cap e (r :+: s)) (Cap e r) ()Source
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.
zero :: Session (Cap (r, e) (Var Z)) (Cap (r, e) r) ()Source
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|:
data Rendezvous r Source
newRendezvous :: IO (Rendezvous r)Source