Alice or Bob?: Process polymorphism in choreographies

Abstract

We present PolyChor\(\lambda\), a language for higher-order functional choreographic programming—an emerging paradigm for concurrent programming. In choreographic programming, programmers write the desired cooperative behaviour of a system of processes and then compile it into an implementation for each process, a translation called endpoint projection. Unlike its predecessor, Chor\(\lambda\), PolyChor\(\lambda\) has both type and 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 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 programmes are deadlock-free by design.