4 ms·
Like others have said, this isn't really about being useful, so much as interesting or revealing. It answers the question "can we be certain that a Python prog
by an1sotropy 4y ago
Like others have said, this isn't really about being useful, so much as interesting or revealing. It answers the question "can we be certain that a Python program with type hints can actually be type-checked?" by saying "sorry, no: it's possible that the type checking will never finish".
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.
- lake_vincent 4y agoAh, I see! That makes a lot of sense, thank you for explaining. 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.
- an1sotropy 4y agoWell, I'm sure mypy and things like it will continue to grow, and the discipline of Python type hinting will probably become more popular, not less, because it offers new opportunities for catching bugs (but maybe not for optimizations, which I think is interesting*). So maybe it was an open question whether type checking would always terminate (now answered in the negative), but that shouldn't stop anyone from using type hints, considering their practical benefits. * https://doc.pypy.org/en/latest/faq.html#would-type-annotations-help-pypy-s-performance https://doc.pypy.org/en/latest/faq.html#would-type-annotatio...