Control.Concurrent.SimpleSession.Positional

Documentation

module Control.Concurrent.SimpleSession.SessionTypes

module Control.Monad.Indexed

data Session s s' a

Instances

IxMonad Session

IxFunctor Session

IxApplicative Session

IxPointed Session

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

send_cap :: Channel t -> Session (Cap t e (Cap t' e' r' :!: r), (Cap t' e' r', x)) (Cap t e r, x) ()

recv_cap :: Channel t -> Session (Cap t e (Cap t' e' r' :?: r), x) (Cap t e r, (Cap t' e' r', x)) ()

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 :: Session (r, (s, x)) (s, (r, x)) ()

swap| may be combined to exchange any two adjacent capabilities.

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