一句话：提出支持效应排他的类型与效应系统，可直接表达“除指定效应外皆可”的函数，并在 Flix 中实现。
现有类型与效应系统只能间接推理“效应缺失”，而效应多态让函数签名可抽象任意未知效应集，增加了难度。本文提出一种新的类型与效应系统，支持效应多态以及并、交、补效应，并将“效应排除”作为一类新的效应多态函数：允许除指定集合外的任意效应，从而直接推理效应缺失。系统基于 Hindley-Milner，保持主类型（模布尔等价），并通过在集合代数上用布尔合一扩展 Algorithm W，实现完备的类型与效应推断。作者在 λ∁ 演算中形式化，证明 progress、preservation 及效应安全定理：被排除效应永不被执行；并将系统实现为 Flix 扩展。案例研究在开源项目中识别出 59 段需效应排除方可保证正确性的代码，并用该扩展重写。
Type and effect systems have been successfully used to statically reason about effects in many different domains, including region-based memory management, exceptions, and algebraic effects and handlers. Such systems’ soundness is often stated in terms of the absence of effects. Yet, existing systems only admit indirect reasoning about the absence of effects. This is further complicated by effect polymorphism which allows function signatures to abstract over arbitrary, unknown sets of effects. We present a new type and effect system with effect polymorphism as well as union, intersection, and complement effects. The effect system allows us to express effect exclusion as a new class of effect polymorphic functions: those that permit any effects except those in a specific set. This way, we equip programmers with the means to directly reason about the absence of effects. Our type and effect system builds on the Hindley-Milner type system, supports effect polymorphism, and preserves principal types modulo Boolean equivalence. In addition, a suitable extension of Algorithm W with Boolean unification on the algebra of sets enables complete type and effect inference. We formalize these notions in the λ ∁ calculus. We prove the standard progress and preservation theorems as well as a non-standard effect safety theorem: no excluded effect is ever performed. We implement the type and effect system as an extension of the Flix programming language. We conduct a case study of open source projects identifying 59 program fragments that require effect exclusion for correctness. To demonstrate the usefulness of the proposed type and effect system, we recast these program fragments into our extension of Flix.
@article{paperbot1900,
title = {With or Without You: Programming with Effect Exclusion},
author = {Matthew Lutze and Magnus Madsen and Philipp Schuster and Jonathan Immanuel Brachthäuser},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607846}
}