effect-sessions-1.0: Sessions and session types for Concurrent Haskell

Safe HaskellNone
LanguageHaskell98

Control.Effect.Sessions.Operations

Synopsis

Documentation

run :: Process [] a -> IO a Source

A process can be run if it is closed (i.e., empty channel environment)

liftIO :: IO a -> Process [] a Source

Lift IO computations to a process

print :: Show a => a -> Process [] () Source

Print to stdout in a process

putStrLn :: String -> Process ([] (Map Name Session)) () Source

putStrLn in a process

send :: Chan c -> t -> Process `[c :-> (t :! End)]` () Source

Send a primitive-typed value

recv :: Chan c -> Process `[c :-> (t :? End)]` t Source

Receive a primitive-typed value

new :: Duality env c => ((Chan (Ch c), Chan (Op c)) -> Process env t) -> Process ((env :\ Op c) :\ Ch c) t Source

Create a new channel and pass its two endpoints to the supplied continuation (the first parameter). This channel is thus only in scope for this continuation

par :: Balanced env (AllBal env') => Process env () -> Process env' () -> Process (Union env env') () Source

Parallel compose two processes, if they contain disjoint (or balanced) sessions

type family AllBal env :: [Map Name Session] Source

Turn all session types into 'balancing checked' session types |

Equations

AllBal [] = [] 
AllBal ((c :-> s) : env) = (c :-> Bal s) : AllBal env 

rsend :: Chan c -> Chan d -> Process `[c :-> (Delg s :*! End), d :-> Bal s]` () Source

Output a channel (dual to a replicated input)

chSend :: Chan c -> Chan d -> Process `[c :-> (Delg s :! End), d :-> Bal s]` () Source

Send a channel d over channel c

chRecv :: Chan c -> (Chan d -> Process env a) -> Process (Union `[c :-> (Delg (env :@ d) :? (env :@ c))]` (env :\ d)) a Source

Receive a channel over a channel c, bind to the name d

subL :: Process `[c :-> s]` a -> Process `[c :-> (s :+ t)]` a Source

Explicit subeffecting introduction of :+ with the current session behaviour on the left

subR :: Process `[c :-> t]` a -> Process `[c :-> (s :+ t)]` a Source

Explicit subeffecting introduction of :+ with the current session behaviour on the right

subEnd :: Chan c -> Process [] a -> Process `[c :-> End]` a Source

Explicit subeffecting introduction of a terminated session for channel c

affineFix :: ((a -> Process `[c :-> Star]` b) -> a -> Process `[c :-> h]` b) -> a -> Process `[c :-> ToFix h]` b Source

Recursion combinator for recursive functions which have an affine fixed-point equation on their effects. For example, if 'h ~ (Seq h a) :+ b' then 'ToFix h = Fix a b'