@fyrfaras @whitequark i just saw >:/

yay! im so excited to "sloppercharge my productivity" or whatever!!!

although i do love the irony that astral's repos use claude. really shows how full of shit they are when their announcement is sucking up to openai's codex but they're using a competitor's slop machine. definitely not just showing a complete lack of values lol

@imbl @fyrfaras @whitequark not a huge surprise sadly, anyone who’s used Python has seen this coming ever since the big data then the LLM researchers got interested in Python.
@Elizafox @imbl @fyrfaras astral's tools (fast typecheckers, etc) are also well-suited to the problem of "shove lots of garbage into the typechecker, see what sticks"; this isn't unique to astral (rust-analyzer is also good for it), astral just happened to accept a buyout at an opportune time

@whitequark @Elizafox @fyrfaras mmmmmm type-safe slop

ive used mypy enough to know that this is going to fail hilariously the first time it encounters wrong or poorly-typed interfaces >:3c

@imbl @Elizafox @fyrfaras i refuse to use mypy because mypy-flavored typing is a net negative to doing programming

@whitequark @Elizafox @fyrfaras fully agree. mypy sucks but its what i learned and its got all the plugins, plus i never got pyright working

i was actually planning on switching to ty for my next project  

@imbl @Elizafox @fyrfaras i'm using pylance, so the slop factor is the same as for ty
@whitequark @imbl @Elizafox I sea, could you please elaborate why mypy is a net negative for programming? ^_^
@fyrfaras @imbl @Elizafox it creates far too much busywork for the amount of bugs it finds. this has the added effect of giving python typing a bad reputation
@whitequark @fyrfaras @imbl I like mypy but I get some people prefer Python to be properly dynamically typed (that’s fine too).

@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.

https://wandering.shop/@xgranade/116259906731072162

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.

The Wandering Shop
@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.

@xgranade @fyrfaras @Elizafox @imbl so this makes sense but it is a profound failure of communication then that anyone calls mypy a typechecker

@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.

@xgranade @fyrfaras @Elizafox @imbl well then I'm sure one of the people who like mypy here can fix it!

@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.
@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)

@glyph @xgranade i personally object to accepting too few programs, not too many
@glyph @xgranade there's a bunch of fine points about different programs but /bin/true to me is a valid and useful python typechecker in a way mypy isn't (and pylance is closer to /bin/true on this scale, in some configurations at least)

@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

@glyph @xgranade i need this (pluggability) for amaranth... but because using mypy makes me miserable amaranth is simply incompatible with every typechecker instead
@whitequark @xgranade in any case, I absolutely understand “the experience of using this sucks”, I just don’t get the category distinction
@glyph maybe it doesn't exist, i took @xgranade at her word
@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?

@glyph @whitequark

```
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?
Rules | ty

ty is an extremely fast Python type checker.

@glyph @xgranade it is normal for a typechecker to include linting rules at the "warn" level. i mean even gcc has those

what is not normal / problematic for me in this context is having those be hard-rejects. "someone dreamed up a rule out of vibes and now i have to mangle perfectly well-formed code" is not something i accept

@glyph @xgranade if gcc shipped with -Werror enabled by default i would have a problem with that too!

@whitequark @glyph Part of the ergonomic difference for me is that I do run ruff (sigh) with warnings as errors. Sometimes that results in false negatives (programs rejected that are valid). In those cases, I can leave a # noqa comment indicating why. 90% of the time that's an unused import that's actually used but it doesn't detect it, though I digress.

Declaring something as Any should be the polite way to spell "fuck off, type checker" but even *that* doesn't work in mypy... hence mangling.

@xgranade @glyph (for comparison, I have ruff configured to explicitly disable the noqa comments because my position is that if you need them, you should fix or disable the entire check instead. I do have a few file-level exemptions for like generated files that are checked in)
@whitequark @glyph That's fair, yeah. I think it's a difference in assigning false positives versus false negatives, but regardless, in either case, we're each making active decisions about how to use data that's noisy by necessity.
@xgranade @glyph there is a bit of that, but it's incidental; my broader position is that the tool should bend to my whims, not the other way around

@whitequark @glyph I think we have different philosophies on that, yeah... not even that I disagree, I just think of it differently? I'm happy working within what a tool wants me to do, it's something my mathy brain is OK with. Just tell me the goddamned rules.

Whereas that's something mypy does not do. The rules are, to your earlier point, vibed up.

@xgranade @whitequark Would it change your opinion if mypy categorized all its "linting" stuff in a way that made it possible to disable at one go, in the way that it seems like most of the "lint" stuff in ty is classified? Rather than having specific categories and then the generalized ad-hoc "strict" category?
@glyph @xgranade provided this was a part of a broader philosophical commitment to develop it as specifically a type-checker, maybe? I would try it again at least
@whitequark @xgranade what else would make it "a type-checker" aside from its misclassification of warnings-as-errors, though? I thought I had gotten my head around this :)
@glyph @xgranade I mean I don't want to deal with like two factions of mypy developers disagreeing how rules should be classified and the resulting release-to-release churn that I can see this resulting in
@whitequark @xgranade ah okay. if such a category were added then the entire point of it would be to have a principled distinction. you can already configure whatever categories you like otherwise

@glyph @whitequark The big one: there need to be rules that allow me to predict its behavior, and those rules need to be rules that are only sensitive to type judgments, *not* out-of-band contextual information.

If I can keep the types of a program invariant, and get different behavior depending on how I express values of those types, then the system isn't just checking the types.

@glyph @whitequark I mean, the example in question is ill-considered in the first place, I think. It's saying that I can assign a value to a variable in some cases but not others, even when the types are held invariant.

That aside, I think if mypy stuck to the documented rules of how Python types behave, *or* didn't call itself a type checker, I'd be much happier. Downgrading ad-hoc errors like func-returns-value to warnings is a good step towards that.

@xgranade @whitequark Would you see https://docs.astral.sh/ty/reference/rules/#invalid-total-ordering as something that should be a 'warning' too?
Rules | ty

ty is an extremely fast Python type checker.

@glyph @whitequark Nope, that's a very clear type error. @functools.total_ordering expects input that meets a protocol. That error is raised on inputs that do not meet that protocol, irrespective of how I write those values.
@xgranade @whitequark the fact that the type checker contains custom logic for this one protocol that isn't expressed in the type signature isn't an issue?

@glyph @xgranade ad-hoc logic like this is expected (and, probably, outright required) to retrofit a language like Python with types, yeah

TypeScript does this a lot also

@whitequark @glyph (Separately, that TypeScript decided on explicitly unsound behavior is maddening.)

@glyph @whitequark I don't think so, no... it's a documented behavior of @functools.partial_ordering. In general, one of the main things that typing in Python does is formalize those kinds of requirements. That's basically a typeshed for the stdlib at that point.

The difference is that it doesn't matter how I get the class that violates the protocol, only that it does indeed violate it.

@glyph @whitequark (There's separately a question as to whether the explicit or implicit typeshed is accurate, but I'd consider that to be a bug that I hope would be fixed. Hell, I'd consider mypy's None handling to be a bug if it wasn't a wontfix.)
@xgranade @whitequark does mypy do this with types *other* than None, too? I was joking about 'void' but if this is really the one special case, it seems like that really might be what's going on

@glyph @whitequark I've definitely hit some, and should have written them down...

But yeah, None is one of the worst culprits. I see a lot of unit-vs-void confusion in GitHub issue threads, which doesn't inspire confidence that there might be a consensus to be found around mypy adopting a formal type system such as the one documented at docs.python.org.

Error codes enabled by default - mypy 1.19.1 documentation

@glyph @whitequark Oh, yeah, definitely. It's perhaps imprecise to say `False: bool` when you could say `False: Literal[False]`, but it's not incorrect.
@glyph @whitequark Weirdly, the docs on that hint to a resolution: "yeah, this isn't strictly a type check, but that's a structural limitation of how mypy works with its current infrastructure, and we hope to fix that in the future." I'd be OK with that, then to @whitequark's point it's at least *aspirationally* a type checker even if it doesn't get there. The WONTFIX is really what drives me nuts.
@glyph @whitequark Every type checker will have some bugs or limitations, that's not surprising to me... it's that when one is found, it gets labelled as wontfix bydesign.

@glyph @whitequark The problem with my original counterexample is that *in both cases* `y` has the exact same type and is assigned the exact same value, but I get different behaviors from mypy depending on *how* I obtained that value.

Maybe put differently, a substitution principle that I would expect to hold is that if `reveal_type(expr1)` is the same as `reveal_type(expr2)`, then substituting `expr2` for `expr1` should never cause *or resolve* a type error.

@xgranade @whitequark is part of the impedance mismatch here because mypy does a poor job of communicating that it is not necessarily type checking Python, but rather type checking for the purpose of mypyc? I think that at least explains the void-like return value example earlier.

@whitequark @glyph I don't know what it says about me, but one of the most deeply frustrating experiences I have with computers is when something tells me a thing is true, I believe that to be the case, act accordingly, and get a face full of dirt for my troubles.

mypy is fine for what it is, but it's just not a type checker.

@xgranade @glyph I despise seeing the # noqa comments. they're pure noise; if a tool was better they wouldn't be needed, so I object to their presence out of principle (and eradicate them by following said principle)
@whitequark @xgranade @glyph in python, unused imports is one that you sometimes need to noqa, because sometimes importing modules has side effects, like registering handlers. in general I do want unused import lints, but you have to disable it for those libraries you just import for the side effect
@unlambda @whitequark @xgranade I have adopted the idiom of doing '__import__("module_with_side_effects")' to indicate that I'm doing the import for the side effects, by discarding the resultant unused import. Linters generally don't mind that.
@glyph @whitequark @xgranade Huh, never thought of that, interesting idea.
@xgranade @whitequark type:ignore[category] scratches that itch on a practical level for me. (I actually use these instead of casts because casts have the tiny runtime overhead of 2 extra unnecessary name lookups.)
@whitequark @glyph @xgranade One day, I had access to Klocwork static code analyzer, as part of bigCorp.
Our management insisted that all issues be resolved. Really silly ""memory-safety" stuff" that involved thousands of code line changes to resolve. Too many changes for the change board to accept for production.
Then, I ran the Klocwork tool against the underlying ARM/linux kernel and userland build, and there were too many violations to count.
Nobody was worried about that.
@whitequark @glyph @xgranade This taught me a lesson. Though I will take your money, I don't want to waste my time, or yours. Time is money.
If my boss asks me to solve a problem, I have to now ask "if I do this, will the organization ship it to prod ?" Because if not, we can skip it.
It's surprising that the boss or "stakeholder" does not ask this herself, but I'm paid to use my entire brain, or none of it. Your choice.

@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

Rules | ty

ty is an extremely fast Python type checker.

@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.