File Download
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.1145/3622871
- Scopus: eid_2-s2.0-85175069254
- WOS: WOS:001087279100075
Supplementary
- Citations:
- Appears in Collections:
Article: Greedy Implicit Bounded Quantification
Title | Greedy Implicit Bounded Quantification |
---|---|
Authors | |
Keywords | Bounded Quantification Mechanical Formalization Type Inference |
Issue Date | 16-Oct-2023 |
Publisher | ACM |
Citation | Proceedings of the ACM on Programming Languages, 2023, v. 7, n. OOPSLA How to Cite? |
Abstract | Mainstream object-oriented programming languages such as Java, Scala, C#, or TypeScript have polymorphic type systems with subtyping and bounded quantification. Bounded quantification, despite being a pervasive and widely used feature, has attracted little research work on type-inference algorithms to support it. A notable exception is local type inference, which is the basis of most current implementations of type inference for mainstream languages. However, support for bounded quantification in local type inference has important restrictions, and its non-algorithmic specification is complex. In this paper, we present a variant of kernel F≤, which is the canonical calculus with bounded quantification, with implicit polymorphism. Our variant, called F≤b, comes with a declarative and an algorithmic formulation of the type system. The declarative type system is based on previous work on bidirectional typing for predicative higher-rank polymorphism and a greedy approach to implicit instantiation. This allows for a clear declarative specification where programs require few type annotations and enables implicit polymorphism where applications omit type parameters. Just as local type inference, explicit type applications are also available in F≤b if desired. This is useful to deal with impredicative instantiations, which would not be allowed otherwise in F≤b. Due to the support for impredicative instantiations, we can obtain a completeness result with respect to kernel F≤, showing that all the well-typed kernel F≤programs can type-check in F≤b. The corresponding algorithmic version of the type system is shown to be sound, complete, and decidable. All the results have been mechanically formalized in the Abella theorem prover. |
Persistent Identifier | http://hdl.handle.net/10722/339347 |
ISI Accession Number ID |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Cui, Chen | - |
dc.contributor.author | Jiang, Shengyi | - |
dc.contributor.author | Dos Santos Oliveira, Bruno C | - |
dc.date.accessioned | 2024-03-11T10:35:53Z | - |
dc.date.available | 2024-03-11T10:35:53Z | - |
dc.date.issued | 2023-10-16 | - |
dc.identifier.citation | Proceedings of the ACM on Programming Languages, 2023, v. 7, n. OOPSLA | - |
dc.identifier.uri | http://hdl.handle.net/10722/339347 | - |
dc.description.abstract | <p>Mainstream object-oriented programming languages such as Java, Scala, C#, or TypeScript have polymorphic type systems with subtyping and bounded quantification. Bounded quantification, despite being a pervasive and widely used feature, has attracted little research work on type-inference algorithms to support it. A notable exception is local type inference, which is the basis of most current implementations of type inference for mainstream languages. However, support for bounded quantification in local type inference has important restrictions, and its non-algorithmic specification is complex. </p><p>In this paper, we present a variant of kernel <em>F</em>≤, which is the canonical calculus with bounded quantification, with implicit polymorphism. Our variant, called <em>F</em>≤<em>b</em>, comes with a declarative and an algorithmic formulation of the type system. The declarative type system is based on previous work on bidirectional typing for predicative higher-rank polymorphism and a greedy approach to implicit instantiation. This allows for a clear declarative specification where programs require few type annotations and enables implicit polymorphism where applications omit type parameters. Just as local type inference, explicit type applications are also available in <em>F</em>≤<em>b</em> if desired. This is useful to deal with impredicative instantiations, which would not be allowed otherwise in <em>F</em>≤<em>b</em>. Due to the support for impredicative instantiations, we can obtain a completeness result with respect to kernel <em>F</em>≤, showing that all the well-typed kernel <em>F</em>≤programs can type-check in <em>F</em>≤<em>b</em>. The corresponding algorithmic version of the type system is shown to be sound, complete, and decidable. All the results have been mechanically formalized in the Abella theorem prover.</p> | - |
dc.language | eng | - |
dc.publisher | ACM | - |
dc.relation.ispartof | Proceedings of the ACM on Programming Languages | - |
dc.rights | This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. | - |
dc.subject | Bounded Quantification | - |
dc.subject | Mechanical Formalization | - |
dc.subject | Type Inference | - |
dc.title | Greedy Implicit Bounded Quantification | - |
dc.type | Article | - |
dc.description.nature | published_or_final_version | - |
dc.identifier.doi | 10.1145/3622871 | - |
dc.identifier.scopus | eid_2-s2.0-85175069254 | - |
dc.identifier.volume | 7 | - |
dc.identifier.issue | OOPSLA | - |
dc.identifier.eissn | 2475-1421 | - |
dc.identifier.isi | WOS:001087279100075 | - |
dc.identifier.issnl | 2475-1421 | - |