4 ms·

That’s not at all what’s going on here. While the Python interpreter permits and executes arbitrary expressions as annotations, Python static type checkers (my

That’s not at all what’s going on here. While the Python interpreter permits and executes arbitrary expressions as annotations, Python static type checkers (mypy, Pytype, Pyre, Pyright) do not. This isn’t just an implementation limitation; the typing specifications (PEP 484 and successors) don’t allow it. For example, although these two definitions evaluate to the same result at runtime: def f() -> int: return 1 def f() -> (lambda: int)(): return 1 only the first is correctly typed by PEP 484. mypy rejects the second with “error: Invalid type comment or annotation”. That’s the whole idea of static type checking: in return for restricting yourself to a controlled subset of the language that isn’t “too dynamic”, you gain the ability to type-check your code without running it. The result of this paper is that one can nonetheless abuse subtyping to perform Turing-complete computation in the type checker. The computation doesn’t happen when your code is executed (annotations have no effect on the Python interpreter at runtime unless your program chooses to inspect them), it happens when you run mypy on it. This is generally considered undesirable, because we want type checking to be decidable, and Turing-complete computation is not.

eru 4y ago
> That’s the whole idea of static type checking: in return for restricting yourself to a controlled subset of the language that isn’t “too dynamic”, you gain the ability to type-check your code without running it. Eh, you are mixing up distinctions. All that's required of _static_ typing is that your static type specification finishes running before you start your program. Whether that static type specification language is Turing complete or not is a completely separate issue. And, yes, you are right that it's generally useful for that language to be decidable. But see eg Haskell's UndecidableInstances.
BiteCode_dev 4y ago
That's why my comment litterally starts with "even before talking about the typing system itself".
- anderskaseorg 4y ago
  I’m sure that you understood the important differences, but there are likely many readers who didn’t (many more programmers are familiar with Python than with mypy). When you write “even if we don’t have P, we’d have Q anyway”, the reader is left with the impression that P and Q are somehow interchangeable or equivalent or comparable—that P is unimportant in the presence of Q. I think it’s instructive to point out that this impression would be mistaken, and the paper’s result of P is interesting and consequential.

eru 4y ago

> That’s the whole idea of static type checking: in return for restricting yourself to a controlled subset of the language that isn’t “too dynamic”, you gain the ability to type-check your code without running it. Eh, you are mixing up distinctions. All that's required of _static_ typing is that your static type specification finishes running before you start your program. Whether that static type specification language is Turing complete or not is a completely separate issue. And, yes, you are right that it's generally useful for that language to be decidable. But see eg Haskell's UndecidableInstances.

BiteCode_dev 4y ago

That's why my comment litterally starts with "even before talking about the typing system itself".

anderskaseorg 4y ago
I’m sure that you understood the important differences, but there are likely many readers who didn’t (many more programmers are familiar with Python than with mypy). When you write “even if we don’t have P, we’d have Q anyway”, the reader is left with the impression that P and Q are somehow interchangeable or equivalent or comparable—that P is unimportant in the presence of Q. I think it’s instructive to point out that this impression would be mistaken, and the paper’s result of P is interesting and consequential.