Alice or Bob?: Process Polymorphism in Choreographies

We present PolyChor\(\lambda\), a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour of a system of communicating processes and then compile it into distributed implementations for each process, a...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2023-03
Main Authors: Graversen, Eva, Hirsch, Andrew K, Montesi, Fabrizio
Format: Article
Language:English
Subjects:
Communication
Polymorphism
Programmers
Semantics
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present PolyChor\(\lambda\), a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour of a system of communicating processes and then compile it into distributed implementations for each process, a translation called \emph{endpoint projection}. Unlike its predecessor, Chor\(\lambda\), PolyChor\(\lambda\) has both type and \emph{process} polymorphism inspired by System F\(_\omega\). That is, PolyChor\(\lambda\) is the first (higher-order) functional choreographic language which gives programmers the ability to write generic choreographies and determine the participants at runtime. This novel combination of features also allows PolyChor\(\lambda\) processes to communicate \emph{distributed values}, leading to a new and intuitive way to write delegation. While some of the functional features of PolyChor\(\lambda\) give it a weaker correspondence between the semantics of choreographies and their endpoint-projected concurrent systems than some other choreographic languages, we still get the hallmark end result of choreographic programming: projected programs are deadlock-free by design.
ISSN:2331-8422