> In what reasonable sense can Python be said to "enforce statically declared types at runtime" here?
It can't, because Python doesn't have statically declared types. It's a strong, dynamically typed language.
Python also doesn't allow you to declare static types. It allows you to declare type hints, which are a sort of adjacent and potentially unrealistic (or just plain incorrect) typechecking proof that doesn't correspond at all to runtime behavior.
If your statement were absolutely true then a product like mypy would neither exist nor provide value.
Python has the capacity to have some form of gradual typing built-in at the language level, but it does not, which has led to the enormous confusion we have before us. The SBCL implementation of Common Lisp is a great example of a strong, dynamically typed language that is able to, when possible, detect errors statically at compile time. That tech is 30 years old now.
There is no reason why the Python bytecode compiler could not statically or dynamically detect this programmer error at either compile-time or run-time present in this statement:
x: int = "x"
Compare to Common Lisp, well known for being dynamically typed (so dynamic that it's possible to change the class of an object at run-time!):
(declaim (type integer x))
(defvar x "oops")
; ==>
Unhandled SIMPLE-TYPE-ERROR in thread #<SB-THREAD:THREAD "main thread" RUNNING {10005D05B3}>:
Cannot set SYMBOL-VALUE of X to "oops", not of type INTEGER.
quitting
compilation unit aborted
caught 1 fatal ERROR condition
Instead, this job in Python is haphazardly relegated to the program readers and IDE implementers.
> 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.
It can't, because Python doesn't have statically declared types. It's a strong, dynamically typed language.
Python also doesn't allow you to declare static types. It allows you to declare type hints, which are a sort of adjacent and potentially unrealistic (or just plain incorrect) typechecking proof that doesn't correspond at all to runtime behavior.