Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
The past few years have seen a surge of interest in choreographic programming, a programming paradigm for concurrent and distributed systems. The paradigm allows programmers to implement a distributed interaction protocol with a single high-level program, called a \emph{choreography}, and then mechanically \emph{project} it into correct implementations of its participating processes. A choreography can be expressed as a $\lambda$-term parameterized by constructors for creating data ``at'' a process and for communicating data between processes. Through this lens, recent work has shown how one can add choreographies to mainstream languages like Java, or even embed choreographies as a DSL in languages like Haskell and Rust. These new choreographic languages allow programmers to write in applicative style (like in functional programming) and write higher-order choreographies for better modularity. But the semantics of functional choreographic languages is not well-understood. Whereas typical $\lambda$-calculi can have their operational semantics defined with just a few rules, existing models for \emph{choreographic} $\lambda$-calculi have \emph{dozens} of complex rules and \emph{no clear or agreed-upon evaluation strategy}.
We show that functional choreographic programming is simple. Beginning with the Chor$\lambda$ model from previous work, we strip away inessential features to produce a ``core'' model called $\lambda^\chi$. We discover that underneath Chor$\lambda$'s apparently ad-hoc semantics lies a close connection to non-strict $\lambda$-calculi; we call the resulting evaluation strategy \emph{semilenient}. Then, inspired by previous non-strict calculi, we develop a notion of \emph{choreographic evaluation contexts} and a special \emph{commute} rule to simplify and explain the unusual semantics of functional choreographic languages. The extra structure leads us to a presentation of $\lambda^\chi$ with just ten rules, and a discovery of three missing rules in previous presentations of Chor$\lambda$. We also show how the extra structure comes with nice properties, which we use to simplify the correspondence proof between choreographies and their projections. Our model serves as both a principled foundation for functional choreographic languages and a good entry point for newcomers.