一句话：提出答案精化修改（ARM）精化类型系统，可靠验证代数效应与处理程序。
代数效应与处理程序可模块化地组织计算效应，但定界续延使控制流复杂，现有精化类型系统难以令人满意地验证此类程序。本文提出答案精化修改（ARM），使精化类型系统能精确追踪程序执行时发生何种效应及顺序，并将这些信息反映为对定界续延类型中精化的修改。作者形式化支持 ARM（及答案类型修改 ATM）的类型系统，证明其可靠性；并将其扩展到 OCaml 5 子集，实现类型检查与推断算法，在多个基准程序上评估，表明 ARM 概念简单且实用。文章还研究了 CPS 变换替代方案，给出双向保持精化类型的新 CPS 变换，但指出其需源程序类型注解、推断类型信息较少等利弊。
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 . While a variety of refinement type systems have been proposed, 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 languages with 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 extended the refinement type system to a subset of OCaml 5 which comes with a built-in support for effect handlers, implemented a type checking and inference algorithm for the extension, and evaluated it on a number of benchmark programs that use algebraic effects and handlers. 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 without delimited continuations. We investigate this alternative in the paper, 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. We show that there are pros and cons with this approach, namely, while one can use an existing refinement type checking and inference algorithm that can only (directly) handle pure programs, there are issues such as needing type annotations in source programs and making the inferred types less informative to a user.
@article{paperbot2576,
title = {Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers},
author = {Fuga Kawamata and Hiroshi Unno and Taro Sekiyama and Tachio Terauchi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3633280}
}