答案改进修正：代数效应与处理器的细化类型系统
摘要：代数效应和处理程序是一种以模块化方式构建具有计算效应的程序的机制。它们最近在实际语言（如OCaml）中越来越受欢迎并被采用。与此同时，通过细化类型系统进行程序验证取得了实质性进展。然而，迄今为止，尚未有一个令人满意的适用于代数效应和处理程序的细化类型系统。本文通过提出一种新颖的代数效应和处理程序细化类型系统来填补这个空白。代数效应和处理程序的表达能力和实用性来源于它们能够操作被界定的延续，但界定的延续也使程序的控制流复杂化并增加了其验证的难度。为了解决这个复杂性，我们引入了一个我们称之为答案细化修饰（ARM）的新概念，它允许细化类型系统在程序执行时精确追踪发生的效应及其顺序，并将这些信息反映在被界定的延续类型的细化中。我们形式化了支持ARM的类型系统（以及答案类型修饰）并证明了其正确性。另外，作为一个概念证明，我们还针对OCaml的一个子集实现了相应的类型检查和推断算法，并在一些基准程序上进行了评估。评估表明，ARM在概念上简单且实用。最后，一个直接推理具有界定的延续程序的自然替代方法是应用一个延续传递风格（CPS）转换将程序转变为纯粹的程序。我们研究了这种替代方案，并提出了一种新颖的代数效应和处理程序的CPS转换，该转换享有双向（细化）类型保持性。
作者：Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi
论文ID：2307.15463
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-31