一句话:提出统一框架,用模态效应类型编码并比较基于行多态与基于能力的效应系统,证明编码保持类型与语义。
效应处理器支持模块化地建模与组合计算效应,效应系统静态保证效应均被处理。近期实用效应系统多基于行多态或能力,但二者基础迥异,其精确关系尚不清晰;难点在于效应追踪通常与函数等特性纠缠。本文提出统一框架,用于编码、分析和比较效应系统。该框架推广模态效应类型,用模态将效应追踪与函数解耦,可精细控制追踪时机与方式,表达不同追踪策略。作者给出从基于行和基于能力的系统到该框架的宏翻译编码,证明编码保持类型与语义。编码揭示不同效应追踪机制的本质,支持直接分析差异,并为语言设计提供洞见。
Effect handlers allow programmers to model and compose computational effects modularly. Effect systems statically guarantee that all effects are handled. Several recent practical effect systems are based on either row polymorphism or capabilities. However, there remains a gap in understanding the precise relationship between effect systems with such disparate foundations. The main difficulty is that in both row-based and capability-based systems, effect tracking is typically entangled with other features such as functions. We propose a uniform framework for encoding, analysing, and comparing effect systems. Our framework exploits and generalises modal effect types, a recent novel effect system which decouples effect tracking from functions via modalities. Modalities offer fine-grained control over when and how effects are tracked, enabling us to express different strategies for effect tracking. We give encodings as macro translations from existing row-based and capability-based effect systems into our framework and show that these encodings preserve types and semantics. Our encodings reveal the essence of effect tracking mechanisms in different effect systems, enable a direct analysis on their differences, and provide practical insights on language design.