Click here to flash read.
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.