Control.Concurrent.FullSession (original) (raw)

Type level construcs

Type level numbers and booleans

data S n Source

Type level successor. `[S](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t:P)` n denotes (n-1).

class Nat n Source

The class which covers type-level natural numbers.

Session types (protocol types)

data Send v u Source

`[Send](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t:Throw)` u1 u2 into u2.

data Catch u' u Source

`[Catch](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t:Catch)` u1 u2 into u2.

data Select u1 u2 Source

`[Select](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t:Select)` u1 u2 into u1 or u2, respectively.

data Offer u1 u2 Source

`[Offer](Control-Concurrent-FullSession.html#t:Offer)` u1 u2 denotes a behavior like either u1 or u2 according to the incoming label.

data End Source

[End](Control-Concurrent-FullSession.html#t:End) denotes a terminated session. Further communication along a channel with type [End](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t:Bot).

data Rec m r Source

`[Rec](Control-Concurrent-FullSession.html#t:Rec)` m r denotes recursive session, where m represents the binder of recursion variable. a type-level natural numer (like `[S](Control-Concurrent-FullSession.html#t:S)` `[Z](Control-Concurrent-FullSession.html#t:Z)`). nesting level of `[Rec](Control-Concurrent-FullSession.html#t:Rec)`, andr is the body of the recursion which may contain `[Var](Control-Concurrent-FullSession.html#t: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 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)

The Session monad

data Session t ss tt a Source

The Session monad. ss and tt denotes the usage of channels.

t denotes a type-tag, which prevents abuse of use of channels. For detail, see [runS](Control-Concurrent-FullSession.html#v:runS).

runS :: Ended n ss => forall a n. (forall t. Session t Nil ss a) -> IO aSource

[runS](Control-Concurrent-FullSession.html#v:runS) runs the [Session](Control-Concurrent-FullSession.html#t:Session). The pretype (see [Session](Control-Concurrent-FullSession.html#t:Session)) must be [Nil](Control-Concurrent-FullSession.html#t:Nil). The posttype must be [Ended](Control-Concurrent-FullSession.html#t:Ended), i.e. all channels must be [End](Control-Concurrent-FullSession.html#t: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 typeSession 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

Network communication

Primitives

Type class for messages

Thread creation

Interfacing with the IO monad

Exception handling

Recursive protocol support

Utility functions for type inferene

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](Control-Concurrent-FullSession.html#t:T)` if x == y. Otherwise b ~ F.

class Sub n n' Source

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

type family SubT n n' :: *Source

Computes subtraction of n by 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

`[Pickup](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t:SList)` ss (S n), `[Pickup](Control-Concurrent-FullSession.html#t:Pickup)` (ss:>Bot:>Recv Char End) n s

is expanded into

 `[SList](Control-Concurrent-FullSession.html#t:SList)` ss (S n), `[PickupR](Control-Concurrent-FullSession.html#t:PickupR)` (ss:>Bot:>Recv Char End) (`[SubT](Control-Concurrent-FullSession.html#t:SubT)` (S n) (S n)) s, `[Sub](Control-Concurrent-FullSession.html#t:Sub)` (S n) (S n)

since `[SubT](Control-Concurrent-FullSession.html#t:SubT)` (`[S](Control-Concurrent-FullSession.html#t:S)` n) (`[S](Control-Concurrent-FullSession.html#t:S)` n) ~ Z, it will be reduced to 

 `[PickupR](Control-Concurrent-FullSession.html#t:PickupR)` (ss:>Bot:>Recv Char End) Z s

and then s is unified with Recv Char End.

class PickupR ss n s | ss n -> sSource

The reversed version of [Pickup](Control-Concurrent-FullSession.html#t:Pickup) which accesses lists in reversed order (counts from right to left). I.e., `[PickupR](Control-Concurrent-FullSession.html#t:PickupR)` (End :> Bot :> Send Int End) Z (Send Int End) is an instance of [PickupR](Control-Concurrent-FullSession.html#t:PickupR).

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

`[Update](Control-Concurrent-FullSession.html#t:Update)` ss n t ss' denotes that ss' is same as ss except that its n-th element is t. Formally, `[Update](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t: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.

Type classes for ended type environments (1)

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

`[Ended](Control-Concurrent-FullSession.html#t: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](Control-Concurrent-FullSession.html#t:End)`.

class IsEnded ss b | ss -> bSource

`[IsEnded](Control-Concurrent-FullSession.html#t: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

Duality of session types

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](Control-Concurrent-FullSession.html#t: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)

Restrictions on session types for network communication

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

Recursive protocol

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

Type equality