Should type(x) == T result in narrowing? (Is type(x) is T better?)

Typing
1

Consider the following two functions:

def assert_int_eq(num: object) -> int:
    assert type(num) == int
    return num

def assert_int_is(num: object) -> int:
    assert type(num) is int
    return num

As far as I can tell, most major type checkers think both of these are valid. Specifically, mypy, Pyright, and Pyrefly all mark them as okay. However, ty does not - by design, since metaclasses can override __eq__. I’m intrigued by that reasoning, but __instancecheck__ and __subclasscheck__ also exist…

Narrowing is (intentionally) left pretty open to interpretation, but this is a pretty visible divergence, so I think it’s at least worth discussing - is it reasonable for type checkers to narrow after a type(x) == T check? Is a type(x) is T check preferable?

This is of course only in the rare instance where you actualy want type and not isinstance.

3 Likes
2

I don’t think I considered metaclasses when implementing that feature for Pyrefly, but in general refinement has a bunch of unsafe behaviors already so this seems like just another safety/practicality tradeoff

1 Like
3

Any subtlety behind needing this over isinstance merits a comment or two, but I feel like the intention behind the code is crystal clear.

It would be better if ty checked first, and scanned to see if the instance’s metaclass did anything weird like overriding __eq__ (and even if it warned about anything like that of the sort) before deciding not to narrow the type for non-metaclass using code.

1 Like
4

I ran into the same issue while working on my suggestion for higher kinded types. I think a good note is that type(x) is something that specifically breaks Liskov’s Substitution Principles, as it is a detection of runtime type (more exactly, if I understand well, type(x) returns the constructor that was called to instantiate x). In clearer terms, it means that if you have S <: T and x : S, well, type(x) == T will fail, although theoretically x is a T because of subtyping, and so subtyping shouldn’t change the code behavior.

What this implies is rather complex to me, because I do see use cases of type(x) == T. My take here is that such expressions shouldn’t play in typing as defined for now, because it does not respect the asumptions of typing, and break the guarantees of it. Python being type-optional means types shouldn’t restrict the code that can be run, so this code has to be allowed in untyped Python.

Hence, if you want to take this code to type checking, you need to come up with a different definition of types, something that isn’t 100% based on LSP. I’m heading in this direction personally, but the work is rather tough as type theories were never made with Python in mind. However, it doesn’t seem impossible as I feel like after a few months, I’m finally nearing a definition that feel satisfying (however, I still need to check if it’s sound, if it breaks things in Python etc).