fyrfaras@Elizafox @whitequark @imbl Alrighty, thank you for explaining it to me. ^^ Also I just read a toot thread, below, by @xgranade that mypy doesn't use “mathematical type checking” but rather “linting heuristics” which could lead to this bad reputation you've mentioned earlier I think.
Cassandra is only carbon now (@[email protected])
As I mentioned earlier, it's a bit more difficult to have good exit strategies with ruff, given that the specs around linting are much more loose. It's even harder to have a good exit strategy for ty, even though there's good specs, because there's not a great type checker to use instead¹. ___ ¹As has been pointed out to me, mypy is, for all its strengths and weaknesses, not a type checker. It doesn't follow formal mathematical type checking rules, it follows linting heuristics.
Cassandra is only carbon now@fyrfaras @Elizafox @whitequark @imbl Like, I'm not trying to be petty or sarcastic about it. Rather, it's that I think some of my earlier (and admittedly a bit toxic) hate of mypy came from deeply misunderstanding what mypy is and is trying to do. I would have expected from docs and the description, that mypy accepts well-typed programs and rejects programs that violate typing rules — but that's not it. It rejects well-typed programs that are likely incorrect, which is what a linter does.
@fyrfaras @Elizafox @whitequark @imbl In particular, I cannot predict the behavior of mypy given knowledge of Python's type system alone. I have to know about what is and is not likely a logic error in Python.
Which is fine if you want a somewhat more rigorous linter that has the benefit of being developed under the auspices of the PSF itself. But it's not what I want or would want out of a type checker.
✧✦Catherine✦✧@whitequark @fyrfaras @Elizafox @imbl Agree, absolutely.
I made the mistake of thinking of it as one for a long time, but I have been disavowed of that notion.
@xgranade @fyrfaras @Elizafox @imbl however the problem is that the mypy website has this misinformation on the landing page
@whitequark @fyrfaras @Elizafox @imbl Ooof, yeah. Were I in the mood to start useless fights, I'd be tempted to PR a change to that page, but it'd just get people hurt for no reason.
I mean, it just isn't a type checker. That's not what it does.
@whitequark I guess part of it is that I'm trying to reconcile "cool people that I think well of work on mypy" and "mypy is manifestly unfit to serve as the thing it advertises itself as." For me, that comes down to trying to understand what mypy *is* for if it's not the thing it's billed as, if there's some kind of semantic drift there.
Were I to make that PR as a frequently loud critic, I don't think it'd come across in good faith, and, well, fair enough.
@xgranade well. how to put it. I don't care how it's fixed, just that it is
@whitequark That's completely fair.
Glyph@xgranade @whitequark I'm still not really clear on why the incorrect simplifying assumptions about python's runtime that ty makes are just the practical compromises of a sound type checker but the incorrect simplifying assumptions that mypy makes put it in an entirely different category of software
@xgranade @whitequark like "too much busywork for the amount of bugs it finds" is not an experience I have had, but we write very different kinds of code so I'm definitely not arguing with that; I could see that 'ty' or 'pylance' might do far better with your code, or might even have a more rigorous approach to certain aspects of their type algebra. but all three happily give this program (and many like it) the thumbs-up:
x = 1
y = 2
locals()['y'] = 'oops'
print(x + y)
@whitequark @xgranade this is actually why I prefer mypy, specifically because (via plugins) it can accept an extension to the type system implemented with runtime hackery, and handle Zope Interface, while none of the other ones can. pydantic also has a similar thing (and dataclasses were originally supported via the 'attrs' plugin, although everybody else eventually got on board with those).
but I guess when it comes to "helpful" warnings, mypy probably does produce a lot more of those
@whitequark @xgranade in any case, I absolutely understand “the experience of using this sucks”, I just don’t get the category distinction
@whitequark @glyph Sorry, was on a StS2 run, heh. Anyway, my understanding of the difference is that sometimes, when you report a false negative in mypy (that is, a program being rejected despite being well-typed), the response is "well, don't write that program." I struggle to put into words how off the mark that is for a type checker, but it's perfectly sensible for a linter.
@xgranade @glyph a type-checker that rejects well-typed programs is by definition buggy. if it's not fixed then it is unfit for purpose
we could have a broader discussion of what "well-typed" means for Python (it is not clear to me at all) but if the above is an accurate assessment of the consensus in mypy development then it is not a(n even aspirationally correct) type-checker
@whitequark That's what I'm getting at, yeah. For a piece of software to be a type checker, there should not be a single case *ever* of a well-typed program that is rejected *by design*.
@xgranade @whitequark do you have a canonical example of such a WONTFIX?
```
def f() -> None:
return
y = f()
```
main.py:4: error: "f" does not return a value (it only ever returns None) [func-returns-value]
Found 1 error in 1 file (checked 1 source file)
@xgranade @whitequark heh. fair enough I guess, although I am tempted to troll “that’s totally a valid type check once you realize that in certain contexts None means ‘null’ but in others it means ‘void’ “
(formally speaking, -> None is already lightly gibberish as it is an unprincipled pun for NoneType; but in support of your point, ty does accept NoneType but Mypy doesn’t)
@glyph @whitequark But that's my point... Python doesn't even have a void, but mypy acts like it does!
```
from typing import Any
def f() -> None:
pass
y: Any = f()
```
Assigning a value to a variable of type `Any` should always be allowed. That should be true in any gradually typed system.
@glyph @whitequark By way of getting at what I mean about expecting there to be rules I can follow, one of those is that if `x = y` typechecks, then `f = lambda: y; x = f()` should also type check.
That doesn't hold, though:
```
from typing import Callable
f: Callable[[], None] = lambda: None
y = f() # error
x: None = None
y = x # ok
```
That means I cannot in general refactor by extracting a value into a function that returns that value, which breaks the whole idea of a type system.
@glyph @whitequark Anyway, sorry for the long reply, but I guess the short version is that I don't think any of the above behavior is consistent with a type system, but it can be consistent with a linter.
That is, knowing the types of a program in Python is not sufficient to know if that program will pass mypy. I have to know about the context in which those types are used, which breaks the abstraction entirely. It makes mypy take on a *much* higher cognitive load.
@xgranade @whitequark No apology necessary whatsoever for a long reply, I asked a complicated question!
@xgranade @whitequark Would you consider pyright's reportSelfClsParameterName warning to also be a violation of this same rule?
@xgranade @whitequark or like… this? https://docs.astral.sh/ty/reference/rules/#ambiguous-protocol-member
that looks a lot like linting
@glyph @whitequark I don't think that's a linting at all? It's saying that type *inference* is disabled in a given context, but if you explicitly specify the types then it will work. That's fairly common (hell, even Rust has it, and it's got about the most formal type system I've seen in an imperative language) at interfaces between code.
Even then, to @whitequark's point (beat me to it), warnings are one thing but *rejecting* a well-typed program is one thing a type checker should never do.
@xgranade @whitequark okay perhaps a clearer "definitely not type checking" one would be https://docs.astral.sh/ty/reference/rules/#deprecated but yeah
mypy doesn't even have a concept of a "warning", I guess, is the problem? It has categories you can enable and disable but they're not grouped together like this
@glyph @whitequark That is type checking, though. Deprecation information is stored in the `__deprecated__` attribute, and the existence of protocols means you can have a protocol that matches the existence of that attribute (as another aside, it's the only existence of a negative type in Python, so that's weird, but a weird type is still a type).
The problem with the `y = None` vs `y = (lambda: None)()` is that in both cases, `y` has the exact same value but mypy only raises on the second one.
mal3abyI don't think that's quite the issue it has, though?
```
y = None
y = (lambda : None)()
Success: no issues found in 1 source file
```
The problem seems to be more that, in certain contexts (after -> and on the RHS of Callable) it interprets the `None` shortcut (and certain synonyms) not as `NoneType`, but as a sort of `PseudoVoid`.
Not saying that's a good thing (nor is its behaviour 100% consistent), but it's possibly more amenable to formal reasoning?
I was abbreviating a bit given the context of the whole thread, but a more complete snippet shows that the problem happens when mypy knows the return type is `NoneType`. Otherwise, it treats the return of `(lambda: None)()` as an implicit `Any`.
```
from typing import Callable
y: None
f = lambda: None
reveal_type(f) # prints `def ()`
y = f() # ok
g: Callable[[], None] = lambda: None
y = g() # errors
x: None = None
y = x # ok
```
@mal3aby @glyph @whitequark As an aside, I have no idea why mypy infers the type of `lambda: None` as being `def ()`, nor why ty completely fails to infer the type and just judges it to be `Unknown`, but a failure in type inference that fails open (that is, to an imprecise but correct type or to a marked failure) is at most a feature request rather than a bug or a design flaw.
Type inference is somewhat distinct from the type system itself.
@xgranade @glyph @whitequark Yeah, `def ()` seems to be its way of spelling (unhelpfully) both `Callable[[], NoneType]` and `Callable[[], PseudoVoid]`, which can only add to the confusion. (I suppose there is some sort of symmetry to performing a transformation to the output that's the reverse of what's performed on input, but in this case I can't see a benefit, and the downsides are obvious.)
@mal3aby It's closer to Callable[[], Any], otherwise it would fail for the same reason. But how mypy handles the relationship between Any and the unnameable void is not only inconsistent with being a type system, it's also inconsistent with Python's documentation on how Any works, or how gradual type systems work in general.
@xgranade
This is not entirely theoretical - if you define
```
from typing import Union
ActualNoneType = Union[None, None]
```
then I think your examples from the thread mostly work (putting ActualNoneType where needed) - except that now it will insist that `return` becomes `return None`. Which I guess *might* make sense, if you accept the whole questionable premise the whole thing is based on (with `return` meaning `return PseudoVoidUnitValue`)?
This is not entirely theoretical - if you define
```
from typing import Union
ActualNoneType = Union[None, None]
```
then I think your examples from the thread mostly work (putting ActualNoneType where needed) - except that now it will insist that `return` becomes `return None`. Which I guess *might* make sense, if you accept the whole questionable premise the whole thing is based on (with `return` meaning `return PseudoVoidUnitValue`)?
@mal3aby It's absolutely cursed that that works, but that just makes the point even more clearly that it's not really a type checker? `Union[A, A]` should never be treated differently than `A`, that it is indicates that mypy is sensitive to how a type is expressed rather than to the type itself.