抽象代数效应处理器的效应系统

许多针对代数效应处理器的效应系统都旨在保证所有被调用的效应都得到恰当的处理。然而,各位研究人员已发展出自己的效应系统,其在表示可能发生的效应集合方式上存在差异。这种情况导致对效应集合的表示与操作在安全效应系统中的要求变得模糊不清。本文提出一种语言 ${\lambda_{\mathrm{EA}}}$ ，其配备抽象现有代数效应处理器效应系统的效应系统。 ${\lambda_{\mathrm{EA}}}$ 的效应系统可参数化于效应代数,该代数抽象了安全效应系统中效应集合表示与操作。我们通过假设给定的效应代数满足称为安全条件的若干属性,来证明 ${\lambda_{\mathrm{EA}}}$ 的类型与效应安全性。因此,我们可通过证明对应具体效应系统的效应代数满足安全条件,从而获得该具体效应系统的安全属性。我们还展示,满足安全条件的效应代数足够表达,能够容纳一些表示效应集合方式各不相同的现有效应系统。我们的框架还能区分现有效应系统中效应集合的安全方面。为此,我们扩展 ${\lambda_{\mathrm{EA}}}$ 和安全条件,以提升 coercions 与类型擦除语义。我们还提出其他效应代数,其中一些在文献中尚未有人研究。我们比较哪些效应代数是安全的,哪些则不安全，以适用于这些扩展。