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

TL;DR

This paper introduces a sound and complete effect inference algorithm for a sophisticated type-and-effect system featuring higher-rank polymorphism and subtyping, addressing complexity and decidability issues in effect inference.

Contribution

It presents a novel effect inference algorithm that handles higher-rank polymorphism and subtyping with a set-like effect semantics, formalized and implemented in a practical language.

Findings

Proves soundness and completeness of the inference algorithm.

Successfully formalized in Rocq proof assistant.

Implemented in a realistic programming language.

Abstract

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.