Functional Choreographic Programming
Functional Choreographic Programming
复制标题
函数式编排编程
DOI：
10.1007/978-3-031-17715-6_15
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Marco Peressotti
中科院分区：
文献类型：
--
作者：
L. Cruz;Eva Graversen;Lovro Lugovi'c;F. Montesi;Marco Peressotti
编排编程是一种用于并发和分布式系统的新兴编程范例，开发人员编写应该执行的通信，然后通过编译器自动获得分布式实现。编排编程理论通常具有关于编译过程的强有力的理论保证，最值得注意的是：生成的实现在操作上与其源代码编排相对应，并且无死锁。目前，该范例的最高级化身是Chal，这是一种面向对象的编排编程语言，面向Java。合唱明显偏离了已知的编舞理论，并引入了表达完全分布的高阶编排(在编排上参数化的编排)的可能性。因此，尚不清楚通常对编舞的保证是否仍然适用于更一般的更高级别的编排。我们介绍了第一个函数式编排编程语言Chor{\lambda}：它引入了编排中作为函数的标准通信原语的新公式，并且它基于{\lambda}演算。Chor{\lambda}是第一个解释高阶编排编程核心思想的理论(就像在Chole中一样)。弥合实践和理论之间的差距需要开发一种新的评估策略，并为{\lambda}术语键入规则，以说明编排中计算的分布式性质。我们用一系列的例子来说明Chor{\lambda}的表现力，其中包括从最初的合唱演示中重构关键示例。我们的理论支持编排编程的预期属性，并弥合了函数式编程和编排编程社区之间的差距。
Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a distributed implementation is automatically obtained by means of a compiler. Theories of choreographic programming typically come with strong theoretical guarantees about the compilation process, most notably: the generated implementations operationally correspond to their source choreographies and are deadlock-free. Currently, the most advanced incarnation of the paradigm is Choral, an object-oriented choreographic programming language that targets Java. Choral deviated significantly from known theories of choreographies, and introduced the possibility of expressing higher-order choreographies (choreographies parameterised over choreographies) that are fully distributed. As a consequence, it is unclear if the usual guarantees of choreographies can still hold in the more general setting of higher-order ones. We introduce Chor{\lambda}, the first functional choreographic programming language: it introduces a new formulation of the standard communication primitive found in choreographies as a function, and it is based upon the {\lambda}-calculus. Chor{\lambda} is the first theory that explains the core ideas of higher-order choreographic programming (as in Choral). Bridging the gap between practice and theory requires developing a new evaluation strategy and typing discipline for {\lambda} terms that accounts for the distributed nature of computation in choreographies. We illustrate the expressivity of Chor{\lambda} with a series of examples, which include reconstructions of the key examples from the original presentation of Choral. Our theory supports the expected properties of choreographic programming and bridges the gap between the communities of functional and choreographic programming.