Expansion for Universal Quantifiers

TL;DR

This paper extends the concept of expansion in type systems to include forall-quantifiers, presenting System Fs which integrates expansion with System F, transforming type inference into a constraint solving problem.

Contribution

It introduces System Fs, an extension of System F with expansion, and proves its main properties, enabling modular type inference via constraint solving.

Findings

System Fs extends expansion to forall-quantifiers.

Type inference is transformed into a constraint solving problem.

Main properties of System Fs are formally proven.

Abstract

Expansion is an operation on typings (i.e., pairs of typing environments and result types) defined originally in type systems for the lambda-calculus with intersection types in order to obtain principal (i.e., most informative, strongest) typings. In a type inference scenario, expansion allows postponing choices for whether and how to use non-syntax-driven typing rules (e.g., intersection introduction) until enough information has been gathered to make the right decision. Furthermore, these choices can be equivalent to inserting uses of such typing rules at deeply nested positions in a typing derivation, without needing to actually inspect or modify (or even have) the typing derivation. Expansion has in recent years become simpler due to the use of expansion variables (e.g., in System E). This paper extends expansion and expansion variables to systems with forall-quantifiers. We present System Fs, an extension of System F with expansion, and prove its main properties. This system turns type inference into a constraint solving problem; this could be helpful to design a modular type inference algorithm for System F types in the future.