标题： 不做出决定：在存在高阶多态性情况下的有效推理的正确和完整 显示英文标题

标题： Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism

摘要： 类型和效果系统帮助程序员在程序中组织数据和计算效果。 虽然传统的类型系统已经开发出具有丰富表达能力的变体，并且在编程语言中得到了广泛使用，但类型和效果系统尚未获得广泛的采用。 原因之一是类型和效果系统更加复杂，现有的推断算法在表达能力、直观性和可判定性之间做出了妥协。 在本工作中，我们提出了一种针对具有子类型、丰富的高阶多态性和直观的类似集合的效果语义的类型和效果系统的效应推断算法。 为了处理高阶多态性的作用域问题，我们将效应约束的求解延迟，将其转换为命题逻辑的公式。 我们证明了我们的算法相对于一个声明式的类型和效果系统是正确和完整的。 所有呈现的结果已经在Rocq证明助手中有形式化表示，该算法已在一种现实的编程语言中成功实现。 显示英文摘要

摘要： 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.