§ INTRODUCTION

Choreographic programming (CP) <cit.> is a paradigm for programming distributed applications that run on multiple nodes.

In CP the programmer writes one, unified program, called a choreography, that is then compiled to individual programs for each node via a compilation step called endpoint projection (EPP).

For example, the following choreography describes a distributed data processing pipeline, involving nodes Alice, Bob, and Carol, which respectively run functions $f$, $g$, and $h$ on their input:

\begin{equation*}
\begin{split}
x \leftarrow \; & \locally{\mathrm{Alice}}{\mathsf{getInput}} \\
y \leftarrow \; & \comm{\mathrm{Alice}}{\mathrm{Bob}}{f(x)} \\
z \leftarrow \; & \comm{\mathrm{Bob}}{\mathrm{Carol}}{g(y)} \\
w \leftarrow \; & \comm{\mathrm{Carol}}{\mathrm{Alice}}{h(z)} \\
& \locally{\mathrm{Alice}}{\mathsf{showResults}(w)} \\
\end{split}
\end{equation*}

Here, we use $\leftarrow$ for variable bindings;

$\locally{\mathrm{Alice}}{t}$ denotes a local computation $t$ at Alice;

and $\comm{\mathrm{Alice}}{\mathrm{Bob}}{t}$ denotes communication from Alice to Bob with message $t$.

In this choreography, Alice first gets some input locally, processes it with $f$, and passes the result to Bob, who processes it with $g$ and passes the result to Carol, who processes it with $h$ and passes it back to Alice to be displayed to the user.

To get an executable program for each node, we can apply endpoint projection to the choreography, resulting in individual programs for Alice, Bob, and Carol:

\[
\begin{minipage}{.35\textwidth}
\begin{equation*}
\begin{split}
x \leftarrow \; & \mathsf{getInput} \\
& \mathsf{send}(\mathrm{Bob}, f(x)) \\
w \leftarrow \; & \mathsf{recv}(\mathrm{Carol}) \\
& \mathsf{showResults}(w)
\end{split}
\end{equation*}
\end{minipage}
\hfill\vline\hfill
\begin{minipage}{.3\textwidth}
\begin{equation*}
\begin{split}
y \leftarrow \; & \mathsf{recv}(\mathrm{Alice}) \\
& \mathsf{send}(\mathrm{Carol}, g(y)) \\
\end{split}
\end{equation*}
\end{minipage}
\hfill\vline\hfill
\begin{minipage}{.3\textwidth}
\begin{equation*}
\begin{split}
z \leftarrow \; & \mathsf{recv}(\mathrm{Bob}) \\
& \mathsf{send}(\mathrm{Alice}, h(z)) \\
\end{split}
\end{equation*}
\end{minipage}
\]

A correct CP language guarantees soundness and completeness of EPP, which further implies that the collection of projected programs is deadlock-free when running together.

Existing research places CP on a solid theoretical foundation <cit.>,

which has informed the design of practical, full-featured standalone CP languages such as Choral <cit.>.

Recent work has introduced library-level CP languages <cit.>, in which choreographies and EPP are completely expressed as constructs in an existing host language.  For example, HasChor <cit.>, implements support for CP by means of a domain-specific language embedded in Haskell.
In HasChor, choreographies are monadic computations in which choreographic operators such as $\locally{\_}{\_}$ and $\comm{\_}{\_}{\_}$ may be used, and EPP is carried out by means of dynamic interpretation of choreographies at run time.  The recently proposed ChoRus library for choreographic programming in Rust <cit.> takes a similarly dynamic approach.

Library-level CP frameworks have the potential to improve the accessibility and practicality of CP by integrating it into general-purpose programming languages.

However, there are no proofs of correctness of EPP for library-level CP frameworks. Indeed, it is unclear to what extent the established theory of CP is applicable in the setting of library-level CP.

To close this gap, in this paper we propose algebraic effects <cit.> as a foundational approach for implementing and verifying library-level CP.

Algebraic effects provide an abstraction that generalizes existing approaches to library-level CP.

In particular, they allow us to define choreographies as computations with user-defined effects and EPP as location-specific effect handlers.

Algebraic effects also lend themselves to proofs of correctness.

They provide abstract syntax trees for choreographies in which CP-specific effects and control flows are manifest, enabling reasoning about them.

Furthermore, given that algebraic effects are “going mainstream” <cit.>, with efficient implementations now available in languages such as OCaml <cit.> and Koka <cit.>, we believe our proposed approach would make library-level CP less ad-hoc and bring it to a broader audience.

In the rest of the paper, we set up a framework for programming with algebraic effects in Agda (<Ref>), which we then use to implement a prototype library-level CP framework (<Ref>).  Finally, we discuss our ongoing work on leveraging our approach to prove the correctness of our library-level CP implementation (<Ref>).  This paper is a literate Agda program.

§ A MINIMAL ALGEBRAIC EFFECTS FRAMEWORK IN AGDA

In this section, we define a minimal algebraic effects framework in Agda, which we will use to implement CP in the next section.

No prior knowledge of algebraic effects is assumed.

We introduce each concept first from a mathematical perspective and then relate it to programming.

Due to lack of space, we do not include any examples in this section, but the next section can be seen as a demonstration of the framework.

Our presentation is influenced by <cit.> and <cit.>, and we refer the reader to them for a comprehensive introduction to algebraic effects.

[0]– the standard library `mkRawMonad` is not general enough for our use

[0]– so we define our own version

§.§ Signatures and Algebras

A signature Sig specifies the equipped operations of an algebra, which includes a type Op of operations and a function Arity giving the number of arguments (represented as the cardinality of a type) of each operation:[Agda uses an infinite hierarchy of universes where $\AgdaPrimitive{Set} : \AgdaPrimitive{Set}_1 : ... : \AgdaPrimitive{Set}_n : \AgdaPrimitive{Set}_{n+1}$ to avoid paradoxes.

For ease of presentation in this paper, we overconstrain the universe of Op to be Set₁ (similarily for Arity).

The actual implementation is universe-polymorphic,
but readers can safely ignore the universe hierarchy without missing the key point of the paper.]

A set $X$ that implements the operations of a signature $\mathbb{F}$ is called an $\mathbb{F}$-algebra.

An $\mathbb{F}$-algebra on the carrier set $X$, written as $\mathbb{F}$ -Alg[ $X$ ] in Agda, is a function of type ⟦ 𝔽 ⟧ $X \rightarrow X$:

\[
\begin{minipage}{.5\textwidth}
\begin{center}\begin{code}%
\>[0]\AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{Sig}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{Op}\AgdaSpace{}%
\AgdaOperator{\AgdaInductiveConstructor{◁}}\AgdaSpace{}%
\AgdaBound{Ar}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{X}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{Σ[}\AgdaSpace{}%
\AgdaBound{o}\AgdaSpace{}%
\AgdaFunction{∈}\AgdaSpace{}%
\AgdaBound{Op}\AgdaSpace{}%
\AgdaFunction{]}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{Ar}\AgdaSpace{}%
\AgdaBound{o}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{X}\AgdaSymbol{)}\<%
\end{code}\end{center}
\end{minipage}
\begin{minipage}{.5\textwidth}
\begin{center}\begin{code}%
\>[0]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}-Alg[\AgdaUnderscore{}]}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{Sig}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
\>[0]\AgdaBound{𝔽}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{-Alg[}}\AgdaSpace{}%
\AgdaBound{X}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}%
\AgdaBound{𝔽}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}%
\AgdaBound{X}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{X}\<%
\end{code}\end{center}
\end{minipage}
\]

⟦ 𝔽 ⟧ $X$ denotes an operation paired with its arity number of elements from the carrier set — a fully applied operation.

⟦ 𝔽 ⟧ $X \rightarrow X$ allows us to make a new element out of a fully applied operation, the very nature of an algebra.

In programming, we can view an effectful operation as giving rise to an algebra, with the allowed effects being the signature, the result of an effect being the arity of the operation, and a carrier set of such an algebra being a functional model of the effectful computation.

§.§ The Free Algebra

Among all the algebras of a signature $\mathbb{F}$, we are particularly interested in one called the free algebra.

Rather than performing operations in the carrier set, the free algebra merely records them as a data type, which we call Term:

The var constructor denotes a variable drawn from some set $A$.

The op constructor denotes a fully applied operation to some other terms.

In programming, Terms correspond to programs where effects are left uninterpreted, with variables being pure computations and operations being effectful computations.

Terms also form a monad (it is actually the free monad), which allows us to chain them together:

We also provide a helper function perform, which constructs a Term that performs an operation and immediately returns its result:

§.§ Effect Handlers

One of the reasons why Terms are called the free algebra of $\mathbb{F}$ is that they are freely interpretable.

Given another $\mathbb{F}$-algebra $X$ and a substitution of variables from $X$, we can interpret a term as an element of $X$:

For variables, interp uses the substitution $f$ to map them to $X$.

For operations, interp first recursively interprets the arguments and then uses ${alg}$ to make a new element of $X$ from a fully applied operation.

In programming, interp forms the foundation of effect handlers.

It lets us systematically handle uninterpreted effects of a computation.

§ CHOREOGRAPHIC PROGRAMMING WITH ALGEBRAIC EFFECTS

In this section, we use the algebraic effects framework from the previous section to implement a CP language.

Due to lack of space, we only consider a minimum CP language with only local computations and communication, omitting features like conditionals and recursion for now.

We start by defining processes (<Ref>), which are the results of endpoint projection.

Then, we move on to defining choreographies (<Ref>).

Unlike previous library-level CP languages, our choreographies abstract over a particular representation of located values, allowing us to erase them and avoid non-totality.

Finally, we define endpoint projection as location-specific effect handlers for choreographies (<Ref>).

We assume a local language of signature 𝕃 that each node uses for local computations, and we parameterize our CP language by it.

We use locations Loc to refer to nodes in a distributed system and define them as Strings.

However, any data type with decidable equality would suffice.

[0]– the opaque prevents Agda from unfolding the definition, making the code more readable in certain cases

[0]– the stdlib's ⊤ is not universe-polymorphic

§.§ Processes

[0]– a seperate modules avoid name conflicts

Processes as Algebraic Effects

<Ref> presents processes as algebraic effects.

Signature ℙ specifies the three operations of processes and their arity:

* `locally performs a local computation of type Term 𝕃 $A$ and returns a value of type $A$.

* `send sends a message of type $A$ to a location and returns a unit value.

* `recv receives a message from a location and returns a value of type $A$.

Here, the performer of the `recv needs to specify what type of value it is expected to receive.

We also define Process as a shorthand for terms using operations from ℙ. Finally, we define the helper functions send, receive, and locally.

§.§ Choreographies

[10]

[2]– the module ends here

[12]

Choreographies as Algebraic Effects

<Ref> presents choreographies as algebraic effects.

One issue that every library-level CP language needs to deal with is how to represent located values.

Located values are variables in a choreography that denote values at different locations.

We give them types $A \ @ \ l$, which intuitively means a value of type $A$ at location $l$.

Existing library-level CP languages such as HasChor <cit.> define located values as a union of a plain value and a unit value — an option type — and have the unspoken invariant that when projecting to location $l$, values at $l$ are a plain value, and otherwise, a unit value.

Internally, HasChor uses an unwrap function to extract the plain value from the union.

The unwrap function is non-total because the union could be a unit value, but HasChor meticulously use it only in situations where the union is a plain value (implicitly use the invariant), so the non-totality never shows up.

This approach does not work in Agda, as it demands that every function be total.

For this reason, we take an alternative approach to located values, in which they are kept abstract and erased before projection in a way that respects the invariant by construction.

We first define At, a type-level function that captures the interface of located values.

Then, we define focus, a particular At that we will use in endpoint projection (we will show another At in the next section).

Intuitively, focus $l$ erases a located value of type $A \ @ \ s$ to $A$ if $l$ is equal to $s$; otherwise, to a unit value.

The signature ℂ specifies the two main operations of choreographies using one overloaded constructor:

* `comm $s$ $s$ $t$ denotes a local computation $t$ at location $s$.

* `comm $s$ $r$ $t$ denotes location $s$ sends the result of a computation $t$ to location $r$.

We also define Choreo as a shorthand for terms using operations from ℂ abstracted over a particular At.

We also require At to be an instance of monads for any location $l$, which allows us to chain together located values.

Our focus is a monad because the identity functor and units are both monads.

We also define two helpful functions, _▷_ and _⇒_◇_, for writing choreographies.

§.§ Endpoint Projection

[23]

[14]

[14]
[23]

Endpoint Projection

We can now define endpoint projection, the process of turning a choreography into a process for a target location.

<Ref> presents our implementation of EPP.

The function epp takes a choreography $c$ and a target location $l$, and uses the effect handler interp to interpret operations in $c$.

For variables, we return them in the generated process.

For operations, we construct a ℂ-Algebra (with all located values erased from $l$'s perspective) alg on processes, which does one step of interpretation.

The only operation we need to interpret is `comm, depending on whether $l$ is equal to $s$ and $r$:

* If $l$ equals $s$ and $r$, meaning $s$ and $r$ are the same, we interpret this operation as a local computation followed by the continuation.

* If $l$ equals $s$ but not $r$, meaning the target location is the sender, we interpret the operation as a local computation followed by a send and the continuation.

* If $l$ equals $r$ but not $s$, meaning the target location is the receiver, we interpret the operation as a receive followed by the continuation.

* If $l$ equals neither $s$ nor $r$, meaning the target location is not involved, we just return the continuation.

§ NEXT STEPS

[0]

Our next step will be to leverage the algebraic-effects-based formulation of CP presented in the last two sections to prove the correctness of endpoint projection, as well as follow-on properties such as deadlock freedom.

At a high level, given a choreographic semantics _⇒ᶜ_ and a network semantics _⇒ⁿ_, soundness of endpoint projection would say that the projected network preserves the semantics of the original choreography.

That is, for choreographies $c$ and $c'$,

[0]

Completeness of EPP, on the other hand, would say that the network reflects the semantics of the original choreography, that is, given choreographies $c$ and $c'$,

[0]

If these correctness conditions hold, the transition systems _⇒ᶜ_ and _⇒ⁿ_ are in bisimulation,

and if choreographies enjoy a progress property, networks also have it, implying that they are deadlock-free.

However, the above definitions of soundness and completeness may be too strong — for instance, they prohibit EPP from doing rewritings that change the behaviors of the network but compute the same result.

Thus, we are working on more relaxed correctness conditions that permit more interesting behaviors in networks while still maintaining deadlock freedom.

In the longer term, we want to bring our algebraic-effects-based formulation of CP to languages with efficient native support for algebraic effects, such as OCaml and Koka.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

authorpersonAndrej Bauer.
titleWhat is algebraic about algebraic effects and
[arxiv]1807.05923 [cs.LO]

[Cruz-Filipe et al(2022)]
authorpersonLuís Cruz-Filipe, personEva
Graversen, personLovro Lugović, personFabrizio
Montesi, and personMarco Peressotti.
Functional Choreographic Programming. In
booktitleTheoretical Aspects of Computing – ICTAC 2022:
19th International Colloquium, Tbilisi, Georgia, September 27–29, 2022,
Proceedings (Tbilisi, Georgia). publisherSpringer-Verlag,
addressBerlin, Heidelberg, pages212–237.

[Cruz-Filipe and Montesi(2020)]
authorpersonLuís Cruz-Filipe and
personFabrizio Montesi. year2020.
A core model for choreographic programming.
journalTheoretical Computer Science
volume802 (year2020), pages38–66.

[Giallorenzo et al(2024)]
authorpersonSaverio Giallorenzo,
personFabrizio Montesi, and personMarco
Peressotti. year2024.
Choral: Object-oriented Choreographic Programming.
journalACM Trans. Program. Lang. Syst.
volume46, number1, Article articleno1
(dateJan. year2024), numpages59 pages.

[Hirsch and Garg(2022)]
authorpersonAndrew K. Hirsch and
personDeepak Garg. year2022.
Pirouette: Higher-Order Typed Functional
volume6, numberPOPL, Article
articleno23 (dateJan. year2022),
numpages27 pages.

[Kashiwa et al(2023)]
authorpersonShun Kashiwa, personGan Shen,
personSoroush Zare, and personLindsey Kuper.
titlePortable, Efficient, and Practical Library-Level
Choreographic Programming.
[arxiv]2311.11472 [cs.PL]

[Kidney et al(2024)]
authorpersonDonnacha Oisín Kidney,
personZhixuan Yang, and personNicolas Wu.
Algebraic Effects Meet Hoare Logic in Cubical
journalProc. ACM Program. Lang.
volume8, numberPOPL, Article articleno56
(dateJan. year2024), numpages33 pages.

authorpersonDaan Leijen.
Type directed compilation of row-typed algebraic
effects. In booktitleProceedings of the 44th ACM SIGPLAN
Symposium on Principles of Programming Languages (Paris, France)
(seriesPOPL '17). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

authorpersonFabrizio Montesi.
titleChoreographic Programming.
thesistypePh. D. Dissertation. schoolIT
University of Copenhagen.

authorpersonFabrizio Montesi.
booktitleIntroduction to Choreographies.
publisherCambridge University Press.

[Plotkin and Power(2003)]
authorpersonGordon Plotkin and personJohn
Power. year2003.
Algebraic operations and generic effects.
journalApplied categorical structures
volume11 (year2003), pages69–94.

[Plotkin and Pretnar(2013)]
authorpersonGordon D Plotkin and
personMatija Pretnar. year2013.
Handling Algebraic Effects.
journalLogical Methods in Computer Science
volumeVolume 9, Issue 4 (dateDec.

[Shen et al(2023)]
authorpersonGan Shen, personShun Kashiwa,
and personLindsey Kuper. year2023.
HasChor: Functional Choreographic Programming for
All (Functional Pearl).
volume7, numberICFP, Article
articleno207 (dateAug. year2023),
numpages25 pages.

[Sivaramakrishnan et al(2021)]
authorpersonKC Sivaramakrishnan,
personStephen Dolan, personLeo White,
personTom Kelly, personSadiq Jaffer, and
personAnil Madhavapeddy. year2021.
Retrofitting effect handlers onto OCaml. In
booktitleProceedings of the 42nd ACM SIGPLAN International
Conference on Programming Language Design and Implementation (Virtual,
Canada) (seriesPLDI 2021). publisherAssociation
for Computing Machinery, addressNew York, NY, USA,

[Sivaramakrishnan et al(2018)]
authorpersonKC Sivaramakrishnan, personDaan
Leijen, personMatija Pretnar, and personTom
Schrijvers. year2018.
Algebraic Effect Handlers go Mainstream (Dagstuhl
Seminar 18172).
journalDagstuhl Reports volume8,
number4 (year2018), pages104–125.