Efficient, Portable, Census-Polymorphic Choreographic Programming

TL;DR

This work advances library-based choreographic programming by addressing three core challenges: efficient knowledge-of-choice (KoC) management, abstraction over the number of participants, and practical porting to diverse host languages. It introduces conclaves and multiply-located values (MLVs) to enable communication-efficient conditionals, and census polymorphism to parametrically express protocols over arbitrary participant sets. To realize these ideas across languages, the paper proposes endpoint projection as dependency injection (EPP-as-DI), enabling CP libraries in Haskell, Rust, and TypeScript with language-appropriate safety guarantees. Formal development includes a Conclaves-&-MLVs lambda calculus, proofs of soundness and deadlock-freedom, and expressivity comparisons with select-&-merge, complemented by real-language implementations and diverse case studies such as a census-polymorphic KV store, secure lottery, and MPC.Given the practical orientation and rigorous formalism, these contributions enable portable, scalable, and verifiably deadlock-free CP libraries for real distributed systems with variable sizes and heterogeneous language ecosystems.

Abstract

Choreographic programming (CP) is a paradigm for implementing distributed systems that uses a single global program to define the actions and interactions of all participants. Library-level CP implementations, like HasChor, integrate well with mainstream programming languages but have several limitations: Their conditionals require extra communication; they require specific host-language features (e.g., monads); and they lack support for programming patterns that are essential for implementing realistic distributed applications. We make three contributions to library-level CP to specifically address these challenges. First, we propose and formalize conclaves and multiply-located values, which enable efficient conditionals in library-level CP without redundant communication. Second, we propose end-point projection as dependency injection, a design pattern that enables library-level CP in host languages without support for monads. Third, we propose census polymorphism, a technique for abstracting over the number of participants in a choreography. We demonstrate these contributions via implementations in Haskell, Rust, and TypeScript.

Figures (23)

• Figure 1: A simple client-server interaction, written using the Has-Chor shen-haschor Haskell library.
• Figure 2: A choreography called [breaklines]haskellkvs written in Haskell using Multi-Chor, with its corresponding sequence diagram. An unspecified number of [breaklines]haskellservers maintain copies of a key-value-store, and a [breaklines]haskellclient makes a request against that store by communicating with the [breaklines]haskellprimary server. The first three arguments are proof-witness objects that identify the parties and prove they have the needed relationships. The forth argument [breaklines]haskellstateRefs is a faceted value containing the servers' individual copies of the [breaklines]haskellState, which could accidentally diverge during [breaklines]haskellupdateState operations. The fifth argument is the client's [breaklines]haskellrequest. Lines 20-21: [breaklines]haskellprimary receives the request and forwards it to all the other servers. Lines 22-35: The servers do work without the client; they all examine the request and, if it's a [breaklines]haskellPut request, update their local state. Line 28: [breaklines]haskellprimary will not proceed until it's received [breaklines]haskell_ack flags from all the other servers. Line 36: [breaklines]haskellprimary sends the response to [breaklines]haskellclient, who can skip ahead to line 52 and exit. Lines 39-51: If the store was updated by a [breaklines]haskellPut, then the servers compare hashes of their copies of the store (the actual comparison is done by [breaklines]haskellprimary on lines 45-47), and if necessary they enter the expensive process of re-syncing their copies.
• Figure 3: Selected rules and definitions from our formalism. (a) The complete syntax of $\boldsymbol{\lambda}_{\boldsymbol{C}}$ terms ($M$, $N$) and types ($T$). (b)TVar, TLambda, TCase, TInl, and TCom are representative of the thirteen total typing rules for $\boldsymbol{\lambda}_{\boldsymbol{C}}$. (c)$⟦\cdot⟧_p$ is EPP from $\boldsymbol{\lambda}_{\boldsymbol{C}}$ to $\boldsymbol{\lambda}_{\boldsymbol{L}}$, parameterized by $p$; here we show only its definition for the communication operator. (d)$\boldsymbol{\lambda}_{\boldsymbol{L}}$ is untyped; LAbsApp, LSend1, and LRecv are representative of its fifteen total semantics rules. NPro, NCom, and NPar are the complete semantics rules for $\boldsymbol{\lambda}_{\boldsymbol{N}}$. Appendix \ref{['sec:more-formalism']} explains all of these systems and their relationships in detail.
• Figure 4: The fundamental operators for writing expressions in Multi-Chor's [breaklines]haskellChoreo monad. Of these four operators, [breaklines]haskellconclave is the only one users will usually call directly; the other three can combine with each other (and with [breaklines]haskellconclave) to make more user-friendly alternatives.
• Figure 5: The definition of choreography in ChoreoTS. The choreographic operators are defined as aliases for function types, and these all get packaged together in a record type [breaklines]typescriptDependencies. A [breaklines]typescriptChoreography is a function from a [breaklines]typescriptDependencies (and any other arguments) to some return value. In order to create a [breaklines]typescriptDependencies, it must have real implementations of each of the operator functions, most of which have additional type parameters. [breaklines]typescriptepp builds a such an object implementing the behavior of each operation for the target party, and passes that object to the choreography function.

Theorems & Definitions (30)

• definition : Census
• definition : Conclave
• definition : Multiply located value (MLV)
• definition : Census polymorphism
• definition : Faceted value
• definition : Quire
• Corollary 1: Deadlock Freedom
• Corollary 2: Deadlock Freedom
• Lemma 1: Conclave
• Lemma 2: Quorum