LIPIcs.ECOOP.2023.44.pdf
- Filesize: 0.87 MB
- 15 pages
Document
Python Type Hints Are Turing Complete (Pearl/Brave New Idea)
Author
Ori Roth 
-
Part of:
Volume:
37th European Conference on Object-Oriented Programming (ECOOP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: European Conference on Object-Oriented Programming (ECOOP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-11
File
Document Identifiers
Author Details
Acknowledgements
The author would like to thank to Yossi Gil for inspiring them to study the topic of nominal subtyping with variance.
Cite AsGet BibTex
Ori Roth. Python Type Hints Are Turing Complete (Pearl/Brave New Idea). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 44:1-44:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.44
https://doi.org/10.4230/LIPIcs.ECOOP.2023.44
Abstract
Grigore proved that Java generics are Turing complete by describing a reduction from Turing machines to Java subtyping. Furthermore, he demonstrated that his "subtyping machines" could have metaprogramming applications if not for their extremely high compilation times. The current work reexamines Grigore’s study in the context of another prominent programming language - Python. We show that the undecidable Java fragment used in Grigore’s construction is included in Python’s type system, making it Turing complete. In contrast to Java, Python type hints are checked by third-party static analyzers and run-time type checkers. The new undecidability result means that both kinds of type checkers cannot fully incorporate Python’s type system and guarantee termination. The paper includes a survey of infinite subtyping cycles in various type checkers and type reification in different Python distributions. In addition, we present an alternative reduction in which the Turing machines are simulated in real time, resulting in a significantly faster compilation. Our work is accompanied by a Python implementation of both reductions that compiles Turing machines into Python subtyping machines.
Subject Classification
ACM Subject Classification
- Software and its engineering → General programming languages
Keywords
- nominal Subtyping with Variance
- Python
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- ECMA International. ECMA Standard 335: Common Language Infrastructure, 3 edition, June 2005. Available at http://www.ecma-international.org/publications/standards/Ecma-335.htm (accessed Aug . 2022).
- Martin Fowler. Fluentinterface, 2005. URL: https://www.martinfowler.com/bliki/FluentInterface.html.
- Yossi Gil and Tomer Levy. Formal language recognition with the Java type checker. In Shriram Krishnamurthi and Benjamin S. Lerner, editors, 30th Europ. Conf OO Prog. (ECOOP 2016), volume 56 of Leibniz International Proceedings in Inf. (LIPIcs), pages 10:1-10:27, Dagstuhl, Germany, 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2016.10.
- Yossi Gil and Ori Roth. Fling - A fluent API generator. In Alastair F. Donaldson, editor, 33rd Europ. Conf OO Prog. (ECOOP 2019), volume 134 of Leibniz International Proceedings in Inf. (LIPIcs), pages 13:1-13:25, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2019.13.
- Ben Greenman, Fabian Muehlboeck, and Ross Tate. Getting f-bounded polymorphism into shape. SIGPLAN Not., 49(6):89-99, June 2014. URL: https://doi.org/10.1145/2666356.2594308.
- Radu Grigore. Java generics are turing complete. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 73-85, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3009837.3009871.
- Andrew Kennedy and Benjamin Pierce. On decidability of nominal subtyping with variance. In Int. Work. Found. & Devel. OO Lang., FOOL/WOOD`07, Nice, France, January 2007. ACM. URL: http://foolwood07.cs.uchicago.edu/program/kennedy-abstract.html.
- Łukasz Langa. PEP 585 - Type Hinting Generics In Standard Collections. Available at https://peps.python.org/pep-0585/ (accessed Nov . 2022).
- Jukka Lehtosalo, Guido van Rossum, Ivan Levkivskyi, and Michael J. Sullivan. mypy. Available at http://mypy-lang.org/ (accessed Aug . 2022).
-
Tomoki Nakamaru, Kazuhiro Ichikawa, Tetsuro Yamazaki, and Shigeru Chiba. Silverchain: a fluent API generator. In Proc. 16th ACM SIGPLAN Int. Conf Generative Prog., GPCE'17, pages 199-211, Vancouver, BC, Canada, 2017. ACM.
- Martin Odersky, Philippe Altherr, Vincent Cremet, Gilles Dubochet, Burak Emir, Philipp Haller, Stéphane Micheloud, Nikolay Mihaylov, Adriaan Moors, Lukas Rytz, Michel Schinz, Erik Stenman, and Matthias Zenger. Scala language specification version 2.13. Available on: https://scala-lang.org/files/archive/spec/2.13/ (accessed Aug . 2022).
- Oracle. The Java Language Specification, Java SE 8 Edition, February 2015. Available at URL: https://docs.oracle.com/javase/specs/.
-
Emil Post. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 52:264-268, 1946.
- Ori Roth. Study of the subtyping machine of nominal subtyping with variance. Proc. ACM Program. Lang., 5(OOPSLA), October 2021. URL: https://doi.org/10.1145/3485514.
- Ross Tate, Alan Leung, and Sorin Lerner. Taming wildcards in java’s type system. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '11, pages 614-627, New York, NY, USA, 2011. Association for Computing Machinery. URL: https://doi.org/10.1145/1993498.1993570.
- Guido van Rossum, Jukka Lehtosalo, and Łukasz Langa. PEP 484 - Type Hints. Available at https://peps.python.org/pep-0484/ (accessed Nov . 2022).
- Guido van Rossum and Ivan Levkivskyi. PEP 483 - The Theory of Type Hints. Available at https://peps.python.org/pep-0483/ (accessed Nov . 2022).
-
Todd Veldhuizen. Using C++ Template Metaprograms, pages 459-473. SIGS Publications, Inc., USA, 1996.
- Tetsuro Yamazaki, Tomoki Nakamaru, Kazuhiro Ichikawa, and Shigeru Chiba. Generating a fluent api with syntax checking from an LR grammar. Proc. ACM Program. Lang., 3(OOPSLA), October 2019. URL: https://doi.org/10.1145/3360560.