We propose a novel type system for effects and handlers using modal types. Conventional effect systems attach effects to function types, which can lead to verbose effect-polymorphic types, especially for higher-order functions. Our modal effect system provides succinct types for higher-order first-class functions without losing modularity and reusability. The core idea is to decouple effects from function types and instead to track effects through relative and absolute modalities, which represent transformations on the ambient effects provided by the context. We formalise the idea of modal effect types in a multimodal System F-style core calculus Met with effects and handlers. Met supports modular effectful programming via modalities without relying on effect variables. We encode a practical fragment of a conventional row-based effect system with effect polymorphism, which captures most common use-cases, into Met in order to formally demonstrate the expressive power of modal effect types. To recover the full power of conventional effect systems beyond this fragment, we seamlessly extend Met to Mete with effect variables. We propose a surface language Metel for Mete with a sound and complete type inference algorithm inspired by FreezeML.

翻译：我们提出了一种基于模态类型的新型效应与处理器类型系统。传统效应系统将效应附加于函数类型，这可能导致冗长的效应多态类型，尤其对于高阶函数而言。我们的模态效应系统为高阶一等函数提供了简洁的类型，同时不丧失模块化与可复用性。其核心思想是将效应从函数类型中解耦，转而通过相对与绝对模态来追踪效应，这些模态表示对上下文所提供的环境效应进行的变换。我们将模态效应类型的思想形式化为一个多模态的System F风格核心演算Met，该演算支持效应与处理器。Met通过模态支持模块化的效应式编程，而无需依赖效应变量。我们将一个具有效应多态性的传统基于行的效应系统的实用片段编码到Met中，该片段覆盖了大多数常见用例，以此形式化地证明模态效应类型的表达能力。为了恢复传统效应系统在此片段之外的完整能力，我们将Met无缝扩展为具有效应变量的Mete。我们为Mete提出了一种表层语言Metel，并设计了一个受FreezeML启发的、健全且完备的类型推断算法。