一句话：提出 PolyChorλ，首个支持类型与进程多态的高阶函数式编排语言，可在运行时确定参与者并保持投影程序无死锁。
本文提出 PolyChorλ，一种面向高阶函数式编排编程（choreographic programming）的语言。编排编程要求程序员描述多个进程的协作行为，再通过端点投影（endpoint projection）为每个进程生成实现。PolyChorλ 在 Chorλ 基础上引入受 System Fω 启发的类型多态与进程多态，是首个支持泛型编排并在运行时决定参与进程的高阶函数式编排语言。该组合还允许进程之间通信分布式值，从而以直观方式表达委托（delegation）。虽然其函数式特性使编排语义与端点投影后并发系统之间的对应关系弱于某些编排语言，但仍保持编排编程的标志性结果：投影所得程序在设计上无死锁。
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.
@article{paperbot2688,
title = {Alice or Bob?: Process polymorphism in choreographies},
author = {EVA GRAVERSEN and ANDREW K. HIRSCH and FABRIZIO MONTESI},
journal = {Journal of Functional Programming},
volume = {34},
year = {2024},
doi = {10.1017/s0956796823000114}
}