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.

翻译：我们提出了一个带有效应和处理器的渐进类型语言GrEff，支持从非检查型到检查型效应类型的迁移。这为将效应类型规范与现有效应类型化语言（不追踪细粒度效应信息）的整合提供了一个简单模型。该语言采用简易模块系统模拟Typed Racket风格的编程模型，支持从非检查型到检查型效应类型的渐进迁移。表层语言GrEff通过精化到核心语言Core GrEff获得语义。我们为Core GrEff建立了不等式理论，用于推理关于效应与处理器编程的语义错误排序及预期程序等价性。从该理论可证明的方程出发，推导出语言的操作语义。进而通过构建操作逻辑关系模型证明渐进性定理，验证该理论的可靠性。这扩展了此前基于嵌入-投影对模型的渐进类型研究，使其能够处理效应类型与子类型。