Remarks on Algebraic Reconstruction of Types and Effects

TL;DR

This paper revisits the algebraic reconstruction algorithm for types and effects from 1991, identifying subtle bugs related to variable binding in higher-rank polymorphism, and discusses implications for static analysis systems.

Contribution

It critically analyzes the original algorithm, uncovers subtle bugs, and clarifies the challenges of implementing higher-rank polymorphism in type-and-effect systems.

Findings

Identified subtle bugs in the original algorithm.

Highlighted challenges of higher-rank polymorphism.

Provided insights for correct implementation.

Abstract

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.