full-sessions-0.4.189: yet another implementation of session types which does not require annotationsSource codeContentsIndex
Control.Concurrent.FullSession.Session
Synopsis
newtype Session t ss tt a = Session (IO a)
runS :: (IsEnded ss T, Ended l ss, Length ss l) => (forall t. Session t Nil ss a) -> IO a
(>>>=) :: Session t ss tt a -> (a -> Session t tt uu b) -> Session t ss uu b
ireturn :: a -> Session t ss ss a
io :: IO a -> Session t ss ss a
new :: Length ss l => Session t ss (Cap Nil Bot :|: ss) (Channel t l)
send :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Send v s)) (Cap e s) ss tt) => Channel t n -> v -> Session t ss tt ()
recv :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Recv v s)) (Cap e s) ss tt) => Channel t n -> Session t ss tt v
sel1 :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Select s x)) (Cap e s) ss tt) => Channel t n -> Session t ss tt ()
sel2 :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Select x s)) (Cap e s) ss tt) => Channel t n -> Session t ss tt ()
select :: (Length ss l, Length tt l, Length uu l, Sub l (S n) n', Update n' (Cap e (Select x y)) (Cap e x) uu ss, Update n' (Cap e (Select x y)) (Cap e y) uu tt) => Channel t n -> Bool -> Session t ss xx () -> Session t tt xx () -> Session t uu xx ()
offer :: (Length ss l, Length tt l, Length uu l, Sub l (S n) n', Update n' (Cap e (Offer x y)) (Cap e x) uu ss, Update n' (Cap e (Offer x y)) (Cap e y) uu tt) => Channel t n -> Session t ss xx a -> Session t tt xx a -> Session t uu xx a
sendS :: (Length ss l, Length tt l, Sub l (S n) n', Sub l (S m) m', Update n' (Cap e (Throw u' u)) (Cap e u) ss tt', Update m' (Cap e' u') (Cap e' End) tt' tt) => Channel t n -> Channel t m -> Session t ss tt ()
recvS :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Catch u' u)) (Cap e u) ss tt) => Channel t n -> Session t ss (Cap Nil u' :|: tt) (Channel t l)
sendS_new :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Throw u' u)) (Cap e u) ss tt, Comp2 u' u'') => Channel t n -> Session t ss (Cap Nil u'' :|: tt) (Channel t l)
forkIO :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' ThreadId
forkOS :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' ThreadId
forkOS_ :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' ()
forkIO_ :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' ()
enter :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Rec r)) (Cap (r :|: e) r) ss tt) => Channel t n -> Session t ss tt ()
zero :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap (r :|: e) (Var Z)) (Cap (r :|: e) r) ss tt) => Channel t n -> Session t ss tt ()
suc :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap (r :|: e) (Var (S v))) (Cap e (Var v)) ss tt) => Channel t n -> Session t ss tt ()
recur :: (Sub l2 l d, AppendEnd d ss ss', Sub l2 (S n) n', EndedWithout n' l2 x ss', Length ss l, Length ss' l2, IsEnded tt' T, Length tt' l2, Ended l2 tt') => (Channel t n -> Session t ss tt ()) -> Channel t n -> Session t ss' tt' ()
class IsEnded ss b | ss -> b
class Ended l ss | l -> ss
class Comp s t u | s u -> t, t u -> s, s t -> u
class Comp2 s t | s -> t, t -> s
class Par ss tt' tt | ss tt' -> tt, ss tt -> tt', tt tt' -> ss
class Par2 t ss tt' tt | t ss tt' -> tt, t ss tt -> tt', t tt tt' -> ss
class EndedWithout n l s ss | n l s -> ss
class AppendEnd n ss ss' | n ss -> ss', n ss' -> ss
typecheck :: (Ended l ss, Length ss l, IsEnded ss T) => Session t Nil ss a -> Session t Nil ss a
typecheck' :: Session t Nil ss a -> Session t Nil ss a
Documentation
newtype Session t ss tt a Source
Session monad. t is an index (like in the ST monad), ss is the precondition of the computation, tt is the postcondition of the computation, and a is the return value
Constructors
Session (IO a)
runS :: (IsEnded ss T, Ended l ss, Length ss l) => (forall t. Session t Nil ss a) -> IO aSource
return the value computed by a session. The forall ensures that internal channels used by the session is inaccessible to the rest of the program
(>>>=) :: Session t ss tt a -> (a -> Session t tt uu b) -> Session t ss uu bSource
bind for indexed monad
ireturn :: a -> Session t ss ss aSource

bind, discarding the result of the computation on LHS

return for indexed monad

io :: IO a -> Session t ss ss aSource
run a computation of type IO a
new :: Length ss l => Session t ss (Cap Nil Bot :|: ss) (Channel t l)Source
create a channel
send :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Send v s)) (Cap e s) ss tt) => Channel t n -> v -> Session t ss tt ()Source
output on a channel
recv :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Recv v s)) (Cap e s) ss tt) => Channel t n -> Session t ss tt vSource
input on a channel
sel1 :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Select s x)) (Cap e s) ss tt) => Channel t n -> Session t ss tt ()Source
output a label `1'
sel2 :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Select x s)) (Cap e s) ss tt) => Channel t n -> Session t ss tt ()Source
output a label `2'
select :: (Length ss l, Length tt l, Length uu l, Sub l (S n) n', Update n' (Cap e (Select x y)) (Cap e x) uu ss, Update n' (Cap e (Select x y)) (Cap e y) uu tt) => Channel t n -> Bool -> Session t ss xx () -> Session t tt xx () -> Session t uu xx ()Source
output a label
offer :: (Length ss l, Length tt l, Length uu l, Sub l (S n) n', Update n' (Cap e (Offer x y)) (Cap e x) uu ss, Update n' (Cap e (Offer x y)) (Cap e y) uu tt) => Channel t n -> Session t ss xx a -> Session t tt xx a -> Session t uu xx aSource
input a label i
sendS :: (Length ss l, Length tt l, Sub l (S n) n', Sub l (S m) m', Update n' (Cap e (Throw u' u)) (Cap e u) ss tt', Update m' (Cap e' u') (Cap e' End) tt' tt) => Channel t n -> Channel t m -> Session t ss tt ()Source
output a channel
recvS :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Catch u' u)) (Cap e u) ss tt) => Channel t n -> Session t ss (Cap Nil u' :|: tt) (Channel t l)Source
input a channel
sendS_new :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Throw u' u)) (Cap e u) ss tt, Comp2 u' u'') => Channel t n -> Session t ss (Cap Nil u'' :|: tt) (Channel t l)Source
create a channel, then pass it to other process
forkIO :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' ThreadIdSource
start a new thread
forkOS :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' ThreadIdSource
start a new OS thread
forkOS_ :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' ()Source
forkIO_ :: (Length ss l, Length tt' l, Length tt l, Length ss' l', Ended l' ss', IsEnded ss' T, Par ss tt' tt) => Session t ss ss' () -> Session t tt tt' ()Source
enter :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap e (Rec r)) (Cap (r :|: e) r) ss tt) => Channel t n -> Session t ss tt ()Source
expand a (Rec u) to u (from Pucella and Tov)
zero :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap (r :|: e) (Var Z)) (Cap (r :|: e) r) ss tt) => Channel t n -> Session t ss tt ()Source
replace (Var Z) with recursion body (from Pucella and Tov)
suc :: (Length ss l, Length tt l, Sub l (S n) n', Update n' (Cap (r :|: e) (Var (S v))) (Cap e (Var v)) ss tt) => Channel t n -> Session t ss tt ()Source
(from Pucella and Tov)
recur :: (Sub l2 l d, AppendEnd d ss ss', Sub l2 (S n) n', EndedWithout n' l2 x ss', Length ss l, Length ss' l2, IsEnded tt' T, Length tt' l2, Ended l2 tt') => (Channel t n -> Session t ss tt ()) -> Channel t n -> Session t ss' tt' ()Source
recursion
class IsEnded ss b | ss -> bSource
T if the all elements of ss are Cap Nil End
show/hide Instances
IsEnded Nil T
IsEnded Nil T
IsEnded (Cap e (Var v) :|: ss) F
IsEnded (Cap e (Var v) :|: ss) F
IsEnded (Cap e (Rec r) :|: ss) F
IsEnded (Cap e (Rec r) :|: ss) F
IsEnded (Cap e Bot :|: ss) F
IsEnded (Cap e Bot :|: ss) F
IsEnded (Cap e (Offer x y) :|: ss) F
IsEnded (Cap e (Offer x y) :|: ss) F
IsEnded (Cap e (Select x y) :|: ss) F
IsEnded (Cap e (Select x y) :|: ss) F
IsEnded (Cap e (Catch x y) :|: ss) F
IsEnded (Cap e (Catch x y) :|: ss) F
IsEnded (Cap e (Throw x y) :|: ss) F
IsEnded (Cap e (Throw x y) :|: ss) F
IsEnded (Cap e (Recv x y) :|: ss) F
IsEnded (Cap e (Recv x y) :|: ss) F
IsEnded (Cap e (Send x y) :|: ss) F
IsEnded (Cap e (Send x y) :|: ss) F
IsEnded ss b => IsEnded (Cap Nil End :|: ss) b
class Ended l ss | l -> ssSource
generates a list of ended types
show/hide Instances
Ended Z Nil
Ended Z Nil
(TCast s (Cap Nil End), Ended n ss) => Ended (S n) (s :|: ss)
(TCast s (Cap Nil End), Ended n ss) => Ended (S n) (s :|: ss)
class Comp s t u | s u -> t, t u -> s, s t -> uSource
sesion type algebra
show/hide Instances
Comp c (Cap Nil End) c
Comp (Cap Nil End) c c
(TCast v v', TCast e e', TCast e' Nil) => Comp (Cap e (Var v)) (Cap e' (Var v')) (Cap e'' Bot)
(Comp2 r r', TCast e e', TCast e' Nil) => Comp (Cap e (Rec r)) (Cap e' (Rec r')) (Cap e'' Bot)
(Comp2 u u', Comp2 v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Offer u v)) (Cap e' (Select u' v')) (Cap e'' Bot)
(Comp2 u u', Comp2 v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Select u v)) (Cap e' (Offer u' v')) (Cap e'' Bot)
(Comp2 u u', TCast v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Catch v u)) (Cap e' (Throw v' u')) (Cap e'' Bot)
(Comp2 u u', TCast v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Throw v u)) (Cap e' (Catch v' u')) (Cap e'' Bot)
(Comp2 u u', TCast t t', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Recv t' u')) (Cap e' (Send t u)) (Cap e'' Bot)
(Comp2 u u', TCast t t', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Send t u)) (Cap e' (Recv t' u')) (Cap e'' Bot)
Comp (Cap Nil End) (Cap Nil End) (Cap Nil End)
class Comp2 s t | s -> t, t -> sSource
session type algebra (2)
show/hide Instances
Comp2 End End
TCast v v' => Comp2 (Var v) (Var v')
Comp2 r r' => Comp2 (Rec r) (Rec r')
(Comp2 u u', Comp2 v v') => Comp2 (Offer u v) (Select u' v')
(Comp2 u u', Comp2 v v') => Comp2 (Offer u v) (Select u' v')
(Comp2 u u', Comp2 v v') => Comp2 (Select u v) (Offer u' v')
(Comp2 u u', Comp2 v v') => Comp2 (Select u v) (Offer u' v')
(Comp2 u u', TCast v v') => Comp2 (Catch v u) (Throw v' u')
(Comp2 u u', TCast v v') => Comp2 (Catch v u) (Throw v' u')
(Comp2 u u', TCast v v') => Comp2 (Throw v u) (Catch v' u')
(Comp2 u u', TCast v v') => Comp2 (Throw v u) (Catch v' u')
(Comp2 u u', TCast t t') => Comp2 (Recv t' u') (Send t u)
(Comp2 u u', TCast t t') => Comp2 (Recv t' u') (Send t u)
(Comp2 u u', TCast t t') => Comp2 (Send t u) (Recv t' u')
(Comp2 u u', TCast t t') => Comp2 (Send t u) (Recv t' u')
class Par ss tt' tt | ss tt' -> tt, ss tt -> tt', tt tt' -> ssSource
parallel composition
show/hide Instances
Par Nil Nil Nil
(Comp s t' t, IsEnded ss b, Par2 b ss tt' tt) => Par (s :|: ss) (t' :|: tt') (t :|: tt)
class Par2 t ss tt' tt | t ss tt' -> tt, t ss tt -> tt', t tt tt' -> ssSource
the specialized case for ended ss
show/hide Instances
Par ss tt' tt => Par2 F ss tt' tt
TCast tt' tt => Par2 T ss tt' tt
class EndedWithout n l s ss | n l s -> ssSource
show/hide Instances
(TCast ss (s :|: ss'), TCast l (S l'), Ended l' ss') => EndedWithout Z l s ss
(TCast ss (Cap Nil End :|: ss'), TCast l (S l'), EndedWithout n l' s ss') => EndedWithout (S n) l s ss
class AppendEnd n ss ss' | n ss -> ss', n ss' -> ssSource
show/hide Instances
TCast ss ss' => AppendEnd Z ss ss'
(AppendEnd n ss ss'', TCast ss' (Cap Nil End :|: ss'')) => AppendEnd (S n) ss ss'
typecheck :: (Ended l ss, Length ss l, IsEnded ss T) => Session t Nil ss a -> Session t Nil ss aSource
typecheck' :: Session t Nil ss a -> Session t Nil ss aSource
Produced by Haddock version 2.4.2