Type Inference for Rank-2 Intersection Types Using Set Unification

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2022

Autores

Ângelo, P (Autor) Outra; Florido, M (Autor) FCUP

Ata de Conferência Internacional

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

Páginas: 462-480

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

27 September 2022 through 29 September 2022

Indexação

ISI Web of Science

Scopus

Outras Informações

ID Authenticus: 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica