Porting "match!" Joinads semantics

[hopac]

Porting "match!" Joinads semantics

[polytypic]

This is an interesting topic. Unfortunately, I don't really have the time to investigate this properly right now.

I did some quick reading of the JoCaml manual and read a few pages from the beginning of The Join Calculus: a Language for Distributed Mobile Programming.

The join-calculus is primarily designed for distributed programming rather than for in-process concurrency like Concurrent ML and Hopac that more closely resemble the pi-calculus with non-deterministic choice.

It seems to me that the main design choice made in join-calculus to make it amenable to distributed programming is the "strict adherence to local synchronization".

What does local synchronization mean?

I would say that it essentially means that there is no synchronization at all between processes. The "synchronization" that join-calculus talks about just means accepting a combination of messages that have been received by a process.

Join-calculus is like Erlang or F# MailboxProcessor with pattern matching over multiple separate messages sent/received at different times. With Erlang and MailboxProcessor (using Scan), the actor, upon receiving a message, tries to pattern match the message and if the matching fails, the message remains in the mailbox. The essence of join-calculus seems to be to extend that pattern matching to occur over multiple messages.

In Erlang and with the MailboxProcessor there is only one mailbox, while in join-calculus a "process abstraction" can define multiple channels. The definition of multiple channels is surely convenient, but does not seem to really add anything, because it seems that if you define a discriminated union type with a case for each channel, you can then coalesce the channels into a single combined channel. After the channels are coalesced, you are left with one channel or mailbox and you then perform the match locally (within the single process abstraction) over all the messages held in the one mailbox.

On the Wikipedia page it is said that

the join-calculus is as expressive as the full pi-calculus

In the JoCaml manual, an encoding of pi-calculus channels is given:

#let new_pi_sync_channel () =
   def send(x) & receive() = reply x to receive & reply to send in
   send, receive
 ;;
val new_pi_sync_channel : unit -> ('a -> unit) * (unit -> 'a) = <fun>

Now, I hope, by this time, you are familiar enough with Concurrent ML or Hopac that you can immediately tell (by looking at the type) that the above does not suffice for encoding channels of CML/Hopac. What the pi-calculus reference seems to be about is about versions of pi-calculus without non-deterministic choice. The join-calculus paper rather plainly states that such a mechanism is not provided by join-calculus and encoding it would be cumbersome:

the CCS (or pi calculus) “external choice” operator is conspicuously absent from our list of encodings : this device can express an atomic choice between communication offers on arbitrary channels, and thus intrinsically creates non-local contention. Its join calculus encoding would necessarily include some rather cumbersome mechanism for resolving this contention

CML/Hopac basically adds two layers of abstraction on top of the simpler form of pi-calculus channels. First of all they add non-deterministic choice, so one can form a choice of multiple send/receive operations of which at most one will be completed. This is also present in Clojure's core.async and Go. On top of that, CML/Hopac (and Racket) adds the event/alternative mechanism with negative acknowledgments that allows the definition of new synchronous operations that can participate in a non-deterministic choice.

In join-calculus, you have both AND and OR -patterns, but these patterns are only over messages held in the mailbox of a single process. There is no communication between processes at the time when the pattern matching in join-calculus occurs. The messages have been asynchronously sent to the process and the process then matches over the bag of messages it has.

Now, what you quoted:

Joinads allow "waiting for several concrete values from several channels"

doesn't really compare directly to CML/Hopac or pi-calculus with non-deterministic choice. First of all, channels in join-calculus are asynchronous rather than synchronous with non-deterministic choice. Also,
channels in join-calculus are many-to-one rather than many-to-many. Furthermore, I do believe that one could coalesce the channels that a process in join-calculus is matching over into one without loss of generality.

In summary, what the join-calculus really allows is for a single process to wait for a combination of multiple asynchronously sent messages defined by a pattern matching expression.

So, to answer your actual question. The channels of join-calculus and Hopac are very different in nature. Trying to emulate one directly with the other will not work (either way). A join-calculus definition essentially defines a single actor that waits for a combination of one or more messages defined by a pattern matching expression. To implement something like that with Hopac, you should define a process with just one channel for receiving the messages, take messages from the mailbox as they arrive and put those messages into a bag (allowing duplicates). Then upon receiving a new message, the process should pattern match over the messages in the bag. If a matching combination is found, the process removes the corresponding messages from the bag, performs the associated action and then wait for further messages.

I think that adding support for join-calculus channels to Hopac could make sense. The addition would be mostly about making the local (entirely sequential) pattern match algorithm efficient (unlike the naive match over all messages in a bag) and the notation usable.

One more addition: Alt.choose and match! have completely different semantics. Neither can emulate the other. Alt.choose performs a non-deterministic concurrent choice between synchronous operations than involve communication between multiple processes. match! performs a pattern match over asynchronously sent messages received by a process and the matching can be performed entirely sequentially without any communication between multiple processes.

Addition: Actually I see now that there is one core aspect of join-calculus that I'm not entirely sure about at this point. In the above I've assumed that a single process abstraction corresponds to a single process. That may not actually be the case and if it isn't then the above translation of a process abstraction to a single process is not correct. Even if each message sent to a process abstraction might spawn a separate process much of the above still holds, but the single Erlang/MB processes analogy would be obviously incorrect. I'll have to finish reading the paper.

Addition: Yes, after reading the semantics more carefully, it is clear that there is nothing that would inherently prevent two right hand sides in a match from being executed in parallel. In most of the examples only one right hand side can be live at any time due to the state (e.g. counter value) being passed within the process abstraction. Nevertheless, this changes the above discussion only in that after finding a match, the right hand side "action" is spawned as a separate process and the matching process then immediately starts waiting for other potential matches.

[vasily-kirichenko]

Thanks for very detailed answer! Will think and re-read it.

About adding support for join-calculus to Hopac - do not get me wrong, I don't have any real world use cases for it, this question was mostly theoretical.

[polytypic]

Related idea to extend CML with a join combinator:

https://github.com/VesaKarvonen/JoinCML

If JoinCML ultimately turns out to be easy enough to implement efficiently, Hopac could be extended to support it.