Is this a joke?
Python type checking allows eval with arbitrary code. Of course it's Turing complete.
Python type checking allows eval with arbitrary code. Of course it's Turing complete.
I'd recommend actually reading the paper.
It also means that it's expressive enough such that it can be more powerful then a traditional type system
Turing equivalence seems more interesting. Intuitively I'd think that type systems are supposed to be more constrained than programs they are being applied to. The fact that they are equivalent makes me think that those type systems are flawed (though I can't explain why).
There are plenty of languages with turing complete type systems.
agda, idris, coq, haskell, scala, etc...
The paper does that by hooking into some basic results of theoretical computer science: Turing Machines (TMs) can model any program, there is no program that can look at another program and say that it finishes execution (the halting problem is undecidable), and, oops, you can compile TMs into Python type hints, therefore type checking Python is undecidable.
If I understand correctly, that means type-checking python as you described was an open problem before, and this paper effectively proves it will never happen (ideally). They do this by establishing Turing completeness of type-hints, which are the main mechanisms for type-checking.
* https://doc.pypy.org/en/latest/faq.html#would-type-annotatio...
I wonder how many people actually do this and whether the proportion is big enough such that much of what's written in comments is heavily distorted.
Although often confused, fairly enough as they were introduced in the same PEP, an annotation is a part of the Python syntax and type hints are a specific set of notations and ways you can use those notations inside an annotation to be used by a type hinter (yes those notations are evaluated to objects at Python runtime but the type hinter never has to be aware of that or even ever use a Python runtime).
The paper is talking about those notations inside a type hinter, not annotation objects inside a Python runtime. e.g. you can get mypy to run a turing complete program using only the notations defined in PEP 484.