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 the 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) 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（以及答案类型修正）的类型系统，并证明了其可靠性。此外，作为概念验证，我们针对OCaml 5的一个子集实现了相应的类型检查与推断算法，并在多个基准程序上进行了评估。评估结果表明，ARM既概念简洁又具备实用价值。最后，直接推理含受限续延程序的一种自然替代方案是应用续延传递风格（CPS）变换，将程序转换为纯程序。我们对此替代方案进行了研究，并针对代数效应与处理器提出了一种新型的双向（细化）类型保持的CPS变换，证明了该方案的可行性。