Algebraic effects and handlers are a mechanism to structure programs with computational effects in a modular way. They are recently gaining popularity and being adopted in practical languages, such as OCaml. Meanwhile, there has been substantial progress in program verification via refinement type systems. However, thus far there has not been a satisfactory refinement type system for algebraic effects and handlers. In this paper, we fill the void by proposing a novel refinement type system for algebraic effects and handlers. The expressivity and usefulness of algebraic effects and handlers come from their ability to manipulate delimited continuations, but delimited continuations also complicate programs' control flow and make their verification harder. To address the complexity, we introduce a novel concept that we call answer refinement modification (ARM for short), which allows the refinement type system to precisely track what effects occur and in what order when a program is executed, and reflect such information as modifications to the refinements in the types of delimited continuations. We formalize our type system that supports ARM (as well as answer type modification, or ATM) and prove its soundness. Additionally, as a proof of concept, we have implemented a corresponding type checking and inference algorithm for a subset of OCaml 5, and evaluated it on a number of benchmark programs. The evaluation demonstrates that ARM is conceptually simple and practically useful. Finally, a natural alternative to directly reasoning about a program with delimited continuations is to apply a continuation passing style (CPS) transformation that transforms the program to a pure program. We investigate this alternative, and show that the approach is indeed possible by proposing a novel CPS transformation for algebraic effects and handlers that enjoys bidirectional (refinement-)type-preservation.

翻译：代数效应与处理器是一种以模块化方式组织带有计算效应的程序结构的机制。近年来，该机制日益受到关注，并已被应用于OCaml等实践性语言中。与此同时，通过精炼类型系统进行的程序验证也取得了重大进展。然而，迄今为止，尚未出现令人满意的用于代数效应与处理器的精炼类型系统。本文通过提出一种新颖的用于代数效应与处理器的精炼类型系统，填补了这一空白。代数效应与处理器的表达力和实用性源于其操控定界延续的能力，但定界延续也使程序的控制流复杂化，增加了验证难度。为应对这一复杂性，我们引入了一个称为“答案精炼修改”（简称ARM）的新概念，它使得精炼类型系统能够精确追踪程序执行时所发生的效应及其顺序，并将此类信息作为对定界延续类型中精炼的修改反映出来。我们对支持ARM（以及答案类型修改，即ATM）的类型系统进行了形式化描述，并证明了其正确性。此外，作为概念验证，我们针对OCaml 5的一个子集实现了相应的类型检查与推理算法，并在多个基准程序上进行了评估。评估结果表明，ARM在概念上简单且在实用中有效。最后，一种直接推理含定界延续程序的自然替代方案是应用续延传递风格（CPS）变换，将程序转化为纯程序。我们研究了这一替代方案，并通过提出一种新颖的、兼具双向（精炼）类型保持特性的代数效应与处理器CPS变换，证明了该方法的可行性。