Efficient, Portable, Census-Polymorphic Choreographic Programming

TL;DR

This paper introduces new techniques for choreographic programming that improve efficiency, portability, and flexibility across different programming languages and distributed system configurations.

Contribution

It formalizes conclaves and multiply-located values, introduces endpoint projection as dependency injection, and proposes census polymorphism for flexible participant management.

Findings

Efficient conditionals without extra communication

Host-language agnostic library-level CP implementation

Support for dynamic participant counts in distributed systems

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.