Categorical Message Passing Language (CaMPL) for programmers
arXiv:2605.09491v1 [cs.PL] 10 May 2026
Daniel Kiyoshi Hashimoto‗
Alexanna Little Berg†
Priyaa Varshinee Srinivasan‡
Abstract Categorical Message Passing Language (CaMPL) is a functional-style concurrent programming language whose semantics is in category theory, more specifically, linear actegories. Its core programming feature is message passing along typed communication channels between concurrent processes. CaMPL also supports controlled non-determinism via ’races’ which allow processes to adapt dynamically while they are running, higher-order processes which pass other processes as messages, and custom channel datatypes called protocols and coprotocols which allow one to define infinite channel types or implement session types. The type system of CaMPL arises from a Curry-Howard-Lambek-like correspondence for concurrent programming, established by Cockett and Pastro in their paper titled “The logic of message passing”. This type system ensures that a formal CaMPL program, i.e., one which does not allow general recursion, will never become deadlocked or livelocked. In this article, we explore the type system of CaMPL, custom channel types, and controlled non-determinism using code examples after briefly introducing its mathematical underpinnings.
1
Introduction
Categorical Message Passing Language (CaMPL) is a functional-style concurrent programming language that uses message-passing concurrency. It implements a type system based on linear logic that was described in Cockett and Pastro’s paper “The logic of message passing” [CP09]. The primary result of their paper was defining and proving a concurrent analogue of the functional programming Curry-Howard-Lambek correspondence or proof-as-programs principle [How80; Lam69; Lam72]. They designed a two-tiered logic consisting of a sequential part, called the message logic, that interacts with a concurrent part, called the message-passing logic. The categorical semantics of the message-passing logic is given by a linear actegory. A linear actegory minimally consists of a monoidal category acting covariantly and contravariantly on a linearly distributive category, satisfying certain coherences [CP09; CS97]. The concurrent type system provided by linear actegories ensures that processes can never be connected in a cycle. That is, at any instance in run-time, the topology of a program is guaranteed to be a finite acyclic graph consisting of processes, which are nodes, and channels, which are edges. The benefit of this property is that problems caused by cycles, such as deadlocks and livelocks, do ‗ Universidade Federal do Rio de Janeiro, Brazil. † University of Calgary, Canada. ‡ Tallinn University of Technology, Estonia. This work was co-funded by the European Union and Estonian Research
Council through the Mobilitas 3.0 (MOB3JD1227).
1
not occur [Lyb18]. However, similar to proving termination in the sequential case, livelock freedom is only guaranteed if we disallow general recursion. Deadlock freedom is still guaranteed. The first implementation of the CaMPL compiler was written by Kumar as described in [Kum18]. This version implemented sequential and concurrent type systems. It added features to define custom concurrent data types called protocols and coprotocols. The categorical semantics for protocols and coprotocols were given by Yeasin in [Yea12]. This compiler performed both a type inference and type checking. The second implementation of the compiler was written by Pon as described in [Pon21; Pon22]. This version re-implemented the existing features and added controlled non-determinism in the form of “races.” Changes to the categorical semantics to include non-determinism were outlined by Little in [Lit22; Lit23]. The most recent feature added to the compiler was higher-order message passing which allows processes to send messages that contain encoded processes which can be decoded and invoked when they are received. The implementation of this feature and the changes to the categorical semantics were written by Norouzbeygi in [Nor25]. The current implementation of CaMPL is available at https://campl-ucalgary.github.io/. In this article, we illustrate CaMPL’s concurrent type system and the above features through a series of code examples. We have also summarized these features with the corresponding channel types and process commands in Table 1 in Appendix A. We use this style whenever we introduce CaMPL terminology.
2
A brief overview of CaMPL
As is tradition, we will introduce CaMPL with a “Hello World!” example program, shown in Example 1. We demonstrate a process named helloworld printing "Hello World!" by sending the string as a message on a channel named console. The console channel has type Console which is a special channel type built-in to the compiler to connect any CaMPL program to the terminal from which it is run. Example 1: Hello World! 1 2 3 4 5 6
proc helloworld :: | Console => = | console => -> do hput ConsolePut on console put " Hello World !" on console hput ConsoleClose on console halt console
-- sends message to the console -- closes console channel and halts
The helloworld process can be invoked by calling it in the main process, run, and giving it the console channel as follows: 7 8
proc run = | console => -> helloworld ( | console => )
-- creates helloworld process
In Example 2, we will demonstrate communication between two user-defined processes: client and server. The client will send a string to server, and server will receive it and echo it back. The main process will create the client and server processes, and it will use a process command called plug to connect them by a channel named ch. 2
Example 2: Server echos Client’s message 1 2 3 4
proc run = | => -> plug -- connects processes by shared channel ch client ( | => ch ) -- creates client process server ( | ch => ) -- creates server process
The CaMPL compiler will infer the type of ch using the process’ definitions. We will discuss channel types in Section 4.2. The client process has an output polarity channel ch which connects it to the server. We discuss polarity in Section 4.1. Client sends its message with put, and it receives the server’s echo with get. Then, it uses halt to close the channel with the server and halt. We can define client as follows: 1 2 3 4 5 6
proc client = | => ch -> on ch do put " Hello Server !" -- sends message to the server get echo -- receives server ’s echo halt
The server process has an input polarity channel ch which connects it to the client. It listens to the client and receives the client’s message with get, echos the message back with put, and finally closes the channel and halts with halt. We can define server as follows: 1 2 3 4 5 6
proc server = | ch => -> on ch do get msg put msg halt
-- receives client ’s message -- sends message back
These are simple programs that exemplify how CaMPL programs are written. In fact, the lines of the code in the second program are out of order as the run process should be the final process defined in a program. Furthermore, the runnable program obtained by reordering the lines still would not produce any observable effects since none of the processes are connected to the outside world. A reader should be left with open questions such as “what was the type of channel ch?” and “what else can this language do?” We hope that these questions motivate the reader to continue on to the more complicated examples in the following sections.
3
Processes
Processes are the main actors of a CaMPL program. A process is specified by the keyword proc followed by a process name, an optional type signature, and lists of its variables and channels. In Example 1, the type signature of process helloworld was “ :: | Console =>” which indicates that it has access to one channel of type Console. This channel is given the name console as indicated by “ = | console =>” on the next line. We will discuss type signatures in Section 4.2. A CaMPL program must have a process with the name run in which the execution of the program begins. This process is the main process and the only process which can create service 3
channels, such as the Console, for communication with the outside world. Consider the process broadcast shown in Example 3. Example 3: Process that broadcasts a message from a single source 1 2 3 4 5 6 7 8 9
proc broadcast = confirmation_msg | source , dest1 => dest2 -> do get msg on source -- receive message from source put msg on dest1 -- send message to other processes put msg on dest2 put confirmation_msg on source -- send confirmation message to source close source -- close all channels and halt close dest1 halt dest2 -- the last channel is closed with the halt command
Observe that line 2 consists of three comma-seperated lists: 1) variables, e.g. confirmation_msg, 2) input polarity channels, e.g. source, dest1, and 3) output polarity channels, e.g. dest2. Variables are instances of sequential types and channels are instances of concurrent types. The channels left of => are input polarity channels. The channels right of => are output polarity channels. Lines 3 - 9 constitute the process body. The channels listed in line 2 are “in scope” of the process body which means that the process can perform operations, called process commands, on these channels. The process body may be a single process command, as shown in the run processes in Examples 1 and 2, or a do block of process commands, as shown in Example 3. Process commands performed on the same channel can be grouped together with “on ch do” as in Example 2 on line 3 of client. This allows one to omit a repetitive “on ch” after each command.
4
Channels
A process uses process commands on a channel to interact with the process plugged into the other end. Two processes are connected by (at most) one typed channel that they use with opposite polarities. The type of a channel defines the interaction that the processes will have over it, and its polarities define each process’s role in the interaction. Thus, the process commands that a process can use on a channel depend on both type and polarity.
4.1
Channel polarities
Recall from Section 3 that processes are defined with two lists of the channels in its scope: input polarity channels and output polarity channels. A channel’s polarity refers to which end of the channel the process uses. In Example 2, the client and the server are connected by a channel ch. The client uses ch with output polarity (the left end) and server uses ch with input polarity (the right end). In the first step of the interaction, a message travels from the left to the right. The client uses put on its output polarity channel ch to send a message. Complementary to put, server uses get on its input polarity channel ch to receive the message. In the second step, the message travels in the opposite direction, so the type of ch is inferred differently compared to the previous step.
4
Channel polarities allow one to define unambiguous interactions between processes. Without polarities to distinguish their roles, both client and server could use a get command at the same time. Then, they would both wait for a message to be sent by the other, thereby causing a deadlock. This scenario is illustrated in Appendix B.
4.2
Built-in channel types
Built-in channel types define the fundamental interactions that are permitted to occur between processes. The type of a channel can either be explicitly defined in the type signature of a process, or the compiler can infer the type of a channel based on how the processes on either end use it. 4.2.1 Put and Get types As mentioned in Section 3, process definitions may include a type signature with three commaseparated lists of sequential types, input concurrent types, and output concurrent types. Variables and channels are bound to types in the order they appear. We modify server from Example 2 and include its type signature. To effectively illustrate the types, we redefine server to have a server_id variable that it will send back to client: Example 4: Server replies to Client with server id 1 2 3 4 5 6
proc server :: Int | Put ([ Char]|Get(Int| TopBot )) => = -- type signature server_id | ch => -> -- new server_id variable on ch do get msg -- receives msg from client put server_id -- sends server_id back halt
Note that ch has type Put([Char]|Get(Int|TopBot)) which is constructed inductively. The outermost layer Put([Char]|...) defines the first step of the interaction in which a string msg travels from output polarity to input polarity (client to server). Accordingly, in line 4, server uses get to receive msg. In the next layer Get(Int|...), an integer server_id travels from input polarity to output polarity (server to client). In line 5, server uses put to send server_id. The inner-most layer TopBot is the base case and final step. We can close the channel or, as above, halt by closing the final open channel. Appendix C has a complete version of Example 4. 4.2.2
Tensor and Par types
We will now consider compound channel types that allow bundling two (or more) channels into one. The types (*), called tensor, and (+), called par, come from multiplicative linear logic and allow changes to be made to the network of processes while ensuring no cycles are introduced. By unbundling the channels, two new channels are created and passed into two new processes. We modify Example 2 to demonstrate (*). We define a new process two_clients that uses fork to unbundle its output channel two_ch and create two instances of client that both send a message to a modified server process. This server uses split to unbundle its input channel two_ch into two channels, ch1 and ch2. After unbundling, two_ch is no longer in scope in either process.
5
Example 5: Client forks to create two new processes 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
proc client :: | => Put ([ Char]| TopBot ) = | => ch -> on ch do put " Hello Server !" -- client sends string halt proc two_clients :: | => Put ([ Char]| TopBot ) (*) Put ([ Char]| TopBot ) = | => two_ch -> fork two_ch as -- unbundles channels ch1 and ch2 ch1 -> client ( | => ch1) -- creates two new client processes ch2 -> client ( | => ch2) -- that each get one channel proc server :: | Put ([ Char]| TopBot ) (*) Put ([ Char]| TopBot ) => = | two_ch => -> do split two_ch into ch1 , ch2 -- unbundles channels ch1 and ch2 on ch1 do -- interacts with first client get msg close on ch2 do -- interacts with second client get msg halt proc run :: | => = | => -> plug two_clients ( | => two_ch ) -- creates a single two_clients process server ( | two_ch => )
A channel of type (*) indicates that the process on the left will be replaced by two new processes that are both connected to the process on the right. What if we wanted the process on the right to be replaced by two new processes instead? Then, we would use (+) which is dual to (*). For a schematic on the usage of (*) and (+) with split and fork, see Figures 1 and 2 in Appendix D.
4.3
Custom channel types
We have covered some basic channel types, but our processes cannot send variable numbers of messages. Consider process forward in Example 6 that only forwards a single message from source: Example 6: Process that forwards a message 1 2 3 4 5 6
proc forward :: | Put ([ Char]| TopBot ) => Put ([ Char]| TopBot ) = | source => dest -> do get msg on source -- receive message from source put msg on dest -- forward message to dest close source -- close all channels and halt halt dest
To allow forward to call itself recursively until all messages are sent, the channel type needs to be able to change from Put to TopBot. This can be achieved by defining custom channel types, called protocols and coprotocols, which can be recursive. Consider the protocol called PassMessages:
6
1 2 3
protocol PassMessages (A| ) => S = SendMsg :: Put(A|S) => S CloseCh :: TopBot => S
-- passes messages of type A -- handle to send another message -- handle to finish sending messages
The above protocol allows an arbitrary number of type A messages to be sent on a Put channel. The handles represent the set of valid interactions, or session types, that may take place on the channel. The handle SendMsg sets the channel type to Put to allow another message to be sent. Once all messages are sent, CloseCh can be used to change the channel type to TopBot. We modify forward to use the PassMessages protocol to send an arbitrary number of type [Char] messages: Example 7: Process that forwards an arbitrary number of messages 1 2 3 4 5 6 7 8 9 10 11 12 13 14
proc forward :: | PassMessages ([ Char]| ) => PassMessages ([ Char]| ) = | source => dest -> hcase source of -- check whether there is another message SendMsg -> do -- indicates another message will be sent get msg on source on dest do -- forward handle and msg hput SendMsg put msg forward ( | source , dest => )-- recurse CloseCh -> do -- indicates all messages have been sent close source on dest do -- forward handle and halt hput CloseCh halt
The sequential type variable A is instantiated with [Char] on line 1 to send an arbitrary number of strings. A handle is received on the input polarity channel source using hcase on line 3. Process bodies for each handle are defined on lines 4 - 9 and 10 - 14. On lines 7 and 13, a communication session is initiated on the output polarity channel dest by activating it with a handle using hput. This sets the channel type as specified by the handle. Coprotocols are functionally the same as protocols. The only difference between protocols and coprotocols is the direction in which the handles travel on the channel, see Figure 3 in Appendix E. For protocols, handles travel in the same direction as messages on a Put channel (hput on output and hcase on input). For coprotocols, handles travel in the same direction as a Get channel (hput on input and hcase on output). For a modified forward process which uses a protocol to receive from src and a coprotocol to send on an input polarity dest, see Appendix E.
5
Controlled non-determinism
Recall Example 5 in which two client processes each sent a message to server. Notice that server received the messages in a pre-determined order. Consider the case when server echos these messages back. With the features we have used so far, server must have the interactions in a pre-determined order. It would wait for the first client before starting its interaction with the second client, so the second client would also wait for the 7
first client. This is parallel but not concurrent! For true concurrency, server should dynamically opt to have interactions in the order it receives messages. We call this controlled non-determinism which uses the race process command. A non-deterministic server is shown in Example 8: Example 8: Server echos each client in the order it receives messages 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
proc server_deterministic = | winner , loser => -> do on winner do -- interacts with client it received a message from first get msg put msg close on loser do -- interacts with other client get msg put msg halt proc server = | two_ch => -> do split two_ch into ch1 , ch2 race -- controlled non - determinism via a race ch1 -> server_deterministic ( | ch1 , ch2 => ) -- client on ch1 wins ch2 -> server_deterministic ( | ch2 , ch1 => ) -- client on ch2 wins
Races can be held for any number of channels on which a process is waiting for a message. The race on line 14 consists of channels ch1 and ch2 as indicated by lines 15 and 16, respectively. A process body is defined for each channel in the race, and the process will execute according to the winning channel’s corresponding process body. If ch1 wins, line 15 will execute and server_deterministic will be called with ch1 in the argument for the winner channel. If ch2 wins, line 16 will execute and server_deterministic will be called with ch2 in the argument for the winner channel.
6
Higher-order message passing
In sequential functional programming, higher-order functions take other functions as input or produce functions as output. Although higher-order functions are not currently supported in CaMPL, a concurrent analogue, called higher-order processes, is. Higher-order processes encode other processes as sequential data – called a higher-order message, pass a higher-order message, and/or decode and invoke an encoded process. Example 9 shows higher-order processes passing helloworld from Example 1: Example 9: Passing helloworld between higher-order processes 1 2 3 4 5 6 7
proc ho_sender :: | => Put( Store (| Console =>) | TopBot ) = | => ch -> do on ch do put store ( helloworld ) -- encode helloworld and send as a message halt proc ho_receiver :: | Put( Store (| Console =>) | TopBot ), Console => =
8
8 9 10 11 12 13 14 15
| ch , console => -> do on ch do get stored_process -- receive message with encoded helloworld close on console do hput ConsolePut put (" Server says: Running the stored process ") use( stored_process )( | console => ) -- decode and invoke helloworld
Observe that ho_sender and ho_receiver are connected along a Put(Store(|Console=>)|TopBot) type channel. The built-in sequential type Store indicates that a higher-order message is being passed. The type signature of the encoded process, in this case helloworld, is indicated within the Store type. To encode a process, the built-in store function is used. This function takes either the name of a previously defined process, as in the above example on line 4, or it takes an anonymous process as an in-line process definition. To decode and invoke an encoded process, the use process command is used as in the above example on line 15. To use an encoded process, a higher-order process must provide instances of variables and channels of the correct types and polarities as specified by the Store type signature.
7
Discussion and future work
The CaMPL project is still very much in progress. As such, CaMPL is a proof-of-concept langauge. On the implementation side, we are actively working on a paper to comprehensively document every programming feature. We are working on updating the compiler to be able to race protocol/coprotocol handles. We also want to add features to work with processes that are distributed over multiple devices and connected by a network. We have summarized the programming features discussed in this article, and the corresponding process commands in Table 1 in Appendix A. On the categorical semantics side, we are working on a precise semantics for non-determinism that considers how races interact with the other features. We are also considering a categorical semantics for message passing between quantum processes [CS23]. This will contribute to the development of programming languages for distributed quantum computing over a quantum internet.
References [CP09]
Robin Cockett and Craig Pastro. “The logic of message-passing”. In: Science of Computer Programming 74.8 (2009), pp. 498–533 (cit. on p. 1).
[CS23]
Robin Cockett and Priyaa Varshinee Srinivasan. Quantum Message Passing Logic (Talk). https://www.reluctantm.com/gcruttw/fmcs2023/Slides/FMCS_2023_Day_2.pdf. Accessed: 2026-04-13. 2023 (cit. on p. 9).
[CS97]
Robin Cockett and Robert Seely. “Weakly distributive categories”. In: Journal of Pure and Applied Algebra 114.2 (1997), pp. 133–173 (cit. on p. 1). 9
[How80]
William A. Howard. “The Formulae-as-Types Notion of Construction [Original manuscript from 1969]”. In: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Ed. by Jonathan P. Seldin and J. Roger Hindley. Academic Press, 1980, pp. 479–490. isbn: 978-0-12-349050-6 (cit. on p. 1).
[Kum18]
Prashant Kumar. “Implementation of Message Passing Language”. Master’s Thesis. Calgary, Alberta, Canada: University of Calgary, Feb. 2018. url: https://cspages. ucalgary.ca/~robin/Theses/PrashantKumar.pdf (cit. on p. 2).
[Lam69]
Joachim Lambek. “Deductive systems and categories II: Standard constructions and closed categories”. In: Category Theory, Homology Theory and their Applications I. Ed. by P. Hilton. Vol. 86. Lecture Notes in Mathematics. Springer, 1969, pp. 76–122 (cit. on p. 1).
[Lam72]
Joachim Lambek. “Deductive systems and categories III: Cartesian closed categories, intuitionist propositional calculus, and combinatory logic”. In: Toposes, Algebraic Geometry and Logic. Ed. by F. W. Lawvere. Vol. 274. Lecture Notes in Mathematics. Springer, 1972, pp. 57–82 (cit. on p. 1).
[Lit22]
Alexanna Little. “Semantics for Non-Determinism in the Categorical Message Passing Language”. PURE Final Assignment: Research Findings and Synthesis. Calgary, Alberta, Canada: University of Calgary, Sept. 2022. url: https://github.com/camplucalgary / campl/ blob / main/ resources / PURE2022 _ResearchFindingsSynthesis _ Little.pdf (cit. on p. 2).
[Lit23]
Alexanna Little. “Formalizing Non-Determinism in the Categorical Message Passing Language”. Undergraduate Thesis. Calgary, Alberta, Canada: University of Calgary, Apr. 2023. url: https://github.com/campl-ucalgary/campl/blob/main/resources/ CPSC502F22W23_FinalReport_Little.pdf (cit. on p. 2).
[Lyb18]
Reginald Lybbert. “Progress for the Message Passing Logic”. Undergraduate Thesis. Calgary, Alberta, Canada: University of Calgary, Apr. 2018. url: https://github.com/ campl-ucalgary/campl/blob/main/resources/ProgressForMPL.pdf (cit. on p. 2).
[Nor25]
Melika Norouzbeygi. “Higher-Order Message Passing in CaMPL”. Master’s Thesis. Calgary, Alberta, Canada: University of Calgary, Sept. 2025. url: https://cspages. ucalgary.ca/~robin/Theses/Melika.pdf (cit. on p. 2).
[Pon21]
Jared Pon. “Implementation Status of CMPL”. Undergraduate Thesis Interim Report. Calgary, Alberta, Canada: University of Calgary, Dec. 2021. url: https://github.com/ campl-ucalgary/campl/blob/main/resources/502.02A_interim_pon.pdf (cit. on p. 2).
[Pon22]
Jared Pon. “Redesigning the Abstract Machine for CaMPL”. Undergraduate Thesis. Calgary, Alberta, Canada: University of Calgary, Apr. 2022. url: https://github.com/ campl-ucalgary/campl/blob/main/resources/JaredPon_final_report.pdf (cit. on p. 2).
[Yea12]
Masuka Yeasin. “Linear Functors and their Fixed Points”. Master’s Thesis. Calgary, Alberta, Canada: University of Calgary, Dec. 2012. url: https://cspages.ucalgary. ca/~robin/Theses/masuka_thesis.pdf (cit. on p. 2).
10
A
Summary of types and process commands
The following table summarizes the interactions provided by the built-in channel types, the programming features discussed in this article, and the corresponding process commands. We denote an argument for a sequential type with A and a concurrent channel type with Ch, Ch1, and Ch2. Process command
Channel type
Description
TopBot
Interaction on channel is over.
Neg(Ch) Put(A|Ch) Get(A|Ch) Ch1(*)Ch2 Ch1(+)Ch2
Custom protocol Custom coprotocol N/A Put(A|Ch) or Get(A|Ch)
N/A N/A
Dual interaction of Ch by negating and identifying with another channel. Message of type A travels from left to right (output to input polarity). Message of type A travels from right to left (input to output polarity). Left process becomes two processes both connected to the right process. Right process becomes two processes both connected to the left process. Handles travel from left to right (output to input polarity). Handles travel from right to left (input to output polarity). Connect pairs of processes by channels. Next process command block selected with controlled non-determinism. Encode another process in a sequential Store type. Decode and invoke the process encoded in a Store type.
close or halt
Section 4.2.1
neg and |=| put/get
4.2.1
get/put
4.2.1
fork/split
4.2.2
split/fork
4.2.2
hput/hcase
4.3
hcase/hput
4.3
plug
2
race
5
store
6
use
6
Table 1: Summary of channel types and process commands.
B
Channel polarity example
Defining the way a process uses a channel by both the type and polarity prevents ambiguity that can cause deadlocks. For example, suppose we do not consider polarity and rewrite our code as follows:
11
Example 10: Code without channel polarity (this code will not compile) 1 2 3 4
proc run = | => -> plug client ( | ch ) server ( | ch )
-- connects processes by shared channel ch -- client process has channel ch (no defined polarity ) -- server process has channel ch (no defined polarity )
We know that we want ch to have a type indicating that a message should be sent and received on it. However, if both processes are defined to first receive a message and then reply, they will both become stuck waiting for a message to be sent by the other: 1 2 3 4 5 6 7 8 9 10 11 12 13
proc client = | ch -> on ch do get msg -- receives server ’s message put " Hello Server !" -- sends message to the server halt proc server = | ch -> on ch do get msg -- receives client ’s message put " Hello Client !" -- sends message to client halt
This is precisely what a deadlock is. In this simple example, it is easy to see the mistake, but in more complicated programs, the type system with polarities has the ability to catch these sorts of errors. Each channel type specifies the complementary roles of the processes on each end of the channel to ensure it is unambiguous.
C 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Put and Get types example
proc server :: Int | Put ([ Char]|Get(Int| TopBot )) => = -- type signature server_id | ch => -> -- new server_id variable on ch do get msg put server_id -- sends server_id back halt proc client :: | => Put ([ Char]|Get(Int| TopBot )) = -- type signature | => ch -> on ch do put " Hello Server !" get int halt proc run = | => -> plug -- connects processes by shared channel ch client ( | => ch ) -- creates client process server ( 5 | ch => ) -- creates server process
12
D
Schematic of fork and split
The diagrams in Figures 1 and 2 visualize the change in the process network on channel types (*) and (+). We use + to denote the output polarity end and - to denote the input polarity.
/
-
-
+
+
Process 𝐴1
fork / split
(*)
Process 𝐴
Process 𝐵
Process 𝐴2
Process 𝐵
+
Figure 1: Change in process network on (*) type
-
split / fork
(+)
+ Process 𝐴
-
/
Process 𝐵1
+ Process 𝐴
+
Process 𝐵
-
Process 𝐵2
Figure 2: Change in process network on (+) type
E
Protocol and coprotocol example +
hput
PassMessages
hcase −
+ hcase
CoPassMessages
hput −
o
/
Figure 3: Direction of handles on protocols and coprotocols Protocol handles travel in the same direction as messages on a Put channel, so forward is receiving handles on source. Coprotocol handles travel in the same direction as messages on a Get channel, so forward is sending handles on dest. To demonstrate a usage of coprotocols, we consider process forward which forwards a single message from source over an input channel dest: Example 11: Process that forwards a message 1 2 3 4
proc forward :: | Put ([ Char]| TopBot ), Get ([ Char]| TopBot ) => = | source , dest => -> do get msg on source -- receive message from source put msg on dest -- forward message to dest
13
5 6
close source halt dest
-- close all channels and halt
We need forward to send an arbitrary number of strings on a Get channel. Furthermore, we want handles to travel in the same direction as the messages, so we define a coprotocol version of PassMessages (in Section 4.3 ) called CoPassMessages to forward the messages on dest. 1 2 3
coprotocol S => CoPassMessages (A| ) = CoSendMsg :: S => Get(A|S) CoCloseCh :: S => TopBot
Notice that the state variable S is on the left side of => in the CoPassMessages definition instead of the right side in PassMessages. We use different handle names than in PassMessages because all handle names must be globally unique. We modify forward to use PassMessages and CoPassMessages as follows: Example 12: Process that forwards an arbitrary number of messages 1 2 3 4 5 6 7 8 9 10 11 12 13 14
proc forward :: | PassMessages ([ Char]| ), CoPassMessages ([ Char]| ) => = | source , dest => -> hcase source of -- check whether there is another message SendMsg -> do -- protocol handle that indicates another message get msg on source on dest do hput CoSendMsg -- send coprotocol handle to forward msg put msg forward ( | source , dest => ) -- recurse CloseCh -> do -- protocol handle that indicates all messages sent close source on dest do hput CoCloseCh -- send handle to indicate all messages sent halt
14