一句话：提出显式类型化、带子类型与强制转换的代数效应处理器核心演算及约束推断算法。
随着代数效应与处理器日益流行，如何高效执行它们成为重要问题。Eff 是原生支持处理器的 ML 风格语言，其基于子类型的效应系统可用于构建效应感知优化编译器，但其核心语言是隐式类型的，导致程序变换脆弱且易错。本文提出一个显式类型化的多态核心演算，支持代数效应处理器与基于子类型的类型-效应系统；该演算将子类型调用具体化为带 coercion 的显式 cast，从而快速暴露程序变换中的类型错误。作者给出类型导向的 elaboration 与基于约束的推断算法，可将隐式类型的 Eff 风格语言转换为该演算。此外，所有 coercion 与效应信息均可直接擦除，表明 coercion 没有计算内容；并给出到无代数效应/处理器的纯语言的 monadic translation，仅在必要时引入 monadic 构造。
Abstract As popularity of algebraic effects and handlers increases, so does a demand for their efficient execution. Eff, an ML-like language with native support for handlers, has a subtyping-based effect system on which an effect-aware optimising compiler could be built. Unfortunately, in our experience, implementing optimisations for Eff is overly error-prone because its core language is implicitly typed, making code transformations very fragile. To remedy this, we present an explicitly typed polymorphic core calculus for algebraic effect handlers with a subtyping-based type-and-effect system. It reifies appeals to subtyping in explicit casts with coercions that witness the subtyping proof, quickly exposing typing bugs in program transformations. Our typing-directed elaboration comes with a constraint-based inference algorithm that turns an implicitly typed Eff-like language into our calculus. Moreover, all coercions and effect information can be erased in a straightforward way, demonstrating that coercions have no computational content. Additionally, we present a monadic translation from our calculus into a pure language without algebraic effects or handlers, using the effect information to introduce monadic constructs only where necessary.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{SalehKPS18,
title = {Explicit effect subtyping},
author = {GEORGIOS KARACHALIAS and MATIJA PRETNAR and AMR HANY SALEH and STIEN VANDERHALLEN and TOM SCHRIJVERS},
journal = {Journal of Functional Programming},
volume = {30},
year = {2020},
doi = {10.1017/s0956796820000131}
}