Type hints in python are _just that_, they're hints. The whole "typed" python ecosystem relies on packages and the language using them, using them correctly, and using them consistently. In my experience so far, I've seen little widespread use, and nothing from core python, which is a huge hole IMO.
Note that you don't include the most common static languages there (cpp, java, golang), you include languages known *specifically " for their extremely powerful type systems, one of which , just like mypy, uses gradual typing!
This supports my argument!
> one of which , just like mypy, uses gradual typing!
This is like arguing that because your scooter also has a petrol engine, it’s as fast and efficient as an F1 car. My argument was that MyPy doesn’t compete with the capabilities of modern statically typed languages. TS might also technically be gradually typed, but most devs I know just go straight to fully typed TS, because working in a mix/gradual environment is painful and the community uptake of strict types is far higher.
I can name dozens that python has that Java doesn't. My point is that if you include cpp or java or golang the statement becomes false. Python's type system is actually generally speaking more robust than those (cpp is comparable, but I don't think python's is worse).
So I'm asking, be specific what capabilities does mypy lack that cpp or java or golang provide? Keep in mind, mypy supports literal types, limited dependent types, dynamic-duck typing (protocols), limited contract types, and more. Java doesn't, go doesn't. Cpp supports some of those but it requires arcane incantations.
that must require some advanced usage of mypy then, because my experience was that even the most simple example got the finger from mypy that would have very obviously worked in Java
mkdir alpha
echo 'beta = True' > alpha/models.py
echo 'from .models import beta' > alpha/__init__.py
echo 'import alpha; print(alpha.beta)' > doit.py
mypy --strict doit.py
# doit.py:1: error: Module has no attribute "beta"
And indeed[0] that's the case. It makes perfect sense that the abstract machine of typed python does not allow everything that the abstract machine of untyped python does, and java would error on trying to use a private class or method just the same.
[0]: https://mypy.readthedocs.io/en/latest/command_line.html#cmdo...
The point of a sound static type system is that you get a guaranty that your program is type-safe even in case not everything is "hinted properly".
With the linter approach on the other hands side it won't get better than what a dynamic language offers anyway: To be (more or less) sure everything is like intended all you can do is to run your program and pray… You can't upfront rule out for sure all kinds of errors like when using a proper static language.
Of course an external tool could model and check against a proper type system, in theory. So that's indeed not the point.
A proper static type system comes with a formal definition and (math-like) proves of soundness (and progress). This will give you the guaranty that a well typed program is sound.
A "linter" can't give you that guaranty. All it can do is to say "LGTM"; but your program could still crash or bug-out in some other way at runtime. That's quite a big difference imho.
Linters are more like automated tests: They may tell you something is wrong, but they don't give any guaranties that things are actually right. A proper static type system OTOH gives such guaranties.
For example I would consider TypeScript being only a very funky linter—as it does not model a sound type system. My understanding is that mypy and friends are not different. All those linters produce not only way to much false positives, no, they also produce false negatives (meaning that they let unsound programs pass; something that can not happen with a formally verified type system).
As an anecdote, I got bitten by that when trying TS (and it was a very sad experience): When playing around with TS for the first time I did not know that TypeScript is barely a linter. I was really very excited about all those things you can do with proper structural types there! I was coming from Scala 2 which has only very limited support (based on JVM reflection) for this kind of types¹. But I always loved the "objects as hash-maps" concept of JS… So I've written some small REST client for one of our back-end services in TS. Everything nicely typed, no escape hatches used. Someone also told me I have to use "stric mode" which will "catch all type errors". That looked a bit odd, but OK JS was not made to be typed in the first place. Everything looked great than. As someone coming form the purely functional Scala camp (where things work when they compile :-D), and encouraged by all those people praising TS for its "powerful type system", I've put the same amount of confidence as in Scala into the typed code I've written in TS. By this I mean you don't need to double check whether things are correct if the typer says they're correct. It's enough to check the logic of your program. You don't have to try out "manually" (this includes written tests!) every line of code. Up to than everything looked good. So I've pushed things and started to do end-to-end test. That was when I fell out of my dress. My code produced runtime errors which where actually "impossible"! The TS "type-checker" said things are such and such but at runtime they were different (which I found out only after some deep debugging sessions as this was something I did not expect in any way)! I think I've wasted one and a half day debugging this shit only to find out that TS "types" are actually worthless. If I have to try out any and every line of code manual anyway what's the point of TS? I could have written this thing in pure JS (where I have to also check any and every line manually), but it would have been much easier without "wrestling" with that quite useless "type system"… :-(
The point is: A dynamic language remains a dynamic language even if you use some linter! Without true guaranties you can't have much additional confidence in your code without testing just everything—even the parts that were already "tested" by our "type system". Actually it's even worse than without a linter if you don't know about its shortcomings and make the mistake to blindly trust such a tool; like you can do in case of a sound type system (modulo the very seldom cases of compiler bugs).
I hope I could make it now more understandable what I mean by "proper static type system".
___
¹ Things improved in Scala 3 though.
I'm pretty sure the mypy and typescript devs would disagree here. The typescript and mypy abstract machines aren't any less sound than Java or c++.
All four are abstract machines that make fundamentally similar guarantees. Cpp and Java can still encounter classcast exceptions and segfaults.
And, like, you still need tests in functional languages. Specifically, I don't think I've encountered anything like
> My code produced runtime errors which where actually "impossible"! The TS "type-checker" said things are such and such but at runtime they were different
Without either explicitly subverting the type system, or dealing with some kind of untyped deserialization along an api boundary, which you absolutely need to test in any language.
I only wanted to point out once more that a proper static type system is of more use than some bolted on linter. (And add the point about type inference).
I don't disagree, but that's not an argument I ever put forth! (and I actually sort of disagree a little bit, mypy has/is getting a bunch of really cool powerful features that put it in the realm of "as cool as" those languages: PEPs 544, 586, 591, 647 (this is a weak form of contract types!), 675 (~constexpr string type), 646 (variadic generic/numeric dependent types!))
Kinda silly that this is optional tooling that came from the community to solve a problem in the original implementation.
Sure, having a community and general inertia, because Python is simply good enough and no alternative has a killer feature, is certainly something you can rely on. It's okay to ask for more, though.
This is literally what mypy does.
There's no difference between a mypy-enabled codebase and a java codebase in terms of static typing (other than that mypy actually supports a generally richer type system).
Like yes if you aren't validating the type hints you aren't getting the value, but if you are, you don't need to run the code! I get most of my python errors at compile time, and you can too. I promise.