Type-and-effect systems help the programmer to organize data and computational effects in a program. While for traditional type systems expressive variants with sophisticated inference algorithms have been developed and widely used in programming languages, type-and-effect systems did not yet gain widespread adoption. One reason for this is that type-and-effect systems are more complex and the existing inference algorithms make compromises between expressiveness, intuitiveness, and decidability. In this work, we present an effect inference algorithm for a type-and-effect system with subtyping, expressive higher-rank polymorphism, and intuitive set-like semantics of effects. In order to deal with scoping issues of higher-rank polymorphism, we delay solving of effect constraints by transforming them into formulae of propositional logic. We prove soundness and completeness of our algorithm with respect to a declarative type-and-effect system. All the presented results have been formalized in the Rocq proof assistant, and the algorithm has been successfully implemented in a realistic programming language.

翻译：类型与效应系统帮助程序员组织程序中的数据与计算效应。尽管针对传统类型系统已发展出具有复杂推断算法的表达性变体并在编程语言中得到广泛应用，类型与效应系统尚未获得广泛采纳。其原因之一是类型与效应系统更为复杂，现有推断算法往往在表达性、直观性与可判定性之间做出妥协。本研究提出一种适用于包含子类型化、表达性高阶多态性及直观集合式效应语义的类型与效应系统的效应推断算法。为处理高阶多态性的作用域问题，我们通过将效应约束转化为命题逻辑公式来延迟求解过程。我们证明了该算法相对于声明式类型与效应系统的可靠性与完备性。所有研究成果已在Rocq证明助手中形式化验证，且该算法已成功应用于实际编程语言中。