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 \emph{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.

Ori Roth is a PhD student at the Technion—Israel Institute of Technology. His research interests include programming languages, software engineering, and automata theory.