full-sessions-0.6.2.1: a monad for protocol-typed network programming

Control.Concurrent.FullSession

Contents

Description

Pi-calculus style communication and concurrency primitives which come with session types.

Synopsis

Type level construcs

Type level numbers and booleans

data Z Source

Type level zero.

Instances

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) 

data S n Source

Type level successor. S n denotes (n+1).

Instances

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) 

data P n Source

Type level predecessor (only for internal use). P n denotes (n-1).

Instances

(yy ~ :> yy' End, zz ~ :> zz' End, Diff' n xx yy' zz') => Diff' (P n) xx yy zz 

class Nat n Source

The class which covers type-level natural numbers.

Instances

Nat Z 
Nat n => Nat (S n) 

data T Source

Type level True.

Instances

IsEndedST End T 
IsEnded Nil T 
EqNat Z Z T 
And T T T 
(tt' ~ tt, SList tt n, Ended n ss, IsEnded ss T) => Par' T ss tt' tt 
a ~ s => RecFoldCont T m n a s (Var m) 
RecFoldCont2 T m n a (Var m) 
RecUnfoldCont T m n s (Rec m s) 

data F Source

Type level False.

Instances

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)

data Send v u Source

Send v u denotes a protocol to emit a value of type v followed by a behavior of type u. Use of send on a channel changes its session type from Send v u into u.

Instances

(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 

data Recv v u Source

Recv v u denotes a protocol of receiving a value of type v followed by a behavior of type u. Use of recv on a channel changes its session type from Recv v u into u.

Instances

(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 

data Throw u' u Source

Throw u1 u2 denotes a behavior to output of a channel with session type u1 followed by a behavior of type u2. Use of sendS on a channel changes its session type from Throw u1 u2 into u2.

Instances

(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 

data Catch u' u Source

Catch u1 u2 is the input of a channel with session type u1 followed by a behavior of type u2. Use of recvS on a channel changes its session type from Catch u1 u2 into u2.

Instances

(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 

data Select u1 u2 Source

Select u1 u2 denotes to be either behavior of type u1 or type u2 after emitting a corresponding label 1 or 2. Use of sel1 or sel2 on a channel changes its session type from Select u1 u2 into u1 or u2, respectively.

Instances

(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 

data Offer u1 u2 Source

Offer u1 u2 denotes a behavior like either u1 or u2 according to the incoming label.

Instances

(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 

data End Source

End denotes a terminated session. Further communication along a channel with type End cannot take place.

Instances

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'') 

data Bot Source

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.

Instances

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 

data Rec m r Source

Rec m r denotes recursive session, where m represents the binder of recursion variable. a type-level natural numer (like S Z). nesting level of Rec, and r is the body of the recursion which may contain Var m.

Instances

(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 

data Var n Source

Recursion variable.

Instances

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 

data SelectN u1 u2 Source

Instances

(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') 

data OfferN u1 u2 Source

Instances

(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

data ss :> s Source

Type-level snoc (reversed version of cons (:)). ss :> s denotes a list ss with s on its end. (FIXME:English)

Instances

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) 

data Nil Source

Type-level empty list ([]).

The Session monad

data Session t ss tt a Source

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.

(>>>) :: Session t ss tt a -> Session t tt uu b -> Session t ss uu bSource

ireturn :: a -> Session t ss ss aSource

Unit (a.k.a return) 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 -> io_ (runS ( ... send c ...) ) is rejected by the Haskell typechecker with error Inferred type is less polymorphic than expected.

Communication and concurrency primitives

Channel types

data Channel t n Source

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

new :: SList ss l => Session t ss (ss :> Bot) (Channel t l)Source

connect :: (Dual Z u u', SList ss l) => Service u -> Session t ss (ss :> u') (Channel t l)Source

connectRunS :: (Dual Z u u', Ended xs n) => Service u -> (forall t. Channel t Z -> Session t (Nil :> u') xs a) -> IO aSource

accept :: (Dual Z u u', SList ss l) => Service u -> Session t ss (ss :> u) (Channel t l)Source

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

connectNw :: (SList ss l, NwSession u) => NwService u -> Session t ss (ss :> u) (Channel t l)Source

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'

sel2N :: (Pickup ss n (SelectN x s), Update ss n s tt) => Channel t n -> Session t ss tt ()Source

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

class Message mes whereSource

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

io :: IO a -> Session t ss ss aSource

io_ :: IO a -> Session t ss ss ()Source

Exception handling

finallys :: Session t ss tt () -> IO () -> Session t ss tt ()Source

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

channeltype1 :: Pickup ss' Z s' => (Channel t Z -> Session t (Nil :> s) ss' a) -> (s, s')Source

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 ~ T if x == y. Otherwise b ~ F.

Instances

EqNat Z Z T 
EqNat Z (S n) F 
EqNat (S n) Z F 
EqNat n n' b => EqNat (S n) (S n') b 

class Sub n n' Source

Computes subtraction of n by n' (FIXME:OK?)

Instances

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 

type family SubT n n' :: *Source

Computes subtraction of n by n'

class And b1 b2 b | b1 b2 -> bSource

type-level &&

Instances

And b F F 
And F b F 
And T T T 

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.

Instances

SList Nil Z 
SList ss l => SList (:> ss s) (S l) 

class Pickup ss n s | ss n -> sSource

Pickup ss n s denotes that the n-th element of the list ss is s. This type class plays an important role in session-type inference.

Formally, Pickup ss n s if s = 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 SubT (S n) (S n) ~ Z, it will be reduced to

     PickupR (ss:>Bot:>Recv Char End) Z s

and then s is unified with Recv Char End.

Instances

(SList ss l, Sub l (S n), PickupR ss (SubT l (S n)) s) => Pickup ss n s 

class PickupR ss n s | ss n -> sSource

The reversed version of Pickup which accesses lists in reversed order (counts from right to left). I.e., PickupR (End :> Bot :> Send Int End) Z (Send Int End) is an instance of PickupR.

Instances

ss ~ :> ss' t => PickupR ss Z t 
(ss ~ :> ss' s', PickupR ss' n t) => PickupR ss (S n) t 

class Update ss n t ss' | ss n t -> ss'Source

Update ss n t ss' denotes that ss' is same as ss except that its n-th element is t. Formally, Update ss n t ss' if 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, Update (End :> Bot :> Send Int End) Z End (End :> Bot :> End)) is an instance of Update.

Note that the list counts from left to right, as in the case of Pickup.

Instances

(SList ss l, Sub l (S n), UpdateR ss (SubT l (S n)) t ss') => Update ss n t ss' 

class UpdateR ss n t ss' | ss n t -> ss'Source

The reversed version of Update.

Instances

UpdateR (:> ss s) Z t (:> ss t) 
UpdateR ss n t ss' => UpdateR (:> ss s) (S n) t (:> ss' s) 

Type classes for ended type environments (1)

class (SList ss n, IsEnded ss T) => Ended n ss | n -> ssSource

Ended n ss denotes that the session-type environment ss (the length of it is n) is Ended. The all elements in an Ended type environments are End.

Instances

Ended Z Nil 
Ended n ss => Ended (S n) (:> ss End) 

class IsEnded ss b | ss -> bSource

IsEnded ss b denotes that b ~ T if ss is Ended, otherwise b ~ F. In other words, b ~ T if the all elements of ss are End

Instances

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 

class IsEndedST s b | s -> bSource

Duality of session types

class Dual n s t | s -> t, t -> sSource

duality

Instances

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

Instances

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

Instances

Par Nil Nil Nil 
(Comp s t' t, IsEnded ss b, Par' b ss tt' tt) => Par (:> ss s) (:> tt' t') (:> tt t) 

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

Instances

(IsEnded ss F, Par ss tt' tt) => Par' F ss tt' tt 
(tt' ~ tt, SList tt n, Ended n ss, IsEnded ss T) => Par' T ss tt' tt 

Type classes for ended type environments (2)

class EndedWithout n s ss | n s -> ssSource

Instances

(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

Instances

(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

Instances

(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

Instances

(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 ss ss' Source

Instances

(SList ss l, SList ss' l', Sub l' l, AppendEnd' (SubT l' l) ss ss') => AppendEnd ss ss' 

class AppendEnd' n ss ss' | n ss -> ss', n ss' -> ssSource

Instances

ss ~ ss' => AppendEnd' Z ss ss' 
(ss' ~ :> ss'' End, AppendEnd' n ss ss'') => AppendEnd' (S n) ss ss' 

class Diff xx yy zz | xx yy -> zzSource

Instances

(SList xx lx, SList yy ly, Diff' (SubT lx ly) xx yy zz, Sub lx ly) => Diff xx yy zz 

class Diff' n xx yy zz | n xx yy -> zzSource

Instances

(xx ~ zz, yy ~ zz) => Diff' Z xx yy zz 
(yy ~ :> yy' End, zz ~ :> zz' End, Diff' n xx yy' zz') => Diff' (P n) xx yy zz 
(xx ~ :> xx' End, zz ~ :> zz' End, Diff' n xx' yy zz') => Diff' (S n) xx yy zz 

Restrictions on session types for network communication

data NwService2 u u' Source

class NwSession u => NwSender u Source

Instances

(NwSender u1, NwSender u2) => NwSender (SelectN u1 u2) 
(NwSession u, Message v) => NwSender (Send v u) 

class NwSession u => NwReceiver u Source

Instances

(NwReceiver u1, NwReceiver u2) => NwReceiver (OfferN u1 u2) 
(NwSession u, Message v) => NwReceiver (Recv v u) 

class NwSession u Source

Instances

NwSession Close 
Nat n => NwSession (Var n) 
(NwReceiver u1, NwReceiver u2) => NwSession (OfferN u1 u2) 
(NwSender u1, NwSender u2) => NwSession (SelectN u1 u2) 
(NwSession u, Nat m) => NwSession (Rec m u) 
(Message v, NwSession u) => NwSession (Recv v u) 
(Message v, NwSession u) => NwSession (Send v u) 

class (NwSession s, NwSession t) => NwDual s t | s -> t, t -> sSource

Instances

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

Instances

Recursive protocol

class RecFold m u s r | m u -> rSource

Instances

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

Instances

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

Instances

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

Instances

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

Instances

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

Instances

RecUnfoldCont F m n s (Var n) 
RecUnfoldCont T m n s (Rec m s) 

Type equality

class TypeEq' () x y b => TypeEq x y b | x y -> bSource

Instances

TypeEq' () x y b => TypeEq x y b 

class TypeEq' q x y b | q x y -> bSource

Instances

b ~ T => TypeEq' () x x b 
TypeEq'' q x y b => TypeEq' q x y b 

class TypeEq'' q x y b | q x y -> bSource

Instances

EqNat x y b => TypeEq'' () x y b