full-sessions-0.4.189: yet another implementation of session types which does not require annotationsSource codeContentsIndex
Control.Concurrent.FullSession.Types
Synopsis
data Cap e t
data End
data Send v u
data Recv v u
data Throw u' u
data Catch u' u
data Rec u
data Var n
data Bot
data Select u1 u2
data Offer u u'
Documentation
data Cap e t Source
capability -- from the implementation of Pucella and Tov ex. Cap Nil (Rec (Send Int (Var Z))) == Cap (Send Int (Var Z):|:Nil) (Send Int (Var Z)) -- (by enter operation) Cap (Send Int (Var Z):|:Nil) (Var Z) == Cap (Send Int (Var Z):|:Nil) (Send Int (Var Z)) -- (by zero operation)
show/hide Instances
Comp c (Cap Nil End) c
Comp (Cap Nil End) c c
(TCast v v', TCast e e', TCast e' Nil) => Comp (Cap e (Var v)) (Cap e' (Var v')) (Cap e'' Bot)
(Comp2 r r', TCast e e', TCast e' Nil) => Comp (Cap e (Rec r)) (Cap e' (Rec r')) (Cap e'' Bot)
(Comp2 u u', Comp2 v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Offer u v)) (Cap e' (Select u' v')) (Cap e'' Bot)
(Comp2 u u', Comp2 v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Select u v)) (Cap e' (Offer u' v')) (Cap e'' Bot)
(Comp2 u u', TCast v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Catch v u)) (Cap e' (Throw v' u')) (Cap e'' Bot)
(Comp2 u u', TCast v v', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Throw v u)) (Cap e' (Catch v' u')) (Cap e'' Bot)
(Comp2 u u', TCast t t', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Recv t' u')) (Cap e' (Send t u)) (Cap e'' Bot)
(Comp2 u u', TCast t t', TCast e e', TCast e' e'', TCast e' Nil) => Comp (Cap e (Send t u)) (Cap e' (Recv t' u')) (Cap e'' Bot)
Comp (Cap Nil End) (Cap Nil End) (Cap Nil End)
data End Source
no operation
show/hide Instances
data Send v u Source
send a value of type v then u
show/hide Instances
(Comp2 u u', TCast t t') => Comp2 (Recv t' u') (Send t u)
(Comp2 u u', TCast t t') => Comp2 (Send t u) (Recv t' u')
data Recv v u Source
receive a value of type v then u
show/hide Instances
(Comp2 u u', TCast t t') => Comp2 (Recv t' u') (Send t u)
(Comp2 u u', TCast t t') => Comp2 (Send t u) (Recv t' u')
data Throw u' u Source
send a channel of session type u' then u
show/hide Instances
(Comp2 u u', TCast v v') => Comp2 (Catch v u) (Throw v' u')
(Comp2 u u', TCast v v') => Comp2 (Throw v u) (Catch v' u')
data Catch u' u Source
receive a channel of session type u' then u
show/hide Instances
(Comp2 u u', TCast v v') => Comp2 (Catch v u) (Throw v' u')
(Comp2 u u', TCast v v') => Comp2 (Throw v u) (Catch v' u')
data Rec u Source
recursion binding
show/hide Instances
Comp2 r r' => Comp2 (Rec r) (Rec r')
data Var n Source
recursion variable
show/hide Instances
TCast v v' => Comp2 (Var v) (Var v')
data Bot Source
this channel is (or, will be) owned by maximum two processes
data Select u1 u2 Source
send a label i then ui (i in {1,2})
show/hide Instances
(Comp2 u u', Comp2 v v') => Comp2 (Offer u v) (Select u' v')
(Comp2 u u', Comp2 v v') => Comp2 (Select u v) (Offer u' v')
data Offer u u' Source
receive a label i then ui (i in {1,2})
show/hide Instances
(Comp2 u u', Comp2 v v') => Comp2 (Offer u v) (Select u' v')
(Comp2 u u', Comp2 v v') => Comp2 (Select u v) (Offer u' v')
Produced by Haddock version 2.4.2