一句话：提出多态效应演算中显式子类型强制转换的化简方法，消除编译开销并证明语义保持。
代数效应处理器越来越流行，但其性能常受编译方式影响。已有高效编译方法通过显式子类型强制转换跟踪效应信息，然而在多态存在时，这些强制转换会被编译为函数的额外参数，带来显著开销。本文提出一个带效应的多态演算，识别并定义必要的化简阶段，以减少不必要的约束，同时证明这些化简保持语义。作者在 Eff 语言中实现了该化简算法，并在若干基准程序上进行性能评估。结果表明，该算法能够消除所有强制转换，使生成代码与手工单态化版本一样高效；不过文中并未证明所提化简的最优性。
Algebraic effect handlers are becoming an increasingly popular way of structuring effectful computations, and their performance is often a concern. One of the proposed approaches towards efficient compilation is tracking effect information through explicit subtyping coercions. However, in the presence of polymorphism, these coercions are compiled into additional arguments of compiled functions, incurring significant overhead. In this paper, we present a polymorphic effectful calculus, identify simplification phases needed to reduce the number of unnecessary constraints, and prove that they preserve semantics. In addition, we implement the simplification algorithm in the Eff language and evaluate its performance on a number of benchmarks. Though we do not prove the optimality of the presented simplifications, the results show that the algorithm eliminates all coercions, resulting in code as efficient as manually monomorphised one.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2404-04218,
title = {Simplifying explicit subtyping coercions in a polymorphic calculus with effects},
author = {Filip Koprivec and Matija Pretnar},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:25)2025}
}