research-article

On subtyping, wildcards, and existential types

Authors:

Nicholas Cameron,

Sophia DrossopoulouAuthors Info & Claims

FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs

Article No.: 4, Pages 1 - 7

https://doi.org/10.1145/1557898.1557902

Published: 06 July 2009 Publication History

Abstract

Wildcards are an often confusing part of the Java type system: the behaviour of wildcard types is not fully specified by subtyping, due to wildcard capture, and the rules for type checking are often misunderstood. Their very formulation seems somehow 'different' from the rest of the Java type system, which is based on a simple, nominal hierarchy.

We investigate subtyping in models for Java with and without generics and wildcards. We separate subclassing from subtyping, unify subtyping for class and wildcard types using existential types, and show that Java wildcards emerge naturally from the combination of inclusion and parametric polymorphism.

References

[1]

Martín Abadi, Luca Cardelli, and Ramesh Viswanathan. An Interpretation of Objects and Object Types. In Principles of Programming Languages (POPL), 1996.

Digital Library

[2]

Gilad Bracha. Generics in the Java Programming Language, 2004. http://java.sun.com/j2se/1.5/pdf/genericstutorial.pdf.

[3]

Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. Making the Future Safe for the Past: Adding Genericity to the Java Programming Language. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 1998.

Digital Library

[4]

K. B. Bruce and J. N. Foster. LOOJ: Weaving LOOM into Java. Lecture Notes in Computer Science, 3086:389--413, 2004.

[5]

Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. Comparing Object Encodings. Information and Computation, 155(1--2), 1999.

Digital Library

[6]

Kim B. Bruce, Martin Odersky, and Philip Wadler. A Statically Safe Alternative to Virtual Types. In European Conference on Object Oriented Programming (ECOOP), 1998.

Digital Library

[7]

Kim B. Bruce, Leaf Petersen, and Adrian Fiech. Subtyping Is Not a Good "Match" for Object-Oriented Languages. In European Conference on Object Oriented Programming (ECOOP), 1997.

[8]

Nicholas Cameron. Existential Types for Variance --- Java Wildcards and Ownership Types. PhD thesis, Imperial College London, 2009.

[9]

Nicholas Cameron and Sophia Drossopoulou. On Subtyping, Wildcards, and Existential Types. Technical Report 04, School of Engineering and Computer Science, VUW, 2009. https://ecs.victoria.ac.nz/twiki/pub/Main/TechnicalReportSeries/ECSTR09-04.pdf.

[10]

Nicholas Cameron, Sophia Drossopoulou, and Erik Ernst. A Model for Java with Wildcards. In European Conference on Object Oriented Programming (ECOOP), 2008.

Digital Library

[11]

Nicholas Cameron, Erik Ernst, and Sophia Drossopoulou. Towards an Existential Types Model for Java Wildcards. In Formal Techniques for Java-like Programs (FTfJP), 2007.

[12]

Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John Mitchell. F-Bounded Quantification for Object-Oriented Programming. In Functional Programming Languages and Computer Architecture (FPCA), 1989.

Digital Library

[13]

Kathleen Fisher and John C. Mitchell. Notes on Typed Object-Oriented Programming. In Symposium on Theoretical Aspects of Computer Science (STACS), 1994.

Digital Library

[14]

James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. The Java Language Specification Third Edition. Addison-Wesley, Boston, Mass., 2005.

Digital Library

[15]

Martin Hofmann and Benjamin C. Pierce. A Unifying Type-Theoretic Framework for Objects. In Symposium on Theoretical Aspects of Computer Science (STACS), 1994.

Digital Library

[16]

Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a Minimal Core Calculus For Java and GJ. ACM Trans. Program. Lang. Syst., 23(3):396--450, 2001. An earlier version of this work appeared at OOPSLA'99.

Digital Library

[17]

Atsushi Igarashi and Mirko Viroli. Variant Parametric Types: A Flexible Subtyping Scheme for Generics. Transactions on Programming Languages and Systems, 28(5):795--847, 2006. An earlier version appeared as "On variance-based subtyping for parametric types" at European Conference on Object Oriented Programming (ECOOP) 2002.

Digital Library

[18]

Mads Torgersen and Erik Ernst and Christian Plesner Hansen. Wild FJ. In Foundations of Object-Oriented Languages (FOOL), 2005.

[19]

Donna Malayeri and Jonathan Aldrich. Integrating Nominal and Structural Subtyping. In European Conference on Object Oriented Programming (ECOOP), 2008.

Digital Library

[20]

M. Odersky and P. Wadler. Pizza into Java: Translating Theory into Practice. In Principles of Programming. Languages (POPL), 1997.

Digital Library

[21]

Benjamin C. Pierce and David N. Turner. Simple Type-Theoretic Foundations for Object-Oriented Programming. Journal of Functional Programming, 4(2):207--247, 1994.

[22]

Chieri Saito and Atsushi Igarashi. Matching thistype to subtyping. In Symposium on Applied Computing (SAC), 2009.

Digital Library

[23]

Mads Torgersen, Christian Plesner Hansen, Erik Ernst, Peter von der Ahé, Gilad Bracha, and Neal Gafter. Adding Wildcards to the Java Programming Language. Journal of Object Technology, 3(11):97--116, 2004. Special issue: OOPS track at SAC 2004, Nicosia/Cyprus.

[24]

Stefan Wehr and Peter Thiemann. Subtyping Existential Types. In Formal Techniques for Java-like Programs (FTfJP), 2008.

Cited By

Saito CIgarashi A(2013)Matching MyType to subtypingScience of Computer Programming10.1016/j.scico.2012.12.01078:7(933-952)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1016/j.scico.2012.12.010
Tardieu ONystrom NPeshansky ISaraswat V(2012)Constrained kindsACM SIGPLAN Notices10.1145/2398857.238467547:10(811-830)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2398857.2384675
Tardieu ONystrom NPeshansky ISaraswat VLeavens GDwyer M(2012)Constrained kindsProceedings of the ACM international conference on Object oriented programming systems languages and applications10.1145/2384616.2384675(811-830)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384616.2384675
Show More Cited By

Index Terms

On subtyping, wildcards, and existential types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Classes and objects
        Data types and structures
      2. Language types

Recommendations

An existential crisis resolved: type inference for first-class existential types

Despite the great success of inferring and programming with universal types, their dual—existential types—are much harder to work with. Existential types are useful in building abstract types, working with indexed types, and providing first-class support ...
Subtyping recursive types

We investigate the interactions of subtyping and recursive types, in a simply typed λ-calculus. The two fundamental questions here are whether two (recursive)types are in the subtype relation and whether a term has a type. To address the first question, ...
On the Decidability of Subtyping with Bounded Existential Types
Programming Languages and Systems
Abstract
Bounded existential types are a powerful language feature for modeling partial data abstraction and information hiding. However, existentials do not mingle well with subtyping as found in current object-oriented languages: the subtyping relation ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs

July 2009

64 pages

ISBN:9781605585406

DOI:10.1145/1557898

Conference Chair:
Anindya Banerjee
IMDEA Software, Spain

Copyright © 2009 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 July 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Funding Sources

Sixth Framework Programme

Conference

ECOOP '09

ECOOP '09: European Conference on Object-Oriented Programming

July 6, 2009

Genova, Italy

Acceptance Rates

FTfJP '09 Paper Acceptance Rate 10 of 15 submissions, 67%;

Overall Acceptance Rate 51 of 75 submissions, 68%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
159
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)3

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Saito CIgarashi A(2013)Matching MyType to subtypingScience of Computer Programming10.1016/j.scico.2012.12.01078:7(933-952)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1016/j.scico.2012.12.010
Tardieu ONystrom NPeshansky ISaraswat V(2012)Constrained kindsACM SIGPLAN Notices10.1145/2398857.238467547:10(811-830)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2398857.2384675
Tardieu ONystrom NPeshansky ISaraswat VLeavens GDwyer M(2012)Constrained kindsProceedings of the ACM international conference on Object oriented programming systems languages and applications10.1145/2384616.2384675(811-830)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384616.2384675
Na HRyu SChoe KPierce B(2012)Exact type parameterization and ThisType supportProceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation10.1145/2103786.2103790(13-24)Online publication date: 28-Jan-2012
https://dl.acm.org/doi/10.1145/2103786.2103790
Tate RLeung ALerner SHall MPadua D(2011)Taming wildcards in Java's type systemProceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1993498.1993570(614-627)Online publication date: 4-Jun-2011
https://dl.acm.org/doi/10.1145/1993498.1993570
Tate RLeung ALerner S(2011)Taming wildcards in Java's type systemACM SIGPLAN Notices10.1145/1993316.199357046:6(614-627)Online publication date: 4-Jun-2011
https://dl.acm.org/doi/10.1145/1993316.1993570
Summers ACameron NDezani-Ciancaglini MDrossopoulou S(2010)Towards a semantic model for Java wildcardsProceedings of the 12th Workshop on Formal Techniques for Java-Like Programs10.1145/1924520.1924522(1-7)Online publication date: 22-Jun-2010
https://dl.acm.org/doi/10.1145/1924520.1924522
Saito CIgarashi AArora SLeavens G(2009)Self type constructorsProceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications10.1145/1640089.1640109(263-282)Online publication date: 26-Oct-2009
https://dl.acm.org/doi/10.1145/1640089.1640109
Saito CIgarashi A(2009)Self type constructorsACM SIGPLAN Notices10.1145/1639949.164010944:10(263-282)Online publication date: 25-Oct-2009
https://dl.acm.org/doi/10.1145/1639949.1640109

View Options

Get Access

Login options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents