@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

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

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

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

@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

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

@xgranade @whitequark I'll have to think more about the shortcuts other checkers take to see if they can be convinced to do something similar but less obvious.

I understand now why this doesn't bother me: I came to Python from a combo of Perl and Lisp (sort of) and it drove me crazy for the first few years; it was too principled to really have Perl vibes but too loose to be a Lisp even though it seemed like it wanted to be one. Stuff like 'why isn't `if` an expression' seemed like a mistake

@xgranade @whitequark eventually I realized that it wants to be what it is, which is kind of mostly a lisp-1 with a bunch of weird caltrops to prevent technically-correct but bad-for-maintainability stuff in a way which is mathematically unprincipled but probably the right call. "We all know -> None means void even though : None doesn't" is one of those annoying "wrong" edge cases I just learned to accept forever ago.

But characterizing Mypy as a "type-aware linter" as a result, is fair

@glyph @whitequark "mathematically unprincipled but probably the right call" That's the core of what bothers me, yeah. A type system is, by definition, a system of mathematical rules. If it's mathematically unprincipled, no matter how well motivated it is, it's not a type system.

(As a side note, `-> None` being an idiom for `-> NoneType` doesn't bother me... having a useful shorthand is not inconsistent with formal reasoning. Accepting `-> None` and rejecting `-> NoneType` is just *weird*.)