In their 1991 paper "Algebraic Reconstruction of Types and Effects," Pierre Jouvelot and David Gifford presented a type-and-effect reconstruction algorithm based on an algebraic structure of effects. Their work is considered a milestone in the development of type-and-effect systems, and has inspired numerous subsequent works in the area of static analysis. However, unlike the later research it spawned, the original algorithm considered a language with higher-rank polymorphism, a feature which is challenging to implement correctly. In this note, we identify subtle bugs related to variable binding in their approach to this feature. We revisit their type system and reconstruction algorithm, and describe the discovered issues.
翻译:在1991年的论文《类型与效应的代数重构》中,Pierre Jouvelot与David Gifford提出了一种基于效应代数结构的类型与效应重构算法。该工作被视为类型与效应系统发展史上的里程碑,对静态分析领域的后续研究产生了深远影响。然而,与受其启发的后续研究不同,原始算法所处理的语言包含高阶多态性——这一特性在正确实现上存在显著挑战。本文指出该算法在处理此特性时涉及变量绑定的若干微妙缺陷。我们重新审视其类型系统与重构算法,并对所发现的问题进行详细阐述。