一句话：提出渐近类型语言 GrEff，支持从未检查到已检查效应类型的渐进迁移，并证明其可靠性与 graduality 定理。
论文研究如何在已有带副作用但缺乏细粒度效应信息的类型语言中，渐进地引入效应类型。作者设计了表面语言 GrEff，并通过 elaboration 将其语义映射到核心语言 Core GrEff；核心语言配备不方程理论，用于刻画语义错误序以及效应与处理器程序所期望的等价关系，并由此导出操作语义。作者构造操作逻辑关系模型证明该理论的可靠性，进而证明 graduality 定理，保证从无检查到有检查效应类型迁移的安全性。该工作将先前 embedding-projection pair 的渐进类型模型扩展至效应类型与子类型，是对 Typed Racket 式渐进迁移编程模型的简化建模。
We present a gradually typed language, GrEff, with effects and handlers that supports migration from unchecked to checked effect typing. This serves as a simple model of the integration of an effect typing discipline with an existing effectful typed language that does not track fine-grained effect information. Our language supports a simple module system to model the programming model of gradual migration from unchecked to checked effect typing in the style of Typed Racket. The surface language GrEff is given semantics by elaboration to a core language Core GrEff. We equip Core GrEff with an inequational theory for reasoning about the semantic error ordering and desired program equivalences for programming with effects and handlers. We derive an operational semantics for the language from the equations provable in the theory. We then show that the theory is sound by constructing an operational logical relations model to prove the graduality theorem. This extends prior work on embedding-projection pair models of gradual typing to handle effect typing and subtyping.
@article{paperbot1861,
title = {Gradual Typing for Effect Handlers},
author = {Max S. New and Eric Giovannini and Daniel R. Licata},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622860}
}