research-article

Intersection types in Java

Author:

Martin PlümickeAuthors Info & Claims

PPPJ '08: Proceedings of the 6th international symposium on Principles and practice of programming in Java

Pages 181 - 188

https://doi.org/10.1145/1411732.1411757

Published: 09 September 2008 Publication History

Get Access

Abstract

In the past we analyzed typeless Java programs. One of our results was, that there may be different correct typings for one method. This means that the principal types of such methods are intersection types. We presented a type-inference algorithm. For typeless Java methods the algorithm infers its principal intersection type. Unfortunately, like Java byte-code, Java does not allow intersection types.

In this paper we present an algorithm, which resolves intersection types of Java methods, such that Java programs with standard typings are generated.

In the algorithm we have to differentiate two cases of intersection types. On the one hand there are methods with intersection types, where for all types the same code is executed. On the other hand there are methods, which call in dependence to its typings different methods. These two cases have to be treated differently during type resolving.

Finally, we will see that this differentiation leads to a refined definition of Java method principal types.

References

[1]

E. Börger and W. Schulte. A programmer friendly modular definition of the semantics of java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 353--404. Springer, 1999.

Digital Library

Google Scholar

[2]

G. Boudol and P. Zimmer. On type inference in the intersection type discipline. Electronic Notes in Theoretical Computer Science, 136:23--42, 2005.

Digital Library

Google Scholar

[3]

M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Logic, 21(4):685--693, 1980.

Google Scholar

[4]

L. Damas and R. Milner. Principal type-schemes for functional programs. Proc. 9th Symposium on Principles of Programming Languages, 1982.

Digital Library

Google Scholar

[5]

J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java#8482; Language Specification. The Java series. Addison-Wesley, 3rd edition, 2005.

Digital Library

Google Scholar

[6]

J. R. Hindley. Types with intersection: An introduction. Formal Aspects of Computing, 4(5):470--486, 1992.

Digital Library

Google Scholar

[7]

A. J. Kfoury and J. B. Wells. Principality and type inference for intersection types using expansion variables. Theoretical Computer Science, 311(1--3):1--70, 2004.

Digital Library

Google Scholar

[8]

D. Leivant. Polymorphic type inference. Proc. 10th Symposium on Principles of Programming Languages 1982, 1983.

Digital Library

Google Scholar

[9]

R. Milner. The definition of Standard ML (Revised). MIT Press, Cambridge, Mass., 1997.

Digital Library

Google Scholar

[10]

M. Plümicke. Typeless Programming in Java 5.0 with wildcards. In V. Amaral, L. Veiga, L. Marcelino, and H. C. Cunningham, editors, 5th International Conference on Principles and Practices of Programming in Java, ACM International Conference Proceeding Series, pages 73--82, September 2007.

Digital Library

Google Scholar

[11]

M. Plümicke and J. Bäuerle. Typeless Programming in Java 5.0. In R. Gitzel, M. Aleksey, M. Schader, and C. Krintz, editors, 4th International Conference on Principles and Practices of Programming in Java, ACM International Conference Proceeding Series, pages 175--181. Mannheim University Press, August 2006.

Digital Library

Google Scholar

[12]

S. van Bakel. Principal type schemes for the strict type assignment system. Journal of Logic and Computing, 3(6):643--670, 1993.

Crossref

Google Scholar

[13]

S. van Bakel. Intersection type assignment systems. Theoretical Computer Science, 151(2):385--435, 1995.

Digital Library

Google Scholar

Cited By

View all

Pearce D(2017)Rewriting for sound and complete union, intersection and negation typesACM SIGPLAN Notices10.1145/3170492.313604252:12(117-130)Online publication date: 23-Oct-2017
https://dl.acm.org/doi/10.1145/3170492.3136042
Pearce DFlatt MErdweg S(2017)Rewriting for sound and complete union, intersection and negation typesProceedings of the 16th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3136040.3136042(117-130)Online publication date: 23-Oct-2017
https://dl.acm.org/doi/10.1145/3136040.3136042
Pearce D(2013)Sound and Complete Flow Typing with Unions, Intersections and NegationsProceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 773710.1007/978-3-642-35873-9_21(335-354)Online publication date: 20-Jan-2013
https://dl.acm.org/doi/10.1007/978-3-642-35873-9_21

Index Terms

Intersection types in Java
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
        Modules / packages
      2. Language types
        Object oriented languages

Recommendations

Typeless programming in Java 5.0
PPPJ '06: Proceedings of the 4th international symposium on Principles and practice of programming in Java

With the introduction of Java 5.0 [9] the type system has been extended by parameterized types, type variables, type terms, and wildcards. As a result very complex types can arise. The termVector<Vector<AbstractList<Integer>>>is for example a correct ...
Typeless programming in Java 5.0 with wildcards
PPPJ '07: Proceedings of the 5th international symposium on Principles and practice of programming in Java

With the introduction of Java 5.0 [8] the type system has been extended by parameterized types, type variables, type terms, and wildcards. As a result very complex types can arise. The term Vector<? super Vector<? extends List<Integer>>> is for example ...
Well-typings for Java_λ
PPPJ '11: Proceedings of the 9th International Conference on Principles and Practice of Programming in Java

In the last decade Java has been extended by some features, which are well-known from functional programming languages. In Java 8 the language will be expanded by closures (λ-expressions).

In our contribution we give a formal definition for an abstract ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PPPJ '08: Proceedings of the 6th international symposium on Principles and practice of programming in Java

September 2008

198 pages

ISBN:9781605582238

DOI:10.1145/1411732

Conference Chairs:
Luis Veiga
Universidade Técnica de Lisboa, Portugal
,
Vasco Amaral
Universidade Nova de Lisboa, Portugal

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 September 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PPPJ08

Sponsor:

PPPJ08: Principles and Practice of Prgramming in Java 2008

September 9 - 11, 2008

Modena, Italy

Acceptance Rates

Overall Acceptance Rate 29 of 58 submissions, 50%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
158
Total Downloads

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

Reflects downloads up to 17 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Pearce D(2017)Rewriting for sound and complete union, intersection and negation typesACM SIGPLAN Notices10.1145/3170492.313604252:12(117-130)Online publication date: 23-Oct-2017
https://dl.acm.org/doi/10.1145/3170492.3136042
Pearce DFlatt MErdweg S(2017)Rewriting for sound and complete union, intersection and negation typesProceedings of the 16th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3136040.3136042(117-130)Online publication date: 23-Oct-2017
https://dl.acm.org/doi/10.1145/3136040.3136042
Pearce D(2013)Sound and Complete Flow Typing with Unions, Intersections and NegationsProceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 773710.1007/978-3-642-35873-9_21(335-354)Online publication date: 20-Jan-2013
https://dl.acm.org/doi/10.1007/978-3-642-35873-9_21

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Index Terms

Recommendations

Typeless programming in Java 5.0

Typeless programming in Java 5.0 with wildcards

Well-typings for Javaλ

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations

Well-typings for Java_λ