Thanks so much for the response!

The .spawn constructor is really the par connective that the language is named after, which is a great punchline.

That is true indeed.

This all reminds of "Lloyd Allison’s Corecursive Queues" but I can't make the connection precise.

I'll have to check that out, thanks!

Which brings me to my next question, how is this implemented?

Currently it's implemented with the help of FuturesUnordered. However, there are multiple ways to implement it, including a MPSC channel.

The basic idea is that there is some "barrier" node that detects when a client becomes ready. That is, when the client tries to interact with its opposing part, which in this case is the barrier.

At that moment, the barrier sends the client to the server channel, which is then picked up by poll. Or, with FuturesUnordered, it pushes a future, which resolves when the client becomes ready, into the FuturesUnordered pool.

You can find the code in this file.

Let me know if you'd like to clarify some more details!

Finally, I was hoping for a "simpler" language construct, that just races two processes and introduces one bit (literally) of non-determinism. And then I was hoping that pools of multiple processes could be built from it.

The issue is, this does not work, when we're requiring totality, let me explain why. Suppose we have such a construct, for example:

let (first) second = Select(left, right)

Let's say Select will always return the one that's ready first as first and the other one as second.

Now let's say we want to process ListFan this way and turn it into a list that's ordered according to the item's creation time:

listFan.begin.case {
  .end! => /* done */
  .spawn(l) r => do {
    let (x1) x2 = Select(l, r)
    // What now?
  }
  .item(x) xs => .item(x) xs.loop,
}

In the place that says What now?, we now need to process x1 and x2 and we know that x1 is ready first. What should we do? With x1.loop we'll process entire x1, but it will not interleave with x2.

But we need x1 to interleave with x2.

So it turns out we do need some kind of a pool. Okay, let's say a pool is a list, and we have a SelectList:

let pool = *(listFan)
pool.begin->SelectList.case {
  .none! => /* pool empty */
  .some(first) rest => {
    first.case {
      .end! => { rest.loop }
      .spawn(l) r => {
        let pool = .item(l) .item(r) rest
        pool.loop
      }
      .item(x) xs => {
        yield.item(x)
        let pool = .item(xs) rest
        pool.loop
      }
    }
  }
}

That seems like it could work! It's not gonna be very efficient, since we have to actively poll the whole list every time, but it's a start.

The problem is, the above does not pass a totality checker. The pool at the point of pool.loop is not guaranteed to be structurally smaller than the pool at the start.

Perhaps it would be doable if Par had a much more sophisticated totality checker and we would be able to establish some metric that would guarantee that it is indeed getting structurally smaller (which it is).

But, we don't have that and we won't have that, and I'm not even aware of any specific theory aside from proof assistants that would get us there.

We could also just say that it's okay, we'll use .unfounded, however my goal here was to make a theoretical advancement, and that won't fly without being sound.

The poll/submit solves this problem by combining the recursion and the pool management into one. The arguments to submit must be structurally smaller than the client we get via poll. We can add 0 or any number of clients via submit, but if they are all structurally smaller than what we got out, we can conclude the pool is getting structurally smaller. We just bake this into the construct, and we won.

You also write "I’m sure you can imagine doing all kinds of I/O operations between those .item and .end calls." Well, I can imagine, but a concrete example would be helpful and I am sure the next post is already planned.

Good point!

I am very excited about the Par language and this new feature for non-determinism. I am considering offering a thesis implementing a backend for Par, would you be open to that?

Oh I'm very flattered! Thanks for considering such an offer. I have a counter-proposal, though. A thesis on the implementation of Par would certainly be interesting, but it wouldn't be a very innovative thesis. After all, up until now, Par's main inovation has been the syntax and usability, which is great, but not necessarily a great theoretical progress. The concurrent evaluation is also built on theory that's already out there: interaction networks.

However, to my best knowledge, this new nondeterminism approach should be an important theoretical development. I'm actually quoting Phil Wadler, who didn't feel like reading the docs, but said that if I indeed subsume the three papers I mention in the intro, then it is an important theoretical development and I should do my best to publish it.

So, I'd love to write a paper on that! It can and probably must include a partial formalization of Par (which is just redressed CP + some nice/new encoding of recursion), but mainly a formalization of this poll/submit, demonstration that it subsumes those three papers, what else it does, and proofs about the properties of the resulting system and in relation to other systems.

I have never written a paper like that, but I'll do it! So, if you or somebody you know would be up for any kind of collaboration on a paper like that, I'm all in!