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


-- | A simple implementation of session types
--   
--   This library is based on the session types implementation from
--   <a>Haskell Session Types with Almost No Class,</a> from the 2008
--   Haskell Symposium. For a full-featured session types library, see the
--   sessions package.
@package simple-sessions
@version 0.1

module Control.Concurrent.SimpleSession.SessionTypes
data Z
data S n
data Eps
data (:!:) a r
data (:?:) a r
data (:+:) r s
data (:&:) r s
data Rec r
data Var v

-- | (:?:)| are declared right associative and with higher precedence than
--   |(:+:)| and |(:&amp;:)|.}
--   
--   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
instance Dual (Var v) (Var v)
instance (Dual r s) => Dual (Rec r) (Rec s)
instance (Dual r1 s1, Dual r2 s2) => Dual (r1 :&: r2) (s1 :+: s2)
instance (Dual r1 s1, Dual r2 s2) => Dual (r1 :+: r2) (s1 :&: s2)
instance Dual Eps Eps
instance (Dual r s) => Dual (a :?: r) (a :!: s)
instance (Dual r s) => Dual (a :!: r) (a :?: s)

module Control.Concurrent.SimpleSession.Implicit

-- | Session| is implemented as the composition of the IO monad with a
--   reader monad carrying a untyped channel.
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) ()

-- | 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:
recv :: Session (Cap e (a :?: r)) (Cap e r) a
close :: Session (Cap e Eps) () ()

-- | 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 :&amp;: 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) ()
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) ()

-- | 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) ()
suc :: Session (Cap (r, e) (Var (S v))) (Cap e (Var v)) ()
class Pop s s' | s -> s'
pop :: (Pop s s') => Session s s' ()
data Rendezvous r
newRendezvous :: IO (Rendezvous r)
accept :: Rendezvous r -> Session (Cap () r) () a -> IO a

-- | 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
instance (Pop (Cap e (Var v)) (Cap e' r')) => Pop (Cap (r, e) (Var (S v))) (Cap e' r')
instance Pop (Cap (r, e) (Var Z)) (Cap (r, e) r)
instance IxMonad Session
instance IxApplicative Session
instance IxPointed Session
instance IxFunctor Session

module Control.Concurrent.SimpleSession.Positional
data Session s s' a
data Cap t e r
data Channel t
io :: IO a -> Session s s a
send :: Channel t -> a -> Session (Cap t e (a :!: r), x) (Cap t e r, x) ()
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) ()
dig :: Session x x' a -> Session (r, x) (r, x') a

-- | swap| may be combined to exchange any two adjacent capabilities.
swap :: Session (r, (s, x)) (s, (r, x)) ()
forkSession :: Session x () () -> Session x () ()
data Rendezvous r
newRendezvous :: IO (Rendezvous r)
accept :: Rendezvous r -> (forall t. Channel t -> Session (Cap t () r, x) y a) -> Session x y a
request :: (Dual r r') => Rendezvous r -> (forall t. Channel t -> Session (Cap t () r', x) y a) -> Session x y a
runSession :: Session () () a -> IO a
instance IxMonad Session
instance IxApplicative Session
instance IxPointed Session
instance IxFunctor Session