有范围效应和处理程序的微积分
摘要：代数效应和处理器已经成为函数式编程中处理副作用的标准方法。它们可以与其他效应进行模块化组合，并且可以清晰地将语法和语义分离，这使它们对广大受众非常有吸引力。然而，并不是所有的效应都可以被归类为代数性的，有些需要更复杂的处理。特别是，具有或创建限定作用域的效应需要特别注意，因为它们的延续由作用域内外两部分组成，而模块化组合引入了额外的复杂性。这些效应被称为有范围的效应，并且因其在流行库中的适用性和应用广泛而受到关注。虽然已经设计了带有内置代数效应和处理器的演算，以便促进其使用，但尚不存在支持有范围效应和处理器的类似演算。本文填补了这个空白：我们提出了$lambda\_{mathit{sc}}$，一种同时对代数效应和有范围效应和处理器提供原生支持的演算。它解决了多态处理器和将未知有范围操作转发给其他处理器的需求。我们的演算基于已有的代数效应演算Eff，并扩展了Koka风格的行多态性，包括形式化语法、操作语义、（类型安全的）类型和效应系统以及类型推断。我们在一系列示例上演示了$lambda\_{mathit{sc}}$的应用。
作者：Roger Bosman, Birthe van den Berg, Wenhao Tang, Tom Schrijvers
论文ID：2304.09697
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-24