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.
Wed 15 OctDisplayed time zone: Perth change
10:50 - 12:05 | |||
10:50 25mTalk | Fusing Session-Typed Concurrent Programming into Functional Programming ICFP Papers Chuta Sano McGill University, Deepak Garg MPI-SWS, Ryan Kavanagh Université du Québec à Montréal, Brigitte Pientka McGill University, Bernardo Toninho Instituto Superior Técnico - University of Lisbon DOI | ||
11:15 25mTalk | Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs ICFP Papers Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Philipp G. Haselwarter Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University DOI Pre-print | ||
11:40 25mTalk | Relax! The Semilenient Core of Choreographic Programming (Functional Pearl) ICFP Papers Dan Plyukhin University of Southern Denmark, Xueying Qin University of Southern Denmark, Fabrizio Montesi University of Southern Denmark DOI Pre-print | ||