顺序和并行程序的直接式效果表示
摘要：用于模拟顺序和并行组合的效应计算模型在多种编程语言中已经被研究了很长一段时间。特别是，流行的do-notation为任何monad的实例提供了一种轻量级的效应嵌入方法。另一方面，idiom bracket notation为applicative提供了一种嵌入方法。首先，尽管monad强制效应以顺序方式执行，忽略了并行性的潜力，但applicative不支持顺序效应。组合顺序和并行效应仍然是一个未解决的问题。这是个更大的问题，因为真实的程序由顺序和并行两个部分组成。其次，常见的表示方法不支持直接调用效应，而是将一种严格的结构强加于代码。 在本文中，我们提出了一种混合的applicative/monadic表示方法，可以尽可能地保留并行性，同时在必要时允许顺序。我们利用一种直接表示法，其中顺序性或并行性是从代码的结构中衍生出来的。我们在Coq中提供了对我们的效应语言的机械化，并证明了我们的编译方法保留了源程序的并行性。
作者：David Richter, Timon B"ohler, Pascal Weisenburger, Mira Mezini
论文ID：2305.08496
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-05-22