full-sessions-0.6.1: a monad for protocol-typed network programmingSource codeContentsIndex
Control.Concurrent.FullSession
Synopsis
class Nat n
data Z
data S n
data P n
data T
data F
class EqNat x y b | x y -> b
class Sub n n'
type family SubT n n' :: *
data ss :> s
data Nil
class Length ss l | ss -> l
class Pickup ss n s | ss n -> s
class PickupR ss n s | ss n -> s
class Update ss n t ss' | ss n t -> ss'
class UpdateR ss n t ss' | ss n t -> ss'
class IsEnded ss b | ss -> b
class (Length ss n, IsEnded ss T) => Ended n ss | n -> ss
class EndedWithout n s ss | n s -> ss
class EndedWithout' n s l ss | n s l -> ss
class EndedWithout2 n m s t ss | n s m t -> ss
class EndedWithout2' n m s t l ss | n m s t l -> ss
class AppendEnd ss ss'
class AppendEnd' n ss ss' | n ss -> ss', n ss' -> ss
close :: (Pickup ss n Close, Update ss n End ss', IsEnded ss F) => Channel t n -> Session t ss ss' ()
send :: (Pickup ss n (Send v a), Update ss n a ss', IsEnded ss F) => Channel t n -> v -> Session t ss ss' ()
recv :: (Pickup ss n (Recv v u), Update ss n u ss', IsEnded ss F) => Channel t n -> Session t ss ss' v
sendS :: (Pickup ss n1 (Throw c1 u1), Update ss n1 u1 ss', Pickup ss' n2 c1, Update ss' n2 End ss'', IsEnded ss F) => Channel t n1 -> Channel t n2 -> Session t ss ss'' ()
recvS :: (Pickup ss n1 (Catch c1 u1), Update ss n1 u1 ss', Length ss' l, IsEnded ss F) => Channel t n1 -> Session t ss (ss' :> c1) (Channel t l)
sel1 :: (Pickup ss n (Select s x), Update ss n s tt, IsEnded ss F) => Channel t n -> Session t ss tt ()
sel2 :: (Pickup ss n (Select x s), Update ss n s tt, IsEnded ss F) => Channel t n -> Session t ss tt ()
ifSelect :: (Pickup ss n (Select x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Bool -> Session t sx xx a -> Session t sy yy a -> Session t ss zz a
offer :: (Pickup ss n (Offer x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Session t sx xx a -> Session t sy yy a -> Session t ss zz a
class Par ss tt' tt | ss tt' -> tt, ss tt -> tt', tt tt' -> ss
class Par' t ss tt' tt | t ss tt' -> tt, t ss tt -> tt', t tt tt' -> ss
forkIOs :: (Length ss l, Length tt' l, Length tt l, Ended l' ss', IsEnded ss b, Par' b ss tt' tt) => Session t ss ss' () -> Session t tt tt' ThreadId
forkOSs :: (Length ss l, Length tt' l, Length tt l, Ended l' ss', IsEnded ss b, Par' b ss tt' tt) => Session t ss ss' () -> Session t tt tt' ThreadId
io :: IO a -> Session t ss ss a
io_ :: IO a -> Session t ss ss ()
new :: Length ss l => Session t ss (ss :> Bot) (Channel t l)
unwind :: (RecFold m u r r, RecUnfold m r r u, Pickup ss n (Rec m r), Update ss n u tt, IsEnded ss F) => Channel t n -> Session t ss tt ()
unwind0 :: (RecFold Z u r r, RecUnfold Z r r u, Pickup ss n (Rec Z r), Update ss n u tt, IsEnded ss F) => Channel t n -> Session t ss tt ()
unwind1 :: (RecFold (S Z) u r r, RecUnfold (S Z) r r u, Pickup ss n (Rec (S Z) r), Update ss n u tt, IsEnded ss F) => Channel t n -> Session t ss tt ()
unwind2 :: (RecFold (S (S Z)) u r r, RecUnfold (S (S Z)) r r u, Pickup ss n (Rec (S (S Z)) r), Update ss n u tt, IsEnded ss F) => Channel t n -> Session t ss tt ()
recur1 :: (EndedWithout n s ss, AppendEnd ss ss', Length ss' l, Ended l tt) => (Channel t n -> Session t ss tt ()) -> Channel t n -> Session t ss' tt ()
recur2 :: (EndedWithout2 n m s s' ss, AppendEnd ss ss', Length 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 ()
data Service u
newService :: Dual Z u u' => IO (Service u)
connect :: (Dual Z u u', Length ss l) => Service u -> Session t ss (ss :> u') (Channel t l)
connectRunS :: (Dual Z u u', Ended xs n) => Service u -> (forall t. Channel t Z -> Session t (Nil :> u') xs a) -> IO a
accept :: (Dual Z u u', Length ss l) => Service u -> Session t ss (ss :> u) (Channel t l)
acceptRunS :: (Dual Z u u', Ended xs n) => Service u -> (forall t. Channel t Z -> Session t (Nil :> u) xs a) -> IO a
data NwService u
mkNwService :: NwSession u => String -> Int -> u -> NwService u
connectNw :: (Length ss l, NwSession u) => NwService u -> Session t ss (ss :> u) (Channel t l)
data NwService2 u u'
mkNwService2 :: (NwSendOnly u, NwReceiveOnly u') => String -> Int -> u -> u' -> NwService2 u u'
connectNw2 :: (Length ss l, NwSendOnly u, NwReceiveOnly u') => NwService2 u u' -> Session t ss ((ss :> u) :> u') (Channel t l, Channel t (S l))
acceptOneNw2 :: (Length ss l, NwSendOnly u, NwReceiveOnly u') => NwService2 u u' -> Session t ss ((ss :> u) :> u') (Channel t l, Channel t (S l))
dualNw :: NwDual u u' => NwService u -> NwService u'
dualNw2 :: (NwDual u1 u1', NwDual u2 u2') => NwService2 u1 u2 -> NwService2 u1' u2'
class Message mes where
parseMessage :: String -> Maybe (mes, String)
showMessage :: mes -> String
class NwSession u => NwSender u
class NwSession u => NwReceiver u
class NwSession u
sel1N :: (Pickup ss n (SelectN s x), Update ss n s tt) => Channel t n -> Session t ss tt ()
sel2N :: (Pickup ss n (SelectN x s), Update ss n s tt) => Channel t n -> Session t ss tt ()
ifSelectN :: (Pickup ss n (SelectN x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Bool -> Session t sx xx a -> Session t sy yy a -> Session t ss zz a
offerN :: (NwReceiver x, NwReceiver y, Pickup ss n (OfferN x y), Update ss n x sx, Update ss n y sy, Diff xx yy zz, IsEnded ss F) => Channel t n -> Session t sx xx a -> Session t sy yy a -> Session t ss zz a
class (NwSession s, NwSession t) => NwDual s t | s -> t, t -> s
class NwSession u => NwSendOnly u
class NwSession u => NwReceiveOnly u
finallys :: Session t ss tt () -> IO () -> Session t ss tt ()
data Bot
data Send v u
data Recv v u
data Throw u' u
data Catch u' u
data Select u1 u2
data Offer u1 u2
data End
data Rec m r
data Var n
data Close
data SelectN u1 u2
data OfferN u1 u2
data Channel t n
class Diff xx yy zz | xx yy -> zz
class Diff' n xx yy zz | n xx yy -> zz
class TypeEq' () x y b => TypeEq x y b | x y -> b
class TypeEq' q x y b | q x y -> b
class TypeEq'' q x y b | q x y -> b
class Dual n s t | s -> t, t -> s
class Comp s t u | s u -> t, t u -> s, s t -> u
data Session t ss tt a
(>>>=) :: Session t ss tt a -> (a -> Session t tt uu b) -> Session t ss uu b
(>>>) :: Session t ss tt a -> Session t tt uu b -> Session t ss uu b
ireturn :: a -> Session t ss ss a
runS :: Ended n ss => forall a n. (forall t. Session t Nil ss a) -> IO a
typecheck1 :: Length ss l => (Channel t l -> Session t (ss :> s) ss' a) -> Session t (ss :> s) ss' a
typecheck2 :: Length ss l => (Channel t (S l) -> Channel t l -> Session t ((ss :> s1) :> s2) ss' a) -> Session t ((ss :> s1) :> s2) ss' a
class RecFold m u s r | m u -> r
class RecFoldCont b m n a s r | b m n a -> r
class RecFold2 m u r | m u -> r
class RecFoldCont2 b m n a r | b m n a -> r
class RecUnfold m r s u | m r s -> u
class RecUnfoldCont b m n s a | b m n s -> a
Documentation
class Nat n Source
show/hide Instances
Nat Z
Nat n => Nat (S n)
data Z Source
show/hide Instances
Show Z
Nat Z
Length 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
show/hide Instances
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
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)
Length ss l => Length (:> ss s) (S l)
UpdateR ss n t ss' => UpdateR (:> ss s) (S n) t (:> ss' s)
data P n Source
show/hide Instances
(yy ~ :> yy' End, zz ~ :> zz' End, Diff' n xx yy' zz') => Diff' (P n) xx yy zz
data T Source
show/hide Instances
IsEnded Nil T
EqNat Z Z T
(tt' ~ tt, Length 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
show/hide Instances
(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
EqNat (S n) Z 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
class EqNat x y b | x y -> bSource
show/hide 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
show/hide Instances
Sub n n
Sub n (S (S n))
Sub n (S n)
Sub (S n) n
Sub (S (S n)) n
type family SubT n n' :: *Source
data ss :> s Source
show/hide Instances
Ended n ss => Ended (S n) (:> ss End)
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
IsEnded ss b => IsEnded (:> ss End) b
UpdateR (:> ss s) Z t (:> ss t)
Length ss l => Length (:> 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
show/hide Instances
class Length ss l | ss -> lSource
show/hide Instances
Length Nil Z
Length ss l => Length (:> ss s) (S l)
class Pickup ss n s | ss n -> sSource
show/hide Instances
(Length 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
show/hide 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
show/hide Instances
(Length 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
show/hide Instances
UpdateR (:> ss s) Z t (:> ss t)
UpdateR ss n t ss' => UpdateR (:> ss s) (S n) t (:> ss' s)
class IsEnded ss b | ss -> bSource
T if the all elements of ss are End
show/hide Instances
IsEnded Nil T
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
IsEnded ss b => IsEnded (:> ss End) b
class (Length ss n, IsEnded ss T) => Ended n ss | n -> ssSource
show/hide Instances
Ended Z Nil
Ended n ss => Ended (S n) (:> ss End)
class EndedWithout n s ss | n s -> ssSource
show/hide Instances
(Length ss l, EndedWithout' (SubT l (S n)) s l ss) => EndedWithout n s ss
class EndedWithout' n s l ss | n s l -> ssSource
show/hide 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
show/hide Instances
(Length 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
show/hide 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
show/hide Instances
(Length ss l, Length 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
show/hide Instances
ss ~ ss' => AppendEnd' Z ss ss'
(ss' ~ :> ss'' End, AppendEnd' n ss ss'') => AppendEnd' (S n) ss ss'
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', Length 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
class Par ss tt' tt | ss tt' -> tt, ss tt -> tt', tt tt' -> ssSource
pointwise extension of Comp -- FIXME: method
show/hide 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
show/hide Instances
(IsEnded ss F, Par ss tt' tt) => Par' F ss tt' tt
(tt' ~ tt, Length tt n, Ended n ss, IsEnded ss T) => Par' T ss tt' tt
forkIOs :: (Length ss l, Length tt' l, Length tt l, Ended l' ss', IsEnded ss b, Par' b ss tt' tt) => Session t ss ss' () -> Session t tt tt' ThreadIdSource
forkOSs :: (Length ss l, Length tt' l, Length 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
io :: IO a -> Session t ss ss aSource
io_ :: IO a -> Session t ss ss ()Source
new :: Length ss l => Session t ss (ss :> Bot) (Channel t l)Source
unwind :: (RecFold m u r r, RecUnfold m r r u, Pickup ss n (Rec m r), Update ss n u tt, IsEnded ss F) => Channel t n -> Session t ss tt ()Source
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', Length 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', Length 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
data Service u Source
newService :: Dual Z u u' => IO (Service u)Source
connect :: (Dual Z u u', Length 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', Length 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
data NwService u Source
mkNwService :: NwSession u => String -> Int -> u -> NwService uSource
connectNw :: (Length ss l, NwSession u) => NwService u -> Session t ss (ss :> u) (Channel t l)Source
data NwService2 u u' Source
mkNwService2 :: (NwSendOnly u, NwReceiveOnly u') => String -> Int -> u -> u' -> NwService2 u u'Source
connectNw2 :: (Length ss l, NwSendOnly u, NwReceiveOnly u') => NwService2 u u' -> Session t ss ((ss :> u) :> u') (Channel t l, Channel t (S l))Source
acceptOneNw2 :: (Length ss l, NwSendOnly u, NwReceiveOnly u') => NwService2 u u' -> Session t ss ((ss :> u) :> u') (Channel t l, Channel t (S l))Source
dualNw :: NwDual u u' => NwService u -> NwService u'Source
dualNw2 :: (NwDual u1 u1', NwDual u2 u2') => NwService2 u1 u2 -> NwService2 u1' u2'Source
class Message mes whereSource
Methods
parseMessage :: String -> Maybe (mes, String)Source
showMessage :: mes -> StringSource
class NwSession u => NwSender u Source
show/hide Instances
(NwSender u1, NwSender u2) => NwSender (SelectN u1 u2)
(NwSession u, Message v) => NwSender (Send v u)
class NwSession u => NwReceiver u Source
show/hide Instances
class NwSession u Source
show/hide Instances
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
class (NwSession s, NwSession t) => NwDual s t | s -> t, t -> sSource
show/hide 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') => 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
show/hide Instances
class NwSession u => NwReceiveOnly u Source
show/hide Instances
finallys :: Session t ss tt () -> IO () -> Session t ss tt ()Source
data Bot Source
show/hide Instances
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 Send v u Source
show/hide 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)
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
show/hide 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)
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
show/hide 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')
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
show/hide 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')
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
show/hide 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')
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
show/hide 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')
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
show/hide Instances
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 Rec m r Source
show/hide 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 => NwReceiveOnly (Rec m u)
NwSendOnly u => NwSendOnly (Rec m u)
NwSession u => NwSession (Rec m u)
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') => 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
show/hide 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)
(v ~ v', Nat v) => NwDual (Var v) (Var v')
IsEnded (:> ss (Var v)) F
data Close Source
show/hide Instances
data SelectN u1 u2 Source
show/hide 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)
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
show/hide 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)
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')
data Channel t n Source
class Diff xx yy zz | xx yy -> zzSource
show/hide Instances
(Length xx lx, Length 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
show/hide 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
class TypeEq' () x y b => TypeEq x y b | x y -> bSource
show/hide Instances
TypeEq' () x y b => TypeEq x y b
class TypeEq' q x y b | q x y -> bSource
show/hide 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
show/hide Instances
EqNat x y b => TypeEq'' () x y b
class Dual n s t | s -> t, t -> sSource
duality
show/hide 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')
class Comp s t u | s u -> t, t u -> s, s t -> uSource
sesion type algebra
show/hide 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
data Session t ss tt a Source
(>>>=) :: Session t ss tt a -> (a -> Session t tt uu b) -> Session t ss uu bSource
(>>>) :: Session t ss tt a -> Session t tt uu b -> Session t ss uu bSource
ireturn :: a -> Session t ss ss aSource
runS :: Ended n ss => forall a n. (forall t. Session t Nil ss a) -> IO aSource
typecheck1 :: Length ss l => (Channel t l -> Session t (ss :> s) ss' a) -> Session t (ss :> s) ss' aSource
typecheck2 :: Length ss l => (Channel t (S l) -> Channel t l -> Session t ((ss :> s1) :> s2) ss' a) -> Session t ((ss :> s1) :> s2) ss' aSource
class RecFold m u s r | m u -> rSource
show/hide 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
show/hide 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
show/hide 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
show/hide 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
show/hide 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
show/hide Instances
RecUnfoldCont F m n s (Var n)
RecUnfoldCont T m n s (Rec m s)
Produced by Haddock version 2.6.0