- Type level construcs
- Session types (protocol types)
- Session type environments
- The Session monad
- Communication and concurrency primitives
- Utility functions for type inferene
- Type classes for type-level operations
- Type level arithmetics and boolean operators
- Operations on type level lists
- Type classes for ended type environments (1)
- Duality of session types
- Parallel composition of session types
- Type classes for ended type environments (2)
- Restrictions on session types for network communication
- Recursive protocol
- Type equality
Pi-calculus style communication and concurrency primitives which come with session types.
- data Z
- data S n
- data P n
- class Nat n
- data T
- data F
- data Send v u
- data Recv v u
- data Throw u' u
- data Catch u' u
- data Select u1 u2
- data Offer u1 u2
- data End
- data Bot
- data Rec m r
- data Var n
- data Close
- data SelectN u1 u2
- data OfferN u1 u2
- data ss :> s
- data Nil
- data Session t ss tt a
- (>>>=) :: Session t ss tt a -> (a -> Session t tt uu b) -> Session t ss uu b
- (>>>) :: Session t ss tt a -> Session t tt uu b -> Session t ss uu b
- ireturn :: a -> Session t ss ss a
- runS :: Ended n ss => forall a n. (forall t. Session t Nil ss a) -> IO a
- data Channel t n
- data Service u
- close :: (Pickup ss n Close, Update ss n End ss', IsEnded ss F) => Channel t n -> Session t ss ss' ()
- send :: (Pickup ss n (Send v a), Update ss n a ss', IsEnded ss F) => Channel t n -> v -> Session t ss ss' ()
- recv :: (Pickup ss n (Recv v u), Update ss n u ss', IsEnded ss F) => Channel t n -> Session t ss ss' v
- sendS :: (Pickup ss n1 (Throw c1 u1), Update ss n1 u1 ss', Pickup ss' n2 c1, Update ss' n2 End ss'', IsEnded ss F) => Channel t n1 -> Channel t n2 -> Session t ss ss'' ()
- recvS :: (Pickup ss n1 (Catch c1 u1), Update ss n1 u1 ss', SList ss' l, IsEnded ss F) => Channel t n1 -> Session t ss (ss' :> c1) (Channel t l)
- sel1 :: (Pickup ss n (Select s x), Update ss n s tt, IsEnded ss F) => Channel t n -> Session t ss tt ()
- sel2 :: (Pickup ss n (Select x s), Update ss n s tt, IsEnded ss F) => Channel t n -> Session t ss tt ()
- ifSelect :: (Pickup ss n (Select x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Bool -> Session t sx xx a -> Session t sy yy a -> Session t ss zz a
- offer :: (Pickup ss n (Offer x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Session t sx xx a -> Session t sy yy a -> Session t ss zz a
- new :: SList ss l => Session t ss (ss :> Bot) (Channel t l)
- newService :: Dual Z u u' => IO (Service u)
- connect :: (Dual Z u u', SList ss l) => Service u -> Session t ss (ss :> u') (Channel t l)
- connectRunS :: (Dual Z u u', Ended xs n) => Service u -> (forall t. Channel t Z -> Session t (Nil :> u') xs a) -> IO a
- accept :: (Dual Z u u', SList ss l) => Service u -> Session t ss (ss :> u) (Channel t l)
- acceptRunS :: (Dual Z u u', Ended xs n) => Service u -> (forall t. Channel t Z -> Session t (Nil :> u) xs a) -> IO a
- connectNw :: (SList ss l, NwSession u) => NwService u -> Session t ss (ss :> u) (Channel t l)
- connectNw2 :: (SList ss l, NwSendOnly u, NwReceiveOnly u') => NwService2 u u' -> Session t ss ((ss :> u) :> u') (Channel t l, Channel t (S l))
- acceptOneNw2 :: (SList ss l, NwSendOnly u, NwReceiveOnly u') => NwService2 u u' -> Session t ss ((ss :> u) :> u') (Channel t l, Channel t (S l))
- sel1N :: (Pickup ss n (SelectN s x), Update ss n s tt) => Channel t n -> Session t ss tt ()
- sel2N :: (Pickup ss n (SelectN x s), Update ss n s tt) => Channel t n -> Session t ss tt ()
- ifSelectN :: (Pickup ss n (SelectN x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Bool -> Session t sx xx a -> Session t sy yy a -> Session t ss zz a
- offerN :: (NwReceiver x, NwReceiver y, Pickup ss n (OfferN x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Session t sx xx a -> Session t sy yy a -> Session t ss zz a
- dualNw :: NwDual u u' => NwService u -> NwService u'
- dualNw2 :: (NwDual u1 u1', NwDual u2 u2') => NwService2 u1 u2 -> NwService2 u1' u2'
- mkNwService :: NwSession u => String -> Int -> u -> NwService u
- mkNwService2 :: (NwSendOnly u, NwReceiveOnly u') => String -> Int -> u -> u' -> NwService2 u u'
- class Message mes where
- parseMessage :: String -> Maybe (mes, String)
- showMessage :: mes -> String
- forkIOs, forkOSs :: (SList ss l, SList tt' l, SList tt l, Ended l' ss', IsEnded ss b, Par' b ss tt' tt) => Session t ss ss' () -> Session t tt tt' ThreadId
- io :: IO a -> Session t ss ss a
- io_ :: IO a -> Session t ss ss ()
- finallys :: Session t ss tt () -> IO () -> Session t ss tt ()
- unwind0 :: (RecFold Z u r r, RecUnfold Z r r u, Pickup ss n (Rec Z r), Update ss n u tt, IsEnded ss F) => Channel t n -> Session t ss tt ()
- unwind1 :: (RecFold (S Z) u r r, RecUnfold (S Z) r r u, Pickup ss n (Rec (S Z) r), Update ss n u tt, IsEnded ss F) => Channel t n -> Session t ss tt ()
- unwind2 :: (RecFold (S (S Z)) u r r, RecUnfold (S (S Z)) r r u, Pickup ss n (Rec (S (S Z)) r), Update ss n u tt, IsEnded ss F) => Channel t n -> Session t ss tt ()
- recur1 :: (EndedWithout n s ss, AppendEnd ss ss', SList ss' l, Ended l tt) => (Channel t n -> Session t ss tt ()) -> Channel t n -> Session t ss' tt ()
- recur2 :: (EndedWithout2 n m s s' ss, AppendEnd ss ss', SList ss' l, Ended l tt) => (Channel t n -> Channel t m -> Session t ss tt ()) -> Channel t n -> Channel t m -> Session t ss' tt ()
- channeltype1 :: Pickup ss' Z s' => (Channel t Z -> Session t (Nil :> s) ss' a) -> (s, s')
- channeltype2 :: (Pickup ss' Z s', Pickup ss' (S Z) t') => (Channel t Z -> Channel t (S Z) -> Session t ((Nil :> s) :> t) ss' a) -> ((s, s'), (t, t'))
- typecheck1 :: SList ss l => (Channel t l -> Session t (ss :> s1) ss' a) -> Session t (ss :> s1) ss' a
- typecheck2 :: SList ss l => (Channel t l -> Channel t (S l) -> Session t ((ss :> s1) :> s2) ss' a) -> Session t ((ss :> s1) :> s2) ss' a
- class EqNat x y b | x y -> b
- class Sub n n'
- type family SubT n n' :: *
- class And b1 b2 b | b1 b2 -> b
- class SList ss l | ss -> l
- class Pickup ss n s | ss n -> s
- class PickupR ss n s | ss n -> s
- class Update ss n t ss' | ss n t -> ss'
- class UpdateR ss n t ss' | ss n t -> ss'
- class (SList ss n, IsEnded ss T) => Ended n ss | n -> ss
- class IsEnded ss b | ss -> b
- class IsEndedST s b | s -> b
- class Dual n s t | s -> t, t -> s
- class Comp s t u | s u -> t, t u -> s, s t -> u
- class Par ss tt' tt | ss tt' -> tt, ss tt -> tt', tt tt' -> ss
- class Par' t ss tt' tt | t ss tt' -> tt, t ss tt -> tt', t tt tt' -> ss
- class EndedWithout n s ss | n s -> ss
- class EndedWithout' n s l ss | n s l -> ss
- class EndedWithout2 n m s t ss | n s m t -> ss
- class EndedWithout2' n m s t l ss | n m s t l -> ss
- class AppendEnd ss ss'
- class AppendEnd' n ss ss' | n ss -> ss', n ss' -> ss
- class Diff xx yy zz | xx yy -> zz
- class Diff' n xx yy zz | n xx yy -> zz
- data NwService u
- data NwService2 u u'
- class NwSession u => NwSender u
- class NwSession u => NwReceiver u
- class NwSession u
- class (NwSession s, NwSession t) => NwDual s t | s -> t, t -> s
- class NwSession u => NwSendOnly u
- class NwSession u => NwReceiveOnly u
- class RecFold m u s r | m u -> r
- class RecFoldCont b m n a s r | b m n a -> r
- class RecFold2 m u r | m u -> r
- class RecFoldCont2 b m n a r | b m n a -> r
- class RecUnfold m r s u | m r s -> u
- class RecUnfoldCont b m n s a | b m n s -> a
- class TypeEq' () x y b => TypeEq x y b | x y -> b
- class TypeEq' q x y b | q x y -> b
- class TypeEq'' q x y b | q x y -> b
Type level construcs
Type level numbers and booleans
Type level zero.
Show Z | |
Nat Z | |
SList Nil Z | |
Ended Z Nil | |
ss ~ :> ss' t => PickupR ss Z t | |
EqNat Z Z T | |
ss ~ ss' => AppendEnd' Z ss ss' | |
(xx ~ zz, yy ~ zz) => Diff' Z xx yy zz | |
(ss ~ :> ss' s, l ~ S l', Ended l' ss', IsEnded ss' T) => EndedWithout' Z s l ss | |
EqNat Z (S n) F | |
(ss ~ :> ss' s, l ~ S l', EndedWithout' m t l' ss') => EndedWithout2' Z (S m) s t l ss | |
EqNat (S n) Z F | |
(ss ~ :> ss' t, l ~ S l', EndedWithout' n s l' ss') => EndedWithout2' (S n) Z s t l ss | |
UpdateR (:> ss s) Z t (:> ss t) |
Type level successor.
denotes S
n(n+1)
.
Sub n (S (S (S (S (S (S (S (S (S n))))))))) | |
Sub n (S (S (S (S (S (S (S (S n)))))))) | |
Sub n (S (S (S (S (S (S (S n))))))) | |
Sub n (S (S (S (S (S (S n)))))) | |
Sub n (S (S (S (S (S n))))) | |
Sub n (S (S (S (S n)))) | |
Sub n (S (S (S n))) | |
Sub n (S (S n)) | |
Sub n (S n) | |
(ss ~ :> ss' s', PickupR ss' n t) => PickupR ss (S n) t | |
EqNat Z (S n) F | |
(ss ~ :> ss' s, l ~ S l', EndedWithout' m t l' ss') => EndedWithout2' Z (S m) s t l ss | |
Show n => Show (S n) | |
Nat n => Nat (S n) | |
Sub (S n) n | |
Sub (S (S n)) n | |
Sub (S (S (S n))) n | |
Sub (S (S (S (S n)))) n | |
Sub (S (S (S (S (S n))))) n | |
Sub (S (S (S (S (S (S n)))))) n | |
Sub (S (S (S (S (S (S (S n))))))) n | |
Sub (S (S (S (S (S (S (S (S n)))))))) n | |
Sub (S (S (S (S (S (S (S (S (S n))))))))) n | |
EqNat (S n) Z F | |
(ss' ~ :> ss'' End, AppendEnd' n ss ss'') => AppendEnd' (S n) ss ss' | |
(xx ~ :> xx' End, zz ~ :> zz' End, Diff' n xx' yy zz') => Diff' (S n) xx yy zz | |
(ss ~ :> ss' End, l ~ S l', EndedWithout' n s l' ss') => EndedWithout' (S n) s l ss | |
(ss ~ :> ss' t, l ~ S l', EndedWithout' n s l' ss') => EndedWithout2' (S n) Z s t l ss | |
EqNat n n' b => EqNat (S n) (S n') b | |
(ss ~ :> ss' End, l ~ S l', EndedWithout2' n m s t l' ss') => EndedWithout2' (S n) (S m) s t l ss | |
Ended n ss => Ended (S n) (:> ss End) | |
SList ss l => SList (:> ss s) (S l) | |
UpdateR ss n t ss' => UpdateR (:> ss s) (S n) t (:> ss' s) |
Type level predecessor (only for internal use).
denotes P
n(n-1)
.
Type level True
.
Type level False
.
IsEndedST Close F | |
IsEndedST Bot F | |
And b F F | |
And F b F | |
(IsEnded ss F, Par ss tt' tt) => Par' F ss tt' tt | |
(RecFold2 n s s', RecUnfold n s' xx s, RecFold m a s' r) => RecFoldCont F m n a s (Rec n r) | |
RecUnfoldCont F m n s (Var n) | |
RecFold2 m a r => RecFoldCont2 F m n a (Rec n r) | |
EqNat Z (S n) F | |
IsEndedST (Var v) F | |
EqNat (S n) Z F | |
IsEndedST (OfferN x y) F | |
IsEndedST (SelectN x y) F | |
IsEndedST (Rec n r) F | |
IsEndedST (Offer x y) F | |
IsEndedST (Select x y) F | |
IsEndedST (Catch x y) F | |
IsEndedST (Throw x y) F | |
IsEndedST (Recv x y) F | |
IsEndedST (Send x y) F | |
IsEnded (:> ss (Var v)) F | |
IsEnded (:> ss (Rec n r)) F | |
IsEnded (:> ss Close) F | |
IsEnded (:> ss Bot) F | |
IsEnded (:> ss (OfferN x y)) F | |
IsEnded (:> ss (SelectN x y)) F | |
IsEnded (:> ss (Offer x y)) F | |
IsEnded (:> ss (Select x y)) F | |
IsEnded (:> ss (Catch x y)) F | |
IsEnded (:> ss (Throw x y)) F | |
IsEnded (:> ss (Recv x y)) F | |
IsEnded (:> ss (Send x y)) F |
Session types (protocol types)
denotes a protocol to emit a value of type Send
v uv
followed by a behavior of type u
.
Use of
on a channel changes its session type from send
into Send
v uu
.
(v ~ v', RecUnfold m u s u') => RecUnfold m (Send v u) s (Send v' u') | |
(v ~ v', RecFold m u s u') => RecFold m (Send v u) s (Send v' u') | |
(v ~ v'', u ~ u'') => Comp End (Send v u) (Send v'' u'') | |
(t ~ t', Dual n u' u) => Dual n (Recv t' u') (Send t u) | |
(t ~ t', Dual n u u') => Dual n (Send t u) (Recv t' u') | |
(v ~ v', RecFold2 m u u') => RecFold2 m (Send v u) (Send v' u') | |
(NwSendOnly u, Message v) => NwSendOnly (Send v u) | |
(Message v, NwSession u) => NwSession (Send v u) | |
(NwSession u, Message v) => NwSender (Send v u) | |
IsEndedST (Send x y) F | |
IsEnded (:> ss (Send x y)) F | |
(v ~ v'', u ~ u'') => Comp (Send v u) End (Send v'' u'') | |
(t ~ t', Message t, Message t', NwDual u' u) => NwDual (Recv t' u') (Send t u) | |
(t ~ t', Message t, Message t', NwDual u u') => NwDual (Send t u) (Recv t' u') | |
(t ~ t', Dual Z u u') => Comp (Recv t u) (Send t' u') Bot | |
(t ~ t', Dual Z u u') => Comp (Send t u) (Recv t' u') Bot |
denotes a protocol of receiving a value of type Recv
v uv
followed by a behavior of type u
.
Use of
on a channel changes its session type from recv
into Recv
v uu
.
(v ~ v', RecUnfold m u s u') => RecUnfold m (Recv v u) s (Recv v' u') | |
(v ~ v', RecFold m u s u') => RecFold m (Recv v u) s (Recv v' u') | |
(v ~ v'', u ~ u'') => Comp End (Recv v u) (Recv v'' u'') | |
(t ~ t', Dual n u' u) => Dual n (Recv t' u') (Send t u) | |
(t ~ t', Dual n u u') => Dual n (Send t u) (Recv t' u') | |
(v ~ v', RecFold2 m u u') => RecFold2 m (Recv v u) (Recv v' u') | |
(NwReceiveOnly u, Message v) => NwReceiveOnly (Recv v u) | |
(Message v, NwSession u) => NwSession (Recv v u) | |
(NwSession u, Message v) => NwReceiver (Recv v u) | |
IsEndedST (Recv x y) F | |
IsEnded (:> ss (Recv x y)) F | |
(v ~ v'', u ~ u'') => Comp (Recv v u) End (Recv v'' u'') | |
(t ~ t', Message t, Message t', NwDual u' u) => NwDual (Recv t' u') (Send t u) | |
(t ~ t', Message t, Message t', NwDual u u') => NwDual (Send t u) (Recv t' u') | |
(t ~ t', Dual Z u u') => Comp (Recv t u) (Send t' u') Bot | |
(t ~ t', Dual Z u u') => Comp (Send t u) (Recv t' u') Bot |
denotes a behavior to output of a channel with session type Throw
u1 u2u1
followed by a behavior of type u2
.
Use of
on a channel changes its session type from sendS
into Throw
u1 u2u2
.
(v ~ v', RecUnfold m u s u') => RecUnfold m (Throw v u) s (Throw v' u') | |
(v ~ v', RecFold m u s u') => RecFold m (Throw v u) s (Throw v' u') | |
(u1 ~ u1'', u ~ u'') => Comp End (Throw u1 u) (Throw u1'' u'') | |
(v ~ v', Dual n u u') => Dual n (Catch v u) (Throw v' u') | |
(v ~ v', Dual n u u') => Dual n (Throw v u) (Catch v' u') | |
(v ~ v', RecFold2 m u u') => RecFold2 m (Throw v u) (Throw v' u') | |
IsEndedST (Throw x y) F | |
IsEnded (:> ss (Throw x y)) F | |
(u1 ~ u1'', u ~ u'') => Comp (Throw u1 u) End (Throw u1'' u'') | |
(t ~ t', Dual Z u u') => Comp (Catch t u) (Throw t' u') Bot | |
(t ~ t', Dual Z u u') => Comp (Throw t u) (Catch t' u') Bot |
is the input of a channel with session type Catch
u1 u2u1
followed by a behavior of type u2
.
Use of
on a channel changes its session type from recvS
into Catch
u1 u2u2
.
(v ~ v', RecUnfold m u s u') => RecUnfold m (Catch v u) s (Catch v' u') | |
(v ~ v', RecFold m u s u') => RecFold m (Catch v u) s (Catch v' u') | |
(u1 ~ u1'', u ~ u'') => Comp End (Catch u1 u) (Catch u1'' u'') | |
(v ~ v', Dual n u u') => Dual n (Catch v u) (Throw v' u') | |
(v ~ v', Dual n u u') => Dual n (Throw v u) (Catch v' u') | |
(v ~ v', RecFold2 m u u') => RecFold2 m (Catch v u) (Catch v' u') | |
IsEndedST (Catch x y) F | |
IsEnded (:> ss (Catch x y)) F | |
(u1 ~ u1'', u ~ u'') => Comp (Catch u1 u) End (Catch u1'' u'') | |
(t ~ t', Dual Z u u') => Comp (Catch t u) (Throw t' u') Bot | |
(t ~ t', Dual Z u u') => Comp (Throw t u) (Catch t' u') Bot |
denotes to be either behavior of type Select
u1 u2u1
or type u2
after emitting a corresponding label 1
or 2
.
Use of
or sel1
on a channel changes its session type from sel2
into Select
u1 u2u1
or u2
, respectively.
(RecUnfold m u1 s u1', RecUnfold m u2 s u2') => RecUnfold m (Select u1 u2) s (Select u1' u2') | |
(RecFold m u1 s u1', RecFold m u2 s u2') => RecFold m (Select u1 u2) s (Select u1' u2') | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (Select u1 u2) (Select u1'' u2'') | |
(Dual n u1 u1', Dual n u2 u2') => Dual n (Offer u1 u2) (Select u1' u2') | |
(Dual n u1 u1', Dual n u2 u2') => Dual n (Select u1 u2) (Offer u1' u2') | |
(RecFold2 m u1 u1', RecFold2 m u2 u2') => RecFold2 m (Select u1 u2) (Select u1' u2') | |
IsEndedST (Select x y) F | |
IsEnded (:> ss (Select x y)) F | |
(u1 ~ u1'', u2 ~ u2'') => Comp (Select u1 u2) End (Select u1'' u2'') | |
(Dual Z u1 u1', Dual Z u2 u2') => Comp (Offer u1 u2) (Select u1' u2') Bot | |
(Dual Z u1 u1', Dual Z u2 u2') => Comp (Select u1 u2) (Offer u1' u2') Bot |
denotes a behavior like either Offer
u1 u2u1
or u2
according to the incoming label.
(RecUnfold m u1 s u1', RecUnfold m u2 s u2') => RecUnfold m (Offer u1 u2) s (Offer u1' u2') | |
(RecFold m u1 s u1', RecFold m u2 s u2') => RecFold m (Offer u1 u2) s (Offer u1' u2') | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (Offer u1 u2) (Offer u1'' u2'') | |
(Dual n u1 u1', Dual n u2 u2') => Dual n (Offer u1 u2) (Select u1' u2') | |
(Dual n u1 u1', Dual n u2 u2') => Dual n (Select u1 u2) (Offer u1' u2') | |
(RecFold2 m u1 u1', RecFold2 m u2 u2') => RecFold2 m (Offer u1 u2) (Offer u1' u2') | |
IsEndedST (Offer x y) F | |
IsEnded (:> ss (Offer x y)) F | |
(u1 ~ u1'', u2 ~ u2'') => Comp (Offer u1 u2) End (Offer u1'' u2'') | |
(Dual Z u1 u1', Dual Z u2 u2') => Comp (Offer u1 u2) (Select u1' u2') Bot | |
(Dual Z u1 u1', Dual Z u2 u2') => Comp (Select u1 u2) (Offer u1' u2') Bot |
End
denotes a terminated session. Further communication along a channel with type End
cannot take place.
IsEndedST End T | |
Comp Close End Close | |
Comp End Close Close | |
Comp End End End | |
Comp End Bot Bot | |
Comp Bot End Bot | |
Dual n End End | |
RecFold2 m End End | |
RecUnfold m End s End | |
RecFold m End s End | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (OfferN u1 u2) (OfferN u1'' u2'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (SelectN u1 u2) (SelectN u1'' u2'') | |
(u ~ u'', m ~ Z, m' ~ Z) => Comp End (Rec m u) (Rec m' u'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (Offer u1 u2) (Offer u1'' u2'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (Select u1 u2) (Select u1'' u2'') | |
(u1 ~ u1'', u ~ u'') => Comp End (Catch u1 u) (Catch u1'' u'') | |
(u1 ~ u1'', u ~ u'') => Comp End (Throw u1 u) (Throw u1'' u'') | |
(v ~ v'', u ~ u'') => Comp End (Recv v u) (Recv v'' u'') | |
(v ~ v'', u ~ u'') => Comp End (Send v u) (Send v'' u'') | |
Ended n ss => Ended (S n) (:> ss End) | |
IsEnded ss b => IsEnded (:> ss End) b | |
(u1 ~ u1'', u2 ~ u2'') => Comp (OfferN u1 u2) End (OfferN u1'' u2'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp (SelectN u1 u2) End (SelectN u1'' u2'') | |
(u ~ u'', m ~ Z, m' ~ Z) => Comp (Rec m u) End (Rec m' u'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp (Offer u1 u2) End (Offer u1'' u2'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp (Select u1 u2) End (Select u1'' u2'') | |
(u1 ~ u1'', u ~ u'') => Comp (Catch u1 u) End (Catch u1'' u'') | |
(u1 ~ u1'', u ~ u'') => Comp (Throw u1 u) End (Throw u1'' u'') | |
(v ~ v'', u ~ u'') => Comp (Recv v u) End (Recv v'' u'') | |
(v ~ v'', u ~ u'') => Comp (Send v u) End (Send v'' u'') |
Bot
is the type for a channel whose both endpoints are already engaged by two processes, so that no further processes can own that channel.
For example, in forkIO (send k e) >>> recv k
, k
has type Bot
.
IsEndedST Bot F | |
Comp End Bot Bot | |
Comp Bot End Bot | |
IsEnded (:> ss Bot) F | |
(m ~ Z, m' ~ Z, Dual (S Z) r r') => Comp (Rec m r) (Rec m' r') Bot | |
(Dual Z u1 u1', Dual Z u2 u2') => Comp (Offer u1 u2) (Select u1' u2') Bot | |
(Dual Z u1 u1', Dual Z u2 u2') => Comp (Select u1 u2) (Offer u1' u2') Bot | |
(t ~ t', Dual Z u u') => Comp (Catch t u) (Throw t' u') Bot | |
(t ~ t', Dual Z u u') => Comp (Throw t u) (Catch t' u') Bot | |
(t ~ t', Dual Z u u') => Comp (Recv t u) (Send t' u') Bot | |
(t ~ t', Dual Z u u') => Comp (Send t u) (Recv t' u') Bot |
denotes recursive session, where Rec
m rm
represents the binder of recursion variable.
a type-level natural numer (like
). nesting level of S
Z
, and
Rec
r
is the body of the recursion which may contain
.
Var
m
(RecFold2 n s s', RecUnfold n s' xx s, RecFold m a s' r) => RecFoldCont F m n a s (Rec n r) | |
RecUnfoldCont T m n s (Rec m s) | |
RecFold2 m a r => RecFoldCont2 F m n a (Rec n r) | |
(TypeEq m n b, RecFoldCont2 b m n a r) => RecFold2 m (Rec n a) r | |
(TypeEq m n b, RecFoldCont b m n a s r) => RecFold m (Rec n a) s r | |
(RecFold2 n s s', RecUnfold m a s' a') => RecUnfold m (Rec n a) s (Rec n a') | |
(u ~ u'', m ~ Z, m' ~ Z) => Comp End (Rec m u) (Rec m' u'') | |
(n ~ m, n ~ m', Dual (S n) r r') => Dual n (Rec m r) (Rec m' r') | |
(Show m, Show r) => Show (Rec m r) | |
(NwReceiveOnly u, Nat m) => NwReceiveOnly (Rec m u) | |
(NwSendOnly u, Nat m) => NwSendOnly (Rec m u) | |
(NwSession u, Nat m) => NwSession (Rec m u) | |
IsEndedST (Rec n r) F | |
IsEnded (:> ss (Rec n r)) F | |
(u ~ u'', m ~ Z, m' ~ Z) => Comp (Rec m u) End (Rec m' u'') | |
(m ~ m', NwDual r r', Nat m) => NwDual (Rec m r) (Rec m' r') | |
(m ~ Z, m' ~ Z, Dual (S Z) r r') => Comp (Rec m r) (Rec m' r') Bot |
Recursion variable.
a ~ s => RecFoldCont T m n a s (Var m) | |
RecUnfoldCont F m n s (Var n) | |
RecFoldCont2 T m n a (Var m) | |
(TypeEq m n b, RecUnfoldCont b m n s a) => RecUnfold m (Var n) s a | |
RecFold m (Var n) s (Var n) | |
(v ~ v', Nat v) => Dual n (Var v) (Var v') | |
RecFold2 m (Var n) (Var n) | |
Show n => Show (Var n) | |
Nat n => NwReceiveOnly (Var n) | |
Nat n => NwSendOnly (Var n) | |
Nat n => NwSession (Var n) | |
IsEndedST (Var v) F | |
(v ~ v', Nat v) => NwDual (Var v) (Var v') | |
IsEnded (:> ss (Var v)) F |
denotes a session that can do nothing but closing it.
Close
(RecUnfold m u1 s u1', RecUnfold m u2 s u2') => RecUnfold m (SelectN u1 u2) s (SelectN u1' u2') | |
(RecFold m u1 s u1', RecFold m u2 s u2') => RecFold m (SelectN u1 u2) s (SelectN u1' u2') | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (SelectN u1 u2) (SelectN u1'' u2'') | |
(RecFold2 m u1 u1', RecFold2 m u2 u2') => RecFold2 m (SelectN u1 u2) (SelectN u1' u2') | |
(NwSendOnly u1, NwSendOnly u2, NwSender u1, NwSender u2) => NwSendOnly (SelectN u1 u2) | |
(NwSender u1, NwSender u2) => NwSession (SelectN u1 u2) | |
(NwSender u1, NwSender u2) => NwSender (SelectN u1 u2) | |
IsEndedST (SelectN x y) F | |
IsEnded (:> ss (SelectN x y)) F | |
(u1 ~ u1'', u2 ~ u2'') => Comp (SelectN u1 u2) End (SelectN u1'' u2'') | |
(NwReceiver u1, NwSender u1', NwReceiver u2, NwSender u2', NwDual u1 u1', NwDual u2 u2') => NwDual (OfferN u1 u2) (SelectN u1' u2') | |
(NwSender u1, NwReceiver u1', NwSender u2, NwReceiver u2', NwDual u1 u1', NwDual u2 u2') => NwDual (SelectN u1 u2) (OfferN u1' u2') |
(RecUnfold m u1 s u1', RecUnfold m u2 s u2') => RecUnfold m (OfferN u1 u2) s (OfferN u1' u2') | |
(RecFold m u1 s u1', RecFold m u2 s u2') => RecFold m (OfferN u1 u2) s (OfferN u1' u2') | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (OfferN u1 u2) (OfferN u1'' u2'') | |
(RecFold2 m u1 u1', RecFold2 m u2 u2') => RecFold2 m (OfferN u1 u2) (OfferN u1' u2') | |
(NwReceiveOnly u1, NwReceiveOnly u2, NwReceiver u1, NwReceiver u2) => NwReceiveOnly (OfferN u1 u2) | |
(NwReceiver u1, NwReceiver u2) => NwSession (OfferN u1 u2) | |
(NwReceiver u1, NwReceiver u2) => NwReceiver (OfferN u1 u2) | |
IsEndedST (OfferN x y) F | |
IsEnded (:> ss (OfferN x y)) F | |
(u1 ~ u1'', u2 ~ u2'') => Comp (OfferN u1 u2) End (OfferN u1'' u2'') | |
(NwReceiver u1, NwSender u1', NwReceiver u2, NwSender u2', NwDual u1 u1', NwDual u2 u2') => NwDual (OfferN u1 u2) (SelectN u1' u2') | |
(NwSender u1, NwReceiver u1', NwSender u2, NwReceiver u2', NwDual u1 u1', NwDual u2 u2') => NwDual (SelectN u1 u2) (OfferN u1' u2') |
Session type environments
Type-level snoc (reversed version of cons (:)
). ss :> s
denotes a list ss
with s
on its end. (FIXME:English)
Ended n ss => Ended (S n) (:> ss End) | |
IsEnded ss b => IsEnded (:> ss End) b | |
(IsEnded ss b1, IsEndedST s b2, And b1 b2 b) => IsEnded (:> ss s) b | |
IsEnded (:> ss (Var v)) F | |
IsEnded (:> ss (Rec n r)) F | |
IsEnded (:> ss Close) F | |
IsEnded (:> ss Bot) F | |
IsEnded (:> ss (OfferN x y)) F | |
IsEnded (:> ss (SelectN x y)) F | |
IsEnded (:> ss (Offer x y)) F | |
IsEnded (:> ss (Select x y)) F | |
IsEnded (:> ss (Catch x y)) F | |
IsEnded (:> ss (Throw x y)) F | |
IsEnded (:> ss (Recv x y)) F | |
IsEnded (:> ss (Send x y)) F | |
UpdateR (:> ss s) Z t (:> ss t) | |
SList ss l => SList (:> ss s) (S l) | |
UpdateR ss n t ss' => UpdateR (:> ss s) (S n) t (:> ss' s) | |
(Comp s t' t, IsEnded ss b, Par' b ss tt' tt) => Par (:> ss s) (:> tt' t') (:> tt t) |
The Session monad
The Session
monad. ss
and tt
denotes the usage of channels.
-
ss
denotes pre-type, which denotes the type-level list of session types required to run the session. -
tt
denotes post-type, which denotes the type-level lists of session types produced by the session.
t
denotes a type-tag, which prevents abuse of use of channels. For detail, see runS
.
(>>>=) :: Session t ss tt a -> (a -> Session t tt uu b) -> Session t ss uu bSource
Bind (a.k.a >>=
) operation for Session
monad.
runS :: Ended n ss => forall a n. (forall t. Session t Nil ss a) -> IO aSource
runS
runs the Session
. The pretype (see Session
) must be Nil
.
The posttype must be Ended
, i.e. all channels must be End
.
Forall'd type variable t
prevents abuse of use of channels inside different run.
For example, new >>>= c ->
is rejected by the Haskell typechecker with error io_
(runS ( ... send c ...) )Inferred type is less polymorphic than expected
.
Communication and concurrency primitives
Channel types
The channel type. The type-level number n
points to the session-type in type environments. For example, in the type
Session t (Nil:>Send Int End) (Nil:>End) ()
,
the usage of the channel c :: Channel t Z
is Send Int End
in pretype and End
in posttype.
General communication
close :: (Pickup ss n Close, Update ss n End ss', IsEnded ss F) => Channel t n -> Session t ss ss' ()Source
send :: (Pickup ss n (Send v a), Update ss n a ss', IsEnded ss F) => Channel t n -> v -> Session t ss ss' ()Source
recv :: (Pickup ss n (Recv v u), Update ss n u ss', IsEnded ss F) => Channel t n -> Session t ss ss' vSource
sendS :: (Pickup ss n1 (Throw c1 u1), Update ss n1 u1 ss', Pickup ss' n2 c1, Update ss' n2 End ss'', IsEnded ss F) => Channel t n1 -> Channel t n2 -> Session t ss ss'' ()Source
recvS :: (Pickup ss n1 (Catch c1 u1), Update ss n1 u1 ss', SList ss' l, IsEnded ss F) => Channel t n1 -> Session t ss (ss' :> c1) (Channel t l)Source
sel1 :: (Pickup ss n (Select s x), Update ss n s tt, IsEnded ss F) => Channel t n -> Session t ss tt ()Source
output a label `1'
sel2 :: (Pickup ss n (Select x s), Update ss n s tt, IsEnded ss F) => Channel t n -> Session t ss tt ()Source
output a label `2'
ifSelect :: (Pickup ss n (Select x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Bool -> Session t sx xx a -> Session t sy yy a -> Session t ss zz aSource
offer :: (Pickup ss n (Offer x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Session t sx xx a -> Session t sy yy a -> Session t ss zz aSource
connectRunS :: (Dual Z u u', Ended xs n) => Service u -> (forall t. Channel t Z -> Session t (Nil :> u') xs a) -> IO aSource
acceptRunS :: (Dual Z u u', Ended xs n) => Service u -> (forall t. Channel t Z -> Session t (Nil :> u) xs a) -> IO aSource
Network communication
Primitives
connectNw2 :: (SList ss l, NwSendOnly u, NwReceiveOnly u') => NwService2 u u' -> Session t ss ((ss :> u) :> u') (Channel t l, Channel t (S l))Source
acceptOneNw2 :: (SList ss l, NwSendOnly u, NwReceiveOnly u') => NwService2 u u' -> Session t ss ((ss :> u) :> u') (Channel t l, Channel t (S l))Source
sel1N :: (Pickup ss n (SelectN s x), Update ss n s tt) => Channel t n -> Session t ss tt ()Source
output a label `1'
ifSelectN :: (Pickup ss n (SelectN x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Bool -> Session t sx xx a -> Session t sy yy a -> Session t ss zz aSource
offerN :: (NwReceiver x, NwReceiver y, Pickup ss n (OfferN x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Session t sx xx a -> Session t sy yy a -> Session t ss zz aSource
dualNw2 :: (NwDual u1 u1', NwDual u2 u2') => NwService2 u1 u2 -> NwService2 u1' u2'Source
mkNwService2 :: (NwSendOnly u, NwReceiveOnly u') => String -> Int -> u -> u' -> NwService2 u u'Source
Type class for messages
parseMessage :: String -> Maybe (mes, String)Source
showMessage :: mes -> StringSource
Thread creation
forkIOs, forkOSs :: (SList ss l, SList tt' l, SList tt l, Ended l' ss', IsEnded ss b, Par' b ss tt' tt) => Session t ss ss' () -> Session t tt tt' ThreadIdSource
start a new thread
Interfacing with the IO monad
Exception handling
Recursive protocol support
unwind0 :: (RecFold Z u r r, RecUnfold Z r r u, Pickup ss n (Rec Z r), Update ss n u tt, IsEnded ss F) => Channel t n -> Session t ss tt ()Source
unwind1 :: (RecFold (S Z) u r r, RecUnfold (S Z) r r u, Pickup ss n (Rec (S Z) r), Update ss n u tt, IsEnded ss F) => Channel t n -> Session t ss tt ()Source
unwind2 :: (RecFold (S (S Z)) u r r, RecUnfold (S (S Z)) r r u, Pickup ss n (Rec (S (S Z)) r), Update ss n u tt, IsEnded ss F) => Channel t n -> Session t ss tt ()Source
recur1 :: (EndedWithout n s ss, AppendEnd ss ss', SList ss' l, Ended l tt) => (Channel t n -> Session t ss tt ()) -> Channel t n -> Session t ss' tt ()Source
recur2 :: (EndedWithout2 n m s s' ss, AppendEnd ss ss', SList ss' l, Ended l tt) => (Channel t n -> Channel t m -> Session t ss tt ()) -> Channel t n -> Channel t m -> Session t ss' tt ()Source
Utility functions for type inferene
channeltype2 :: (Pickup ss' Z s', Pickup ss' (S Z) t') => (Channel t Z -> Channel t (S Z) -> Session t ((Nil :> s) :> t) ss' a) -> ((s, s'), (t, t'))Source
typecheck1 :: SList ss l => (Channel t l -> Session t (ss :> s1) ss' a) -> Session t (ss :> s1) ss' aSource
typecheck2 :: SList ss l => (Channel t l -> Channel t (S l) -> Session t ((ss :> s1) :> s2) ss' a) -> Session t ((ss :> s1) :> s2) ss' aSource
Type classes for type-level operations
Type level arithmetics and boolean operators
class EqNat x y b | x y -> bSource
Equality on type-level natural numbers. b ~
if T
x == y
. Otherwise b ~ F
.
Computes subtraction of n
by n'
(FIXME:OK?)
Sub n n | |
Sub n (S (S (S (S (S (S (S (S (S n))))))))) | |
Sub n (S (S (S (S (S (S (S (S n)))))))) | |
Sub n (S (S (S (S (S (S (S n))))))) | |
Sub n (S (S (S (S (S (S n)))))) | |
Sub n (S (S (S (S (S n))))) | |
Sub n (S (S (S (S n)))) | |
Sub n (S (S (S n))) | |
Sub n (S (S n)) | |
Sub n (S n) | |
Sub (S n) n | |
Sub (S (S n)) n | |
Sub (S (S (S n))) n | |
Sub (S (S (S (S n)))) n | |
Sub (S (S (S (S (S n))))) n | |
Sub (S (S (S (S (S (S n)))))) n | |
Sub (S (S (S (S (S (S (S n))))))) n | |
Sub (S (S (S (S (S (S (S (S n)))))))) n | |
Sub (S (S (S (S (S (S (S (S (S n))))))))) n |
Operations on type level lists
class SList ss l | ss -> lSource
The class which covers session-type environments. The second parameter of the class denotes the length of the list.
class Pickup ss n s | ss n -> sSource
denotes that the Pickup
ss n sn
-th element of the list ss
is s
.
This type class plays an important role in session-type inference.
Formally,
if Pickup
ss n ss = pickup ss n
where pickup
is:
pickup ss n = pickupR ss (len ss - (n+1)) where pickupR (ss:>s) Z = s pickupR (ss:>s) (S n) = pickupR ss n len Nil = 0 len (ss:>s) = (len ss) + 1
For example, Pickup (End :> Bot :> Send Int End) Z t)
is an instance of Pickup
, and t
is unified with Bot
.
Note that the list counts from left to right.
For example, The 0
-th element of the list ((Nil :> End) :> Bot) :> Send Int End
is End
.
Usually the list is accessed from the right end. The context
SList
ss (S n),Pickup
(ss:>Bot:>Recv Char End) n s
is expanded into
SList
ss (S n),PickupR
(ss:>Bot:>Recv Char End) (SubT
(S n) (S n)) s,Sub
(S n) (S n)
since
, it will be reduced to
SubT
(S
n) (S
n) ~ Z
PickupR
(ss:>Bot:>Recv Char End) Z s
and then s
is unified with Recv Char End
.
class Update ss n t ss' | ss n t -> ss'Source
denotes that Update
ss n t ss'ss'
is same as ss
except that its n
-th element is t
.
Formally,
if Update
ss n t ss'ss' = update ss n t
where update
is:
update ss n t = updateR ss (len ss - (n+1)) t where updateR (ss:>_) Z t = ss :> t updateR (ss:>s) (S n) t = updateR ss n t :> s len Nil = 0 len (ss:>s) = (len ss) + 1
In other words,
is an instance of Update
(End :> Bot :> Send Int End) Z End (End :> Bot :> End))Update
.
Note that the list counts from left to right, as in the case of Pickup
.
Type classes for ended type environments (1)
class (SList ss n, IsEnded ss T) => Ended n ss | n -> ssSource
class IsEnded ss b | ss -> bSource
denotes that b ~ T if IsEnded
ss bss
is Ended, otherwise b ~ F
. In other words, b ~ T
if the all elements of ss are End
IsEnded Nil T | |
IsEnded ss b => IsEnded (:> ss End) b | |
(IsEnded ss b1, IsEndedST s b2, And b1 b2 b) => IsEnded (:> ss s) b | |
IsEnded (:> ss (Var v)) F | |
IsEnded (:> ss (Rec n r)) F | |
IsEnded (:> ss Close) F | |
IsEnded (:> ss Bot) F | |
IsEnded (:> ss (OfferN x y)) F | |
IsEnded (:> ss (SelectN x y)) F | |
IsEnded (:> ss (Offer x y)) F | |
IsEnded (:> ss (Select x y)) F | |
IsEnded (:> ss (Catch x y)) F | |
IsEnded (:> ss (Throw x y)) F | |
IsEnded (:> ss (Recv x y)) F | |
IsEnded (:> ss (Send x y)) F |
Duality of session types
class Dual n s t | s -> t, t -> sSource
duality
Dual n Close Close | |
Dual n End End | |
(v ~ v', Nat v) => Dual n (Var v) (Var v') | |
(n ~ m, n ~ m', Dual (S n) r r') => Dual n (Rec m r) (Rec m' r') | |
(v ~ v', Dual n u u') => Dual n (Catch v u) (Throw v' u') | |
(v ~ v', Dual n u u') => Dual n (Throw v u) (Catch v' u') | |
(Dual n u1 u1', Dual n u2 u2') => Dual n (Offer u1 u2) (Select u1' u2') | |
(Dual n u1 u1', Dual n u2 u2') => Dual n (Select u1 u2) (Offer u1' u2') | |
(t ~ t', Dual n u' u) => Dual n (Recv t' u') (Send t u) | |
(t ~ t', Dual n u u') => Dual n (Send t u) (Recv t' u') |
Parallel composition of session types
class Comp s t u | s u -> t, t u -> s, s t -> uSource
sesion type algebra
Comp Close End Close | |
Comp End Close Close | |
Comp End End End | |
Comp End Bot Bot | |
Comp Bot End Bot | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (OfferN u1 u2) (OfferN u1'' u2'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (SelectN u1 u2) (SelectN u1'' u2'') | |
(u ~ u'', m ~ Z, m' ~ Z) => Comp End (Rec m u) (Rec m' u'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (Offer u1 u2) (Offer u1'' u2'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp End (Select u1 u2) (Select u1'' u2'') | |
(u1 ~ u1'', u ~ u'') => Comp End (Catch u1 u) (Catch u1'' u'') | |
(u1 ~ u1'', u ~ u'') => Comp End (Throw u1 u) (Throw u1'' u'') | |
(v ~ v'', u ~ u'') => Comp End (Recv v u) (Recv v'' u'') | |
(v ~ v'', u ~ u'') => Comp End (Send v u) (Send v'' u'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp (OfferN u1 u2) End (OfferN u1'' u2'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp (SelectN u1 u2) End (SelectN u1'' u2'') | |
(u ~ u'', m ~ Z, m' ~ Z) => Comp (Rec m u) End (Rec m' u'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp (Offer u1 u2) End (Offer u1'' u2'') | |
(u1 ~ u1'', u2 ~ u2'') => Comp (Select u1 u2) End (Select u1'' u2'') | |
(u1 ~ u1'', u ~ u'') => Comp (Catch u1 u) End (Catch u1'' u'') | |
(u1 ~ u1'', u ~ u'') => Comp (Throw u1 u) End (Throw u1'' u'') | |
(v ~ v'', u ~ u'') => Comp (Recv v u) End (Recv v'' u'') | |
(v ~ v'', u ~ u'') => Comp (Send v u) End (Send v'' u'') | |
(m ~ Z, m' ~ Z, Dual (S Z) r r') => Comp (Rec m r) (Rec m' r') Bot | |
(Dual Z u1 u1', Dual Z u2 u2') => Comp (Offer u1 u2) (Select u1' u2') Bot | |
(Dual Z u1 u1', Dual Z u2 u2') => Comp (Select u1 u2) (Offer u1' u2') Bot | |
(t ~ t', Dual Z u u') => Comp (Catch t u) (Throw t' u') Bot | |
(t ~ t', Dual Z u u') => Comp (Throw t u) (Catch t' u') Bot | |
(t ~ t', Dual Z u u') => Comp (Recv t u) (Send t' u') Bot | |
(t ~ t', Dual Z u u') => Comp (Send t u) (Recv t' u') Bot |
class Par ss tt' tt | ss tt' -> tt, ss tt -> tt', tt tt' -> ssSource
pointwise extension of Comp
-- FIXME: method
class Par' t ss tt' tt | t ss tt' -> tt, t ss tt -> tt', t tt tt' -> ssSource
the specialized case for ended
ss -- FIXME
Type classes for ended type environments (2)
class EndedWithout n s ss | n s -> ssSource
(SList ss l, EndedWithout' (SubT l (S n)) s l ss) => EndedWithout n s ss |
class EndedWithout' n s l ss | n s l -> ssSource
(ss ~ :> ss' s, l ~ S l', Ended l' ss', IsEnded ss' T) => EndedWithout' Z s l ss | |
(ss ~ :> ss' End, l ~ S l', EndedWithout' n s l' ss') => EndedWithout' (S n) s l ss |
class EndedWithout2 n m s t ss | n s m t -> ssSource
(SList ss l, EndedWithout2' (SubT l (S n)) (SubT l (S m)) s t l ss) => EndedWithout2 n m s t ss |
class EndedWithout2' n m s t l ss | n m s t l -> ssSource
(ss ~ :> ss' s, l ~ S l', EndedWithout' m t l' ss') => EndedWithout2' Z (S m) s t l ss | |
(ss ~ :> ss' t, l ~ S l', EndedWithout' n s l' ss') => EndedWithout2' (S n) Z s t l ss | |
(ss ~ :> ss' End, l ~ S l', EndedWithout2' n m s t l' ss') => EndedWithout2' (S n) (S m) s t l ss |
class AppendEnd' n ss ss' | n ss -> ss', n ss' -> ssSource
ss ~ ss' => AppendEnd' Z ss ss' | |
(ss' ~ :> ss'' End, AppendEnd' n ss ss'') => AppendEnd' (S n) ss ss' |
Restrictions on session types for network communication
data NwService2 u u' Source
class NwSession u => NwReceiver u Source
(NwReceiver u1, NwReceiver u2) => NwReceiver (OfferN u1 u2) | |
(NwSession u, Message v) => NwReceiver (Recv v u) |
class (NwSession s, NwSession t) => NwDual s t | s -> t, t -> sSource
NwDual Close Close | |
(v ~ v', Nat v) => NwDual (Var v) (Var v') | |
(NwReceiver u1, NwSender u1', NwReceiver u2, NwSender u2', NwDual u1 u1', NwDual u2 u2') => NwDual (OfferN u1 u2) (SelectN u1' u2') | |
(NwSender u1, NwReceiver u1', NwSender u2, NwReceiver u2', NwDual u1 u1', NwDual u2 u2') => NwDual (SelectN u1 u2) (OfferN u1' u2') | |
(m ~ m', NwDual r r', Nat m) => NwDual (Rec m r) (Rec m' r') | |
(t ~ t', Message t, Message t', NwDual u' u) => NwDual (Recv t' u') (Send t u) | |
(t ~ t', Message t, Message t', NwDual u u') => NwDual (Send t u) (Recv t' u') |
class NwSession u => NwSendOnly u Source
NwSendOnly Close | |
Nat n => NwSendOnly (Var n) | |
(NwSendOnly u1, NwSendOnly u2, NwSender u1, NwSender u2) => NwSendOnly (SelectN u1 u2) | |
(NwSendOnly u, Nat m) => NwSendOnly (Rec m u) | |
(NwSendOnly u, Message v) => NwSendOnly (Send v u) |
class NwSession u => NwReceiveOnly u Source
NwReceiveOnly Close | |
Nat n => NwReceiveOnly (Var n) | |
(NwReceiveOnly u1, NwReceiveOnly u2, NwReceiver u1, NwReceiver u2) => NwReceiveOnly (OfferN u1 u2) | |
(NwReceiveOnly u, Nat m) => NwReceiveOnly (Rec m u) | |
(NwReceiveOnly u, Message v) => NwReceiveOnly (Recv v u) |
Recursive protocol
class RecFold m u s r | m u -> rSource
RecFold m Close s Close | |
RecFold m End s End | |
RecFold m (Var n) s (Var n) | |
(TypeEq m n b, RecFoldCont b m n a s r) => RecFold m (Rec n a) s r | |
(RecFold m u1 s u1', RecFold m u2 s u2') => RecFold m (OfferN u1 u2) s (OfferN u1' u2') | |
(RecFold m u1 s u1', RecFold m u2 s u2') => RecFold m (SelectN u1 u2) s (SelectN u1' u2') | |
(RecFold m u1 s u1', RecFold m u2 s u2') => RecFold m (Offer u1 u2) s (Offer u1' u2') | |
(RecFold m u1 s u1', RecFold m u2 s u2') => RecFold m (Select u1 u2) s (Select u1' u2') | |
(v ~ v', RecFold m u s u') => RecFold m (Catch v u) s (Catch v' u') | |
(v ~ v', RecFold m u s u') => RecFold m (Throw v u) s (Throw v' u') | |
(v ~ v', RecFold m u s u') => RecFold m (Recv v u) s (Recv v' u') | |
(v ~ v', RecFold m u s u') => RecFold m (Send v u) s (Send v' u') |
class RecFoldCont b m n a s r | b m n a -> rSource
a ~ s => RecFoldCont T m n a s (Var m) | |
(RecFold2 n s s', RecUnfold n s' xx s, RecFold m a s' r) => RecFoldCont F m n a s (Rec n r) |
class RecFold2 m u r | m u -> rSource
RecFold2 m Close Close | |
RecFold2 m End End | |
RecFold2 m (Var n) (Var n) | |
(TypeEq m n b, RecFoldCont2 b m n a r) => RecFold2 m (Rec n a) r | |
(RecFold2 m u1 u1', RecFold2 m u2 u2') => RecFold2 m (OfferN u1 u2) (OfferN u1' u2') | |
(RecFold2 m u1 u1', RecFold2 m u2 u2') => RecFold2 m (SelectN u1 u2) (SelectN u1' u2') | |
(RecFold2 m u1 u1', RecFold2 m u2 u2') => RecFold2 m (Offer u1 u2) (Offer u1' u2') | |
(RecFold2 m u1 u1', RecFold2 m u2 u2') => RecFold2 m (Select u1 u2) (Select u1' u2') | |
(v ~ v', RecFold2 m u u') => RecFold2 m (Catch v u) (Catch v' u') | |
(v ~ v', RecFold2 m u u') => RecFold2 m (Throw v u) (Throw v' u') | |
(v ~ v', RecFold2 m u u') => RecFold2 m (Recv v u) (Recv v' u') | |
(v ~ v', RecFold2 m u u') => RecFold2 m (Send v u) (Send v' u') |
class RecFoldCont2 b m n a r | b m n a -> rSource
RecFoldCont2 T m n a (Var m) | |
RecFold2 m a r => RecFoldCont2 F m n a (Rec n r) |
class RecUnfold m r s u | m r s -> uSource
RecUnfold m Close s Close | |
RecUnfold m End s End | |
(TypeEq m n b, RecUnfoldCont b m n s a) => RecUnfold m (Var n) s a | |
(RecUnfold m u1 s u1', RecUnfold m u2 s u2') => RecUnfold m (OfferN u1 u2) s (OfferN u1' u2') | |
(RecUnfold m u1 s u1', RecUnfold m u2 s u2') => RecUnfold m (SelectN u1 u2) s (SelectN u1' u2') | |
(RecUnfold m u1 s u1', RecUnfold m u2 s u2') => RecUnfold m (Offer u1 u2) s (Offer u1' u2') | |
(RecUnfold m u1 s u1', RecUnfold m u2 s u2') => RecUnfold m (Select u1 u2) s (Select u1' u2') | |
(v ~ v', RecUnfold m u s u') => RecUnfold m (Catch v u) s (Catch v' u') | |
(v ~ v', RecUnfold m u s u') => RecUnfold m (Throw v u) s (Throw v' u') | |
(v ~ v', RecUnfold m u s u') => RecUnfold m (Recv v u) s (Recv v' u') | |
(v ~ v', RecUnfold m u s u') => RecUnfold m (Send v u) s (Send v' u') | |
(RecFold2 n s s', RecUnfold m a s' a') => RecUnfold m (Rec n a) s (Rec n a') |
class RecUnfoldCont b m n s a | b m n s -> aSource
RecUnfoldCont F m n s (Var n) | |
RecUnfoldCont T m n s (Rec m s) |