More Web Proxy on the site http://driver.im/

research-article

Java generics are turing complete

Author:

Radu GrigoreAuthors Info & Claims

ACM SIGPLAN Notices, Volume 52, Issue 1

Pages 73 - 85

https://doi.org/10.1145/3093333.3009871

Published: 01 January 2017 Publication History

Abstract

This paper describes a reduction from the halting problem of Turing machines to subtype checking in Java. It follows that subtype checking in Java is undecidable, which answers a question posed by Kennedy and Pierce in 2007. It also follows that Java's type checker can recognize any recursive language, which improves a result of Gill and Levy from 2016. The latter point is illustrated by a parser generator for fluent interfaces.

References

[1]

N. Amin and R. Tate. Java and Scala’s type systems are unsound: The existential crisis of null pointers. In OOPSLA, 2016.

Digital Library

[2]

R. O. Bjarnason. More Scala typehackery. https://apocalisp.wordpress.com/2009/09/02/ (see also https://michid.wordpress.com/2010/01/29), 2009.

[3]

A. Breslav. Mixed-site variance in Kotlin. http://blog.jetbrains.com/kotlin/2013/06/mixed, 2013.

[4]

B. Courcelle. On jump-deterministic pushdown automata. Mathematical Systems Theory, 1977.

[5]

L. Dionne. Boost.Hana. http://boostorg.github.io/hana, 2016.

[6]

Y. Gil and T. Levy. Formal language recognition with the Java type checker. In ECOOP, 2016.

[7]

O. Goldreich. Computational complexity: a conceptual perspective. Cambridge University Press, 2008.

[8]

J. Gosling, B. Joy, G. Steele, G. Bracha, and A. Buckley. The Java language specification, 2015. Java SE 8 Edition. B. Greenman, F. Muehlboeck, and R. Tate. Getting F-bounded polymorphism into shape. In PLDI, 2014.

Digital Library

[9]

R. Grigore. Parser generator for fluent interfaces. http://rgrig.appspot.com/javats, 2016.

[10]

J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison–Wesley, 1979.

Digital Library

[11]

A. J. Kennedy and B. Pierce. On decidability of nominal subtyping with variance. In FOOL, 2007.

[12]

D. E. Knuth. On the translation of languages from left to right. Information and Control, 1965.

[13]

M. Lange and H. Leiß. To CNF or not to CNF? An efficient yet presentable version of the CYK algorithm. Informatica Didactica, 2009.

[14]

X. Leroy. Formal verification of a realistic compiler. CACM, 2009.

Digital Library

[15]

M. Lillibridge. Translucent Sums: A Foundation for Higher-Order Modules. PhD thesis, CMU, 1997.

[16]

E. Lippert. A simple problem whose decidability is not known. Theoretical Computer Science Stack Exchange, 2013. http://cstheory.stackexchange.com/q/18866.

[17]

H. G. Mairson. Deciding ML typability is complete for deterministic exponential time. In POPL, 1990.

Digital Library

[18]

M. Odersky. Scaling DOT to Scala – soundness. http://scala-lang. org/blog/2016/02/17/scaling-dot-soundness.html, 2016.

[19]

B. C. Pierce. Bounded quantification is undecidable. Information and Computation, 1994.

Digital Library

[20]

A. Rossberg. Undecidability of OCaml type checking. Caml mailing list, 1999. http://caml.inria.fr/pub/old_caml_site/caml-list/1507.html. M. Sulzmann, G. J. Duck, S. L. P. Jones, and P. J. Stuckey. Understanding functional dependencies via constraint handling rules. J. Funct. Program., 2007.

Digital Library

[21]

R. Tate, A. Leung, and S. Lerner. Taming wildcards in Java’s type system. In PLDI, 2011.

Digital Library

[22]

A. M. Turing. On computable numbers, with an application to the Entscheidungsproblem. J. of Math, 1936.

[23]

T. L. Veldhuizen. C++ templates are Turing complete. Technical report, Indiana University, 2003.

[24]

M. Viroli. On the recursive generation of parametric types. Technical report, University of Bologna, 2000.

[25]

K. Wansbrough. Instance declarations are universal. http://www.lochan.org/keith/publications/undec.html (see also https://wiki.haskell.org/Type_SK), 1998.

[26]

S. Wehr and P. Thiemann. On the decidability of subtyping with bounded existential types. In APLAS, 2009.

Digital Library

[27]

S. Weirich. RepLib: a library for derivable type classes. In Haskell, 2006.

Digital Library

[28]

J. B. Wells. Typability and type checking in System F are equivalent and undecidable. Annals of Pure and Applied Logic, 1999.

[29]

Y. Zhang, M. C. Loring, G. Salvaneschi, B. Liskov, and A. C. Myers. Lightweight, flexible object-oriented generics. In PLDI, 2015.

Digital Library

Cited By

Lozov PKosarev DIvanov DBoulytchev D(2023)Relational Solver for Java Generics Type SystemLogic-Based Program Synthesis and Transformation10.1007/978-3-031-45784-5_8(118-128)Online publication date: 16-Oct-2023
https://doi.org/10.1007/978-3-031-45784-5_8
Boruch-Gruszecki AWaśko RXu YParreaux L(2022)A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoningProceedings of the ACM on Programming Languages10.1145/35633426:OOPSLA2(1526-1555)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563342
Dura AReichenbach CSöderberg E(2021)JavaDL: automatically incrementalizing Java bug pattern detectionProceedings of the ACM on Programming Languages10.1145/34855425:OOPSLA(1-31)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485542
Show More Cited By

Index Terms

Java generics are turing complete
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features

Recommendations

Java generics are turing complete
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

This paper describes a reduction from the halting problem of Turing machines to subtype checking in Java. It follows that subtype checking in Java is undecidable, which answers a question posed by Kennedy and Pierce in 2007. It also follows that Java's ...
Object and reference immutability using Java generics
ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering

A compiler-checked immutability guarantee provides useful documentation, facilitates reasoning, and enables optimizations. This paper presents Immutability Generic Java (IGJ), a novel language extension that expresses immutability without changing Java'...
Compile-time type-checking for custom type qualifiers in Java
OOPSLA '07: Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companion

We have created a system that enables programmers to add custom type qualifiers to the Java language in a backward-compatible way. The system allows programmers to write type qualifiers in their programs and to create compiler plug-ins that enforce the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 52, Issue 1

POPL '17

January 2017

901 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3093333

Editor:
Matthew Fluet

Issue’s Table of Contents

POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
January 2017
901 pages
ISBN:9781450346603
DOI:10.1145/3009837
General Chair:
Giuseppe Castagna
Paris Diderot University, France / CNRS, France
,
Program Chair:
Andrew D. Gordon
Microsoft Research, UK / University of Edinburgh, UK

Copyright © 2017 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 the author(s) 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: 01 January 2017

Published in SIGPLAN Volume 52, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
807
Total Downloads

Downloads (Last 12 months)43
Downloads (Last 6 weeks)5

Reflects downloads up to 05 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Lozov PKosarev DIvanov DBoulytchev D(2023)Relational Solver for Java Generics Type SystemLogic-Based Program Synthesis and Transformation10.1007/978-3-031-45784-5_8(118-128)Online publication date: 16-Oct-2023
https://doi.org/10.1007/978-3-031-45784-5_8
Boruch-Gruszecki AWaśko RXu YParreaux L(2022)A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoningProceedings of the ACM on Programming Languages10.1145/35633426:OOPSLA2(1526-1555)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563342
Dura AReichenbach CSöderberg E(2021)JavaDL: automatically incrementalizing Java bug pattern detectionProceedings of the ACM on Programming Languages10.1145/34855425:OOPSLA(1-31)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485542
Roth O(2021)Study of the subtyping machine of nominal subtyping with varianceProceedings of the ACM on Programming Languages10.1145/34855145:OOPSLA(1-27)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485514
Kalhauge CPalsberg JFreund SYahav E(2021)Logical bytecode reductionProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454091(1003-1016)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454091
Bravetti MFrancalanza AGolovanov IHüttel HJakobsen MKettunen MRavara A(2020)Behavioural Types for Memory and Method Safety in a Core Object-Oriented LanguageProgramming Languages and Systems10.1007/978-3-030-64437-6_6(105-124)Online publication date: 24-Nov-2020
https://doi.org/10.1007/978-3-030-64437-6_6
Kushigian BRawat AJust R(2019)Medusa: Mutant Equivalence Detection Using Satisfiability Analysis2019 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW)10.1109/ICSTW.2019.00035(77-82)Online publication date: Apr-2019
https://doi.org/10.1109/ICSTW.2019.00035
Racordon DLaemmel RPereira JMosses P(2024)Type Checking with Rewriting RulesProceedings of the 17th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3687997.3695640(171-183)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3687997.3695640
Belyakova JChung BTate RVitek J(2024)Decidable Subtyping of Existential Types for JuliaProceedings of the ACM on Programming Languages10.1145/36564218:PLDI(1091-1114)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656421
DeYoung HMordido APfenning FDas A(2024)Parametric Subtyping for Structural Parametric PolymorphismProceedings of the ACM on Programming Languages10.1145/36329328:POPL(2700-2730)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632932
Show More Cited By

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.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents