Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Patrycja Balik, Szymon Jędras, Piotr Polesiuk

TL;DR

The paper tackles inferring effects in programs with higher-rank polymorphism and set-like effects, addressing ergonomics, expressiveness, and decidability. It introduces a sound and complete two-stage effect reconstruction algorithm that delays solving certain constraints using algebraic type schemes, effect guards, and extraction of propositional formulas, with formal verification in Rocq and a practical implementation in the Fram language. Key contributions include extending effect inference to System F-like polymorphism, proving soundness and completeness with respect to the declarative type-and-effect system, and demonstrating practicality through formalization and integration in a realistic language. The work enables ergonomic, expressive effect systems with reliable inference in real-world languages, paving the way for broader adoption of type-and-effect approaches.

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.

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

TL;DR

The paper tackles inferring effects in programs with higher-rank polymorphism and set-like effects, addressing ergonomics, expressiveness, and decidability. It introduces a sound and complete two-stage effect reconstruction algorithm that delays solving certain constraints using algebraic type schemes, effect guards, and extraction of propositional formulas, with formal verification in Rocq and a practical implementation in the Fram language. Key contributions include extending effect inference to System F-like polymorphism, proving soundness and completeness with respect to the declarative type-and-effect system, and demonstrating practicality through formalization and integration in a realistic language. The work enables ergonomic, expressive effect systems with reliable inference in real-world languages, paving the way for broader adoption of type-and-effect approaches.

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.
Paper Structure (16 sections, 2 theorems, 3 equations, 6 figures)

This paper contains 16 sections, 2 theorems, 3 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Simplified Setting
  3. Syntax
  4. Scopes and Substitutions
  5. Declarative Type System
  6. Type and effect matching.
  7. Constraints, subeffecting, and subtyping.
  8. Type schemes.
  9. Typing relation.
  10. Algorithmic Effect Inference
  11. Type and effect matching.
  12. Constraints, subeffecting, and subtyping.
  13. The algorithm.
  14. Effect Inference with Higher-Rank Polymorphism
  15. Higher-rank polymorphism.
  16. ...and 1 more sections

Key Result

theorem thmcountertheorem

For the expression $e$ defined over the set of type variables $\Delta$, if $infer(\Gamma;\;e) = (\Delta' ;\;\tau ;\;\varepsilon ;\;\Omega)$, then $\Delta,\Delta'; \Omega; \Gamma \vdash e : \tau \mathrel{/} \varepsilon$.

Figures (6)

  • Figure 1: The syntax of the simplified calculus.
  • Figure 2: Type and effect matching.
  • Figure 3: Typing relation.
  • Figure 4: Translation of syntactic effects.
  • Figure 5: The effect inference algorithm for the simplified problem.
  • ...and 1 more figures

Theorems & Definitions (3)

  • remark thmcounterremark
  • theorem thmcountertheorem: Soundness
  • theorem thmcountertheorem: Completeness