Control.Concurrent.FullSession

Contents

Type level construcs
- Type level numbers and booleans
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

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 Close Source

Close denotes a session that can do nothing but closing it.

Instances

NwReceiveOnly Close
NwSendOnly Close
NwSession Close
IsEndedST Close F
NwDual Close Close
Comp Close End Close
Comp End Close Close
Dual n Close Close
RecFold2 m Close Close
RecUnfold m Close s Close
RecFold m Close s Close
IsEnded (:> ss Close) 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 ([]).

Instances

SList Nil Z
IsEnded Nil T
Ended Z Nil
Par Nil Nil Nil

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.

data Service u Source

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

newService :: Dual Z u u' => IO (Service u)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

dualNw :: NwDual u u' => NwService u -> NwService u'Source

dualNw2 :: (NwDual u1 u1', NwDual u2 u2') => NwService2 u1 u2 -> NwService2 u1' u2'Source

mkNwService :: NwSession u => String -> Int -> u -> NwService uSource

mkNwService2 :: (NwSendOnly u, NwReceiveOnly u') => String -> Int -> u -> u' -> NwService2 u u'Source

Type class for messages

class Message mes whereSource

Methods

parseMessage :: String -> Maybe (mes, String)Source

showMessage :: mes -> String Source

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' ThreadId Source

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

Instances

IsEndedST Close F
IsEndedST End T
IsEndedST Bot F
IsEndedST (Var v) 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

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 NwService u Source

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

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

Instances

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

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