research-article

Open access

Greedy Implicit Bounded Quantification

Authors:

Bruno C. d. S. OliveiraAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue OOPSLA2

Article No.: 295, Pages 2083 - 2111

https://doi.org/10.1145/3622871

Published: 16 October 2023 Publication History

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.

References

[1]

Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. 1991. Inheritance as Implicit Coercion. Information and Computation, 93, 1 (1991), 172–221. https://doi.org/10.1016/0890-5401(91)90055-7

Digital Library

[2]

Luca Cardelli. 1993. An Implementation of F_<:. SRC Research Reports, Digital Equipment Corporation.

[3]

Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. 1991. An Extension of System F with Subtyping. In Proceedings of the International Conference on Theoretical Aspects of Computer Software. 750–770. isbn:3540544151 https://doi.org/10.1007/3-540-54415-1_73

[4]

Luca Cardelli and Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. ACM Comput. Surv., 17, 4 (1985), 471–523. https://doi.org/10.1145/6041.6042

Digital Library

[5]

Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira. 2023. Greedy Implicit Bounded Quantification (Artifact). https://doi.org/10.5281/zenodo.8336774

Digital Library

[6]

Pierre-Louis Curien and Giorgio Ghelli. 1992. Coherence of Subsumption, Minimum Typing and Type-Checking in F≤. Mathematical Structures in Computer Science, 2, 1 (1992), 55–91. https://doi.org/10.1017/S0960129500001134

[7]

Stephen Dolan and Alan Mycroft. 2017. Polymorphism, Subtyping, and Type Inference in MLsub. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 60–72. https://doi.org/10.1145/3009837.3009882

Digital Library

[8]

Jana Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. 429–442. https://doi.org/10.1145/2500365.2500582

Digital Library

[9]

Jana Dunfield and Neelakantan R. Krishnaswami. 2019. Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types. In Proceedings of the ACM on Programming Languages. 3, Article 9, https://doi.org/10.1145/3290322

Digital Library

[10]

Jonathan Eifrig, Scott Smith, and Valery Trifonov. 1995. Sound Polymorphic Type Inference for Objects. In Proceedings of the 10th ACM International Conference on Object Oriented Programming Systems Languages and Applications. 169–184. https://doi.org/10.1145/217838.217858

Digital Library

[11]

Jonathan Eifrig, Scott Smith, and Valery Trifonov. 1995. Type Inference for Recursively Constrained Types and Its Application to OOP. Electronic Notes in Theoretical Computer Science, 1 (1995), 132–153. https://doi.org/10.1016/S1571-0661(04)80008-2

[12]

Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. 2016. Visible Type Application. In European Symposium on Programming. 229–254. https://doi.org/10.1007/978-3-662-49498-1_10

Digital Library

[13]

Andrew Gacek. 2008. The Abella Interactive Theorem Prover (System Description). In Proceedings of 4th International Joint Conference on Automated Reasoning. 154–161. https://doi.org/10.1007/978-3-540-71070-7_13

Digital Library

[14]

Jean-Yves Girard. 1972. Interprétation fonctionnelle et elimination des coupures de l’arithmétique d’ordre supérieur. Université de Paris 7.

[15]

Roger Hindley. 1969. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc., 146 (1969), 29–60. https://doi.org/10.2307/1995158

[16]

Haruo Hosoya and Benjamin C. Pierce. 1999. How Good is Local Type Inference? University of Pennsylvania.

[17]

Christopher Jenkins and Aaron Stump. 2018. Spine-Local Type Inference. In Proceedings of the 30th Symposium on Implementation and Application of Functional Languages. 37–48. https://doi.org/10.1145/3310232.3310233

Digital Library

[18]

Didier Le Botlan and Didier Rémy. 2003. ML^ F: Raising ML to the Power of System F. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming. 27–38. https://doi.org/10.1145/944705.944709

Digital Library

[19]

Daan Leijen. 2008. HMF: Simple Type Inference for First-class Polymorphism. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming. 283–294. https://doi.org/10.1145/1411204.1411245

Digital Library

[20]

Guillaume André Fradji Martres. 2023. Type-Preserving Compilation of Class-Based Languages. Ph. D. Dissertation. EPFL. https://doi.org/10.5075/epfl-thesis-8218

[21]

Henry Mercer, Cameron Ramsay, and Neel Krishnaswami. 2022. Implicit Polarized F: Local Type Inference for Impredicativity. arXiv preprint arXiv:2203.01835, https://doi.org/10.48550/arXiv.2203.01835

[22]

Robin Milner. 1978. A Theory of Type Polymorphism in Programming. J. Comput. System Sci., 17, 3 (1978), 348–375. https://doi.org/10.1016/0022-0000(78)90014-4

[23]

Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations to Work. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 54–67. https://doi.org/10.1145/237721.237729

Digital Library

[24]

Martin Odersky, Christoph Zenger, and Matthias Zenger. 2001. Colored Local Type Inference. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 41–53. https://doi.org/10.1145/360204.360207

Digital Library

[25]

Lionel Parreaux. 2020. The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl). In Proceedings of the ACM on Programming Languages. 4, Article 124, https://doi.org/10.1145/3409006

Digital Library

[26]

Lionel Parreaux and Chun Yin Chau. 2022. MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types. In Proceedings of the ACM on Programming Languages. 6, Article 141, https://doi.org/10.1145/3563304

Digital Library

[27]

Simon Peyton Jones and Mark Shields. 2004. Lexically Scoped Type Variables. March, Draft

[28]

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical Type Inference for Arbitrary-Rank Types. Journal of Functional Programming, 17, 1 (2007), 1–82. https://doi.org/10.1017/s0956796806006034

Digital Library

[29]

Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 305–315. https://doi.org/10.1145/143165.143228

Digital Library

[30]

Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press. isbn:0262162091

[31]

Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 252–265. https://doi.org/10.1145/268946.268967

Digital Library

[32]

Hubert Plociniczak. 2016. Decrypting Local Type Inference. Ph. D. Dissertation. EPFL.

[33]

François Pottier. 1998. Type Inference in the Presence of Subtyping: From Theory to Practice. Ph. D. Dissertation. INRIA.

[34]

Didier Rémy and Boris Yakobowski. 2008. From ML to ML^ F: Graphic Type Constraints with Efficient Type Inference. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming. 63–74. https://doi.org/10.1145/1411204.1411216

Digital Library

[35]

John C. Reynolds. 1974. Towards a Theory of Type Structure. In Programming Symposium. 408–425. https://doi.org/10.1007/3-540-06859-7_148

[36]

Dilip Sequeira. 1998. Type Inference With Bounded Quantification. Ph. D. Dissertation. University of Edinburgh.

[37]

Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. 2020. A Quick Look at Impredicativity. In Proceedings of the ACM on Programming Languages. 4, Article 89, https://doi.org/10.1145/3408971

Digital Library

[38]

Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. 2018. Guarded Impredicative Polymorphism. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. 783–796. https://doi.org/10.1145/3192366.3192389

Digital Library

[39]

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages. 274–293. https://doi.org/10.4230/LIPIcs.SNAPL.2015.274

[40]

Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. 2008. FPH: First-class Polymorphism for Haskell. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming. 295–306. https://doi.org/10.1145/1411204.1411246

Digital Library

[41]

Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. Consistent Subtyping for All. ACM Transactions on Programming Languages and Systems, 42, 1 (2019), Article 2, https://doi.org/10.1145/3310339

Digital Library

[42]

Jinxu Zhao and Bruno C. d. S. Oliveira. 2022. Elementary Type Inference. In 36th European Conference on Object-Oriented Programming. 2:1–2:28. https://doi.org/10.4230/LIPIcs.ECOOP.2022.2

[43]

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference. In Proceedings of the ACM on Programming Languages. 3, Article 112, https://doi.org/10.1145/3341716

Digital Library

[44]

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira. 2023. Recursive Subtyping for All. In Proceedings of the ACM on Programming Languages. 7, Article 48, https://doi.org/10.1145/3571241

Digital Library

Cited By

Parreaux LBoruch-Gruszecki AFan AChau C(2024)When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class PolymorphismProceedings of the ACM on Programming Languages10.1145/36328908:POPL(1418-1450)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632890

Index Terms

Greedy Implicit Bounded Quantification
1. Theory of computation
  1. Logic
    1. Type theory

Recommendations

Decidable subclassing-bounded quantification
TLDI '05: Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation

Bounded Quantification allows Quantified types to specify subtyping bounds for the type variables they introduce. It has undecidable subtyping and type checking. This paper shows that subclassing-bounded Quantification---type variables have subclassing ...
Java type inference is broken: can we fix it?
OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications

Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity ...
Java type inference is broken: can we fix it?

Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue OOPSLA2

October 2023

2250 pages

EISSN:2475-1421

DOI:10.1145/3554312

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 October 2023

Published in PACMPL Volume 7, Issue OOPSLA2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Huawei
Hong Kong Research Grants Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
274
Total Downloads

Downloads (Last 12 months)274
Downloads (Last 6 weeks)17

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Parreaux LBoruch-Gruszecki AFan AChau C(2024)When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class PolymorphismProceedings of the ACM on Programming Languages10.1145/36328908:POPL(1418-1450)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632890

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents