The compilation step in static languages type-checks such that the compiled-instructions wont run if the source-code is invalid.
Since this isnt how python works, one would reasonably expect the spirit of a type system to be preserved -- ie., to enforce runtime checks.
> The compilation step in static languages type-checks such that the compiled-instructions wont run if the source-code is invalid.
Nothing is forcing anyone to run code that does not pass type checking with `mypy --strict`.
> Since this isnt how python works, one would reasonably expect the spirit of a type system to be preserved -- ie., to enforce runtime checks.
Python already had mechanisms for this, which again, as I said, already informs the static type checking mechanisms.
Also, no, this is not what I expect from the type hints, this is not what I felt was missing from python before type hints.
What I want from type hints and in python in general is static type checking, I want to know, without executing one single line of code, if I have type errors, that is the key selling point of mypy and type hints to me and the key deficiency that python had without type hints and mypy.
I already had every ability to do runtime type checking in python before type hints and mypy, and they were woefully inadequate in comparison to static type checking.
Are there still mistakes in the typeshed like 2**-1 is int?
There are type hints for the standard library and using `--strict` works just fine if that is all you are using. This does not preclude bugs from the standard library or errors in types but bugs in a statically typed language's compiler also does not defeat the purpose of static typing either and having a static typed language does not eliminate the possibility of bugs in the compiler or standard library either.
It seems people forget that reinterpret_cast, void * (c++), Object (java), (interface{}) (golang) exists. If all you are using is the standard library then you will be able to write much safer code in python than in golang, given it passes static type validation. At least python's type system has generics.
> Are there still mistakes in the typeshed like 2*-1 is int?
I'm sure there are still mistakes, just like I'm sure there are still bugs in most compilers.
There's also something about 'soundness' one could say.
Type systems are decidable and thus cannot, by definition, rule out all errors. Instead, they look at a subset of possible errors. This subset is provably eliminated from valid code. "Dynamically typed" languages reduce that subset to the empty set.