full-sessions-0.4.181: yet another implementation of session types which does not require annotations Source code Contents Index

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) 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 Instances Comp2 End End

data Send v u Source

send a value of type v then u 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 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 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 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 Instances Comp2 r r' => Comp2 (Rec r) (Rec r')

data Var n Source

recursion variable 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}) 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}) 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