Has anyone done any choreographic programming with Elixir? The idea is that, instead of writing parts of a concurrent system separately and hoping that you’ve gotten the interactions between clients and server right, you instead write a choreography from some global viewpoint; a compiler of some sort then takes this choreography and constructs projections for each participant in the system.
See page 5 for and example in a Java-like language: https://arxiv.org/pdf/2303.03983v3 (that’s a direct link to the Real-World Choreographic Programming paper)
Makes a little bit more sense now. Building such a thing in elixir with metaprogramming is trivial, the other question is whether we need such a feature.
The processes from elixir are concurrent entities that implement message passing out of the box. That example could be implemented more or less with the features already present in Elixir.
Highly doubt it, such concepts that involve a paradigm shift need to be extremely good for anyone to take them seriously. I can see how languages like Java could greatly benefit from it, however in Elixir I doubt this improves anything over existing way to write code.
The chief motivation for choreographies is that they produce deadlock-free programs by construction, which is a pretty neat property. (See paper for details.) This is especially compelling for environments that need strong safety assurances.
Elixir—while providing higher-level concurrency primitives than, say, Java—doesn’t do deadlock-free construction natively.
OK, so it sounds like you’re saying that you (@fmn and @D4no0) feel like choreographies are a common paradigm in Elixir code (I agree based on my experience) but that no one is doing mechanical endpoint projection. That’s good! That means I’ve got some work to do.
you could try to poke around slim intersection of “Elixir” and “BPM” / “Business Process Management”, no promises though
in Elixir software i was witnessed, it was quite often bit implicit choreography baked into application itself.
at the end, it might be a default way of going things, no? particular app/service/actor knows that “if i got this (pun intended) i do that” etc. and when you have bunch of apps/services/actors which just know what to do when something happens, well, you have choreography, i guess?
At a high level, it sounds like this choreography overlaps quite a bit with OTP and the primitives it and Elixir provides out of the box. A choreography as I understand it captures both the participants at play and the types of messages passed between them.
For the first aspect, choreographing the participants at play translates to orchestrating processes and can be explicitly defined via Supervisors, DynamicSupervisors, and Supervision Trees.
Then for the second aspect, the types of messages being passed e.g. the security protocol notation used in choreographic programming e.g. Alice.expr -> Bob.x could be translated to Alice.expr -> Alice.call(Bob, {:expr, result}) -> Bob.handle_call({:expr, result}, Alice) assuming Alice and Bob were GenServers.
As far as I know, there aren’t any guardrails in place that ensures all messages that are passed are handled/acted upon aside from test coverage. For asynchronous communication, a process “casting” with its message is totally happy shouting into the void aka it’s message “left unread” in the black hole of the receiving process’ mailbox so to speak. But when it comes to synchronous communication, a process “calling” with its message will get temporarily blocked if left unread and surface an error if the reply is used downstream so that generally gets caught pretty quickly. Regardless, preventing missing callbacks could be a potential area where choreographic programming would shine.
It seems like a fundamental value add from a dev experience perspective is how workflows can be expressed/encoded as a sequence diagram via choreographies and then translated into projections that represent the participants in those diagrams with the required send/receive functions defined. In my book, both ways of “framing” can be useful and being able to flip between the two depending on the situation would be pretty sweet.
For example, it would be cool if you could just write some choreography that uses endpoint projection to generate the proper Supervisor and GenServer implementations or biolerplate. On the flip side, it’d also be very cool to create an editable “virtual” file that stitches together the choreography for a specific workflow rather than rifling through multiple files/functions from a stacktrace.
This is not a novel idea, but I have a feeling the outcome will be the same as previous attempts. There was an attempt back in the day to integrate UML diagrams more into development, some tools even offered code generation based on diagrams.
While the idea is not bad, adding another layer of abstraction into the equation makes writing code even harder and requires developers to know not only the ecosystem that is the base but also how to correctly design with the new abstraction.
The one thing I would love to see however, is a visual representation of this from the written code. A lot of times it becomes hard to reason about a collection of processes interacting between each-other, ideally in a format like cisco packet tracer, where you can also see everything happening in real-time.
really? I’d assume the wikipedia example would look sth like
def client() do
send(cas_pid, {credentials, serviceID})
receive do
result -> client_does_something()
end
end
def service() do
receive do
result -> server_does_something()
end
end
def cas() do
receive do
request ->
case check(request) do
:success ->
token = genToken(request)
send(client_pid, {:success, token})
send(server_pid, {:success, token})
:failure ->
send(client_pid, :failure)
send(server_pid, :failure)
end
end
end
(please do not use this CAS in production)
Can you provide a more choreocrapic example?
Can you point to some public code that brought you to your conclusion?
Maybe I am not reading well but it does sound like OP is after something like TLA+. It is made to guarantee that no deadlocks or various other parallel displeasantries happen in your code.
I’d say Erlang/Elixir’s processes, Golang’s goroutines and Rust’s channels are quite close to what is being referred to as choreographic programming but you can still shoot yourself in the foot (you can also deadlock 2 or more Elixir processes if you really try).
If what OP is thinking about is also what I am thinking, they want declarative programming that provides various guarantees just by the virtue of how are various agents described but IMO we’re not quite there yet. So far that’s kind of sci-fi I am afraid, at least from the point of view of the classic / mainstream programming.
Fwiw, TLA+ is a language (and toolchain) for describing algorithms and not code. It shines for concurrent algorithms, but is equally useful for the state machine approach to computation in general (it views the latter as a generalisation of the former in any case)
TLA+ and choreographic programming are related in the sense that they both work with concurrent systems, but CP gets you a correct-by-construction implementation. TLA+ is “just” for model checking. (Still super useful and really cool! Glad to see TLA+ is known to some other folks.)
So far that’s kind of sci-fi I am afraid, at least from the point of view of the classic / mainstream programming.
I should have been more clear (and maybe this will clear up some of the confusion I’ve been seeing from others): I am a programming languages researcher. I am not looking for some tool to solve some concrete problem. My job is to make this “sci-fi” a reality.
Choreographic programming is a new paradigm that can solve whole classes of bugs, and I’m experimenting with CP and Elixir. Everyone is going to have some tacit choreography in their programs; CP as a paradigm brings these protocols/agreements/choreographies to the forefront and treats them as a thing in and of themselves.
I need to know if someone has encountered a library to do the automatic choreography → endpoint projection before. I’m pretty sure the answer is “no” since no one has mentioned a concrete library.
All the tools y’all have mentioned suggest that solving concurrency bugs is something you have on your minds. That’s good because it means there’s a need that this might fill!
Choreographies differ significantly and materially from the UML-based code generation you’re describing. I agree that kind of tool makes things harder to maintain. Choreographies are code, though, so they don’t have the same drawbacks. If you (or anyone else) would like to see more about choreographies, these papers are useful:
The one thing I would love to see however, is a visual representation of this from the written code. A lot of times it becomes hard to reason about a collection of processes interacting between each-other, ideally in a format like cisco packet tracer, where you can also see everything happening in real-time.
Pirouette seems interesting, but the assumptions it makes seem to diverge somewhat from practical reality:
in 2.2: “Message sending is instantaneous and certain: messages do not get lost in the air.”
in 3.1, referencing the conditions on the SendE rule: “The second check reflects the fact that sends from a node to itself is not meaningful.”
That latter one would come as a surprise to most BEAM developers
Agreed that it’s an interesting read, but the one thing that isn’t in that paper is the actual choreography! It’s tricky to evaluate a technique’s expressiveness without seeing it express things.
Pirouette seems interesting, but the assumptions it makes seem to diverge somewhat from practical reality
You might have noticed that Pirouette is mostly concerned with making sure that the guarantees of choreographic programming hold in an ideal scenario—if they didn’t we’d be in trouble. Instantaneous and certain messages seems reasonable when you’re running on a single machine—unless there’s some other underlying bug in the BEAM.
Extending the formalism to account for self-sent messages wouldn’t be all that difficult. This idiom is certainly convenient with BEAM languages; I would argue that it’s not essential to concurrent programming so it’s understandable why the authors chose this. Again, that doesn’t mean we couldn’t adapt the findings from this paper to BEAM languages.
Real-World Choreographic Programming
the one thing that isn’t in the paper is the actual choreography
It is, actually—though it’s a little tricky to spot. On the first page there are two badges about the artifact. (In this case, that’s the source for the IRC server/client & choreography.) You can click on those to get a link to where the artifact is hosted on Zenodo: Accepted Artifact for Real-World Choreographic Programming: Full-Duplex Asynchrony and Interoperability. This is typical for most research papers; most journals and conferences would prefer a full code listing separate rather than embedded in a PDF. I agree it would have been nice to see more snippets from the choreography in this paper, but I can understand also why the authors did it the way they did.
