We describe a new concrete approach to giving predictable error locations for sequential (flow-sensitive) effect systems. Prior implementations of sequential effect systems rely on either computing a bottom-up effect and comparing it to a declaration (e.g., method annotation) or leaning on constraint-based type inference. These approaches do not necessarily report program locations that precisely indicate where a program may "go wrong" at runtime. Instead of relying on constraint solving, we draw on the notion of a residual from literature on ordered algebraic structures. Applying these to effect quantales (a large class of sequential effect systems) yields an implementation approach which accepts exactly the same program as an original effect quantale, but for effect-incorrect programs is guaranteed to fail type-checking with predictable error locations tied to evaluation order. We have implemented this idea in a generic effect system implementation framework for Java, and report on experiences applying effect systems from the literature and novel effect systems to Java programs. We find that the reported error locations with our technique are significantly closer to the program points that lead to failed effect checks.

翻译：我们描述了一种新的具体方法，用于为顺序（流敏感）效应系统提供可预测的错误位置。先前的顺序效应系统实现要么依赖于计算自底向上的效应并与声明（例如，方法注解）进行比较，要么依赖基于约束的类型推断。这些方法并不一定能报告精确指示程序可能在运行时“出错”位置的程序位置。我们不依赖约束求解，而是借鉴了有序代数结构文献中的“残差”概念。将这些概念应用于效应量子（一大类顺序效应系统）产生了一种实现方法，该方法接受的程序与原始效应量子完全相同，但对于效应不正确的程序，保证以与求值顺序相关的可预测错误位置导致类型检查失败。我们已在 Java 的通用效应系统实现框架中实现了这一思想，并报告了将文献中的效应系统及新型效应系统应用于 Java 程序的经验。我们发现，使用我们的技术报告的错误位置显著更接近导致效应检查失败的程序点。