Type Inference for Rank-2 Intersection Types Using Set Unification

• Type: Article in International Conference Proceedings Book
• Date: 2022

Authors

Ângelo, P (Author) Other; Florido, M (Author) FCUP

Conference proceedings International

Title: Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings

Pages: 462-480

19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022

27 September 2022 through 29 September 2022

Indexing

ISI Web of Science

Scopus

Other information

Authenticus ID: P-00X-9KQ

DOI: 10.1007/978-3-031-17715-6_29

Abstract (EN): Several type inference approaches for rank-2 idempotent and commutative intersection types have been presented in the literature. Type inference relies on two stages: type constraint generation and solving. Defining constraint generation rules is rather straightforward, with one exception. To infer the type of an application, several derivations of the argument are required, one for each instance of the domain type of the function. The types of these derivations are then constrained against the instances. Noting that these derivations are isomorphic, by renaming of type variables, they can be obtained via a duplication operation on a single derivation of the argument. The application rule then constrains the intersection type resulting from duplication against the domain type of the function, resulting in an equality constraint between intersections. By treating intersections as sets, these constraints can be solved by solving a set unification problem, thus ensuring the types of the argument unify with the domain type of the function. Here we present a new type inference algorithm for rank-2 intersection types, which relies on set unification to solve equality constraints between intersections, and show it is both sound and complete. © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Language: English

Type (Professor's evaluation): Scientific