| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Control.Effect.Sessions.Operations
- run :: Process [] a -> IO a
- liftIO :: IO a -> Process [] a
- print :: Show a => a -> Process [] ()
- putStrLn :: String -> Process ([] (Map Name Session)) ()
- send :: Chan c -> t -> Process `[c :-> (t :! End)]` ()
- recv :: Chan c -> Process `[c :-> (t :? End)]` t
- new :: Duality env c => ((Chan (Ch c), Chan (Op c)) -> Process env t) -> Process ((env :\ Op c) :\ Ch c) t
- par :: Balanced env (AllBal env') => Process env () -> Process env' () -> Process (Union env env') ()
- type family AllBal env :: [Map Name Session]
- rsend :: Chan c -> Chan d -> Process `[c :-> (Delg s :*! End), d :-> Bal s]` ()
- chSend :: Chan c -> Chan d -> Process `[c :-> (Delg s :! End), d :-> Bal s]` ()
- chRecv :: Chan c -> (Chan d -> Process env a) -> Process (Union `[c :-> (Delg (env :@ d) :? (env :@ c))]` (env :\ d)) a
- subL :: Process `[c :-> s]` a -> Process `[c :-> (s :+ t)]` a
- subR :: Process `[c :-> t]` a -> Process `[c :-> (s :+ t)]` a
- subEnd :: Chan c -> Process [] a -> Process `[c :-> End]` a
- affineFix :: ((a -> Process `[c :-> Star]` b) -> a -> Process `[c :-> h]` b) -> a -> Process `[c :-> ToFix h]` b
Documentation
run :: Process [] a -> IO a Source
A process can be run if it is closed (i.e., empty channel environment)
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 |
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