Choreographic programming is a programming paradigm, whereby the overall behaviour of a distributed system is coded as a choreography from a global viewpoint. The choreography can then be automatically compiled (projected) to a correct implementation for each participant. Choreographic programming relieves the programmer from manually writing the separate send and receive actions performed by participants and avoids the problem of communication mismatches. However, the applicability of this paradigm in the real world remains largely unexplored for two reasons. First, while there have been several proposals of choreographic programming languages, none of them have been used to implement a realistic, widely-used protocol. Thus there is a lack of experience on how realistic choreographic programs are structured and on the relevance of the features explored in theoretical models. Second, applications of choreographic programming shown so far are intrusive since each participant must use exactly the code projected from the choreography. This prevents using the projected code with existing third-party implementations of some participants. We carry out the first development in choreographic programming of a widespread real-world protocol: the Internet Relay Chat (IRC) protocol. Our development is based on Choral, an object-oriented choreographic programming language. Two of Choral's features are key to our implementation: higher-order choreographies for modelling the complex interaction patterns due to IRC's asynchronous nature; and user-definable communication semantics for achieving interoperability with third-party implementations. We also discover a missing piece: the capability of statically detecting that choices on alternative distributed behaviours are appropriately communicated by means of message types. We extend the Choral compiler with an elegant solution based on subtyping.

翻译：编舞编程是一种编程范式，其中分布式系统的整体行为从全局视角被编码为编排（编舞）。该编舞随后可自动编译（投影）为每个参与者的正确实现。编舞编程免除了程序员手动编写参与者之间独立的发送和接收操作，并避免了通信不匹配的问题。然而，该范式在现实世界中的适用性因两个原因而基本未得到探索：第一，尽管已有多种编舞编程语言的提案，但尚无一种被用于实现实际的、广泛使用的协议。因此，缺乏关于实际编舞程序如何构建以及理论模型中探索的特性相关性的经验；第二，目前展示的编舞编程应用具有侵入性，因为每个参与者必须完全使用由编舞投影生成的代码。这阻碍了将投影代码与某些参与者的现有第三方实现集成使用。我们首次在编舞编程中开发了一个广泛使用的现实世界协议：互联网中继聊天（IRC）协议。我们的开发基于面向对象的编舞编程语言Choral。Choral的两个特性对我们的实现至关重要：用于建模IRC异步特性导致的复杂交互模式的高阶编舞；以及用于实现与第三方实现互操作性的用户自定义通信语义。我们还发现一个缺失环节：能够静态检测到替代分布式行为的选择是否通过消息类型被适当通信的能力。我们基于子类型化，为Choral编译器扩展了一个优雅的解决方案。