> If your statement were absolutely true then a product like mypy would neither exist nor provide value.
I don't see why that would be the case. The value of Mypy is that it's essentially a proof language over something that resembles Python[1]: it's a way to do some amount of static typing without having to maintain a separate copy and representation of the program.
And sure: Python could detect inconsistent type hints at runtime. But why would it? It's already strongly typed, and the presence of type hints usually means that someone is already running Mypy or another checker during development. It's not clear that there's a significant advantage to be gained, particularly one that justifies the additional overhead.
[1]: "Resembles Python" because mypy does not actually evaluate any Python. It doesn't know what types your program has at runtime; it only knows type hints and a few small rules (for things like string literals) and trusts the developer to reconcile those rules with Python's runtime behavior.
Do you think other languages should do the same, because very few do any kind of runtime type checking (e.g. bounds checking) due to the performance penalty. Why focus specifically on python's lack of runtime type checking?
Anecdotally, my code in python is functionally fully typechecked and runtime type checking would solely penalize me by slowing down my code. There's no need for it because the type checker correctly proves the soundness of the program's types, in exactly the same way that Java's or C++'s do.
The point is precisely that you don't need to suffer the costs of runtime type checking if you have a solid typechecker. Lisp's approach here is worse than the one adopted by python/js/ts/go/etc.
I don't see why that would be the case. The value of Mypy is that it's essentially a proof language over something that resembles Python[1]: it's a way to do some amount of static typing without having to maintain a separate copy and representation of the program.
And sure: Python could detect inconsistent type hints at runtime. But why would it? It's already strongly typed, and the presence of type hints usually means that someone is already running Mypy or another checker during development. It's not clear that there's a significant advantage to be gained, particularly one that justifies the additional overhead.
[1]: "Resembles Python" because mypy does not actually evaluate any Python. It doesn't know what types your program has at runtime; it only knows type hints and a few small rules (for things like string literals) and trusts the developer to reconcile those rules with Python's runtime behavior.