We need a better story about Any

[ilevkivskyi]

While working on protocols, I noticed that stubs often use Any where object will be more appropriate and vice versa. Because of how protocol inference works and how current mypy solver works, this leads to problems since sometimes mypy infers Any instead of giving an error (maybe we could improve this by "tightening" solver?)

I think the root of the problem is that wee don't have a good story about Any. I believe the rules for interaction between Any and other things should be like this (where C is a normal class like int or str):

(1) join(Any, object) == object
(2) meet(Any, object) == Any
(3) join(Any, C) == C
(4) meet(Any, C) == C
(5) join(Any, NoReturn) == Any
(6) meet(Any, NoReturn) == NoReturn

I use NoReturn for uninhabited type, since it is how it is currently called in PEP 484. The above rules could be summarized in a simple diagram:

        object
          |
         Any (if it appears in a meet)
        / | \
... all other types ...
        \ | /
         Any (if it appear in a join)
          |
       NoReturn

Currently, mypy behaves in a completely different way, and I believe this is not right, let me explain why. We could focus on rules (3) and (4). Currently, mypy returns Any in both these cases. Here is why it is not safe:

from typing import Any

x = 'a'
y: Any = 1

lst = [x, y]
lst[0] >> 1  # not detected by mypy, fails at runtime, will be fixed by rule (3)

def f(x: int) -> None:
    x >> 1
def g(x: Any) -> None:
    pass

funs = [f, g]
funs[0]('a')  # not detected by mypy, fails at runtime, will be fixed by rule (4)

@JukkaL I will be grateful for your opinion.

[gvanrossum]

Hm, I have to think about this. I'm not sure I agree with everything in the first diagram either. I thought joins with Any always gave Any? (IOW why is rule (2) not the same as rule (4)?)

Off-topic there's also something with y: Any = 1 where I'd like mypy to behave differently: IMO it should infer that y is temporarily an int but allow assigning anything to it later.

[ilevkivskyi]

@gvanrossum

I thought joins with Any always gave Any?

The reasoning why I don't like this is similar to why we recently prohibited simplifying Union[int, Any] to Any, this is not safe (see example).

(IOW why is rule (2) not the same as rule (4)?)

Rules (2) and (5) are different form others because I want to preserve the fact that object is an "absolute top" and NoReturn is an "absolute bottom". This is natural, consider this simplified reasoning: Any is something that has all methods and all values, but object is something that has all values but no methods, therefore object is wider that Any. Similarly we find that Any is wider than NoReturn.

[gvanrossum]

OK, that explains (1), (2), (5) and (6) to me. That leaves (3) and (4). I think you're saying (3) join(Any, C) == C because C has fewer methods than Any, while (4) meet(Any, C) == C because C has fewer values.

It seems the right way to think about the lattice is that up (join) is the direction of fewer methods and more values (with fewer methods being tested first), while down (meet) is the direction of fewer values and more methods (with fewer values being tested first).

PS. Please have pity on my feeble understanding. I have never had any theory classes about this at all, since except for Simula, OO was invented after I graduated!

[JukkaL]

The join with Any is Any to avoid false positives. For example, consider this code:

class A: pass
class B(A): pass

def f(x: B, y: Any) -> None:
    a = [x, y]
    g1(a)  # should this be fine?
    g2(a)  # what about this?

def g1(a: List[A]) -> None: pass
def g2(a: List[B]) -> None: pass

I think that both calls should be accepted, since each could be okay, given a suitable precise type for y. The philosophy is that replacing a type with an Any type should not generate additional errors if we can avoid that. That's why the inferred type of a is List[Any], not List[B].

[gvanrossum]

So you disagree with (1) and (3) from the OP?

(1) join(Any, object) == object
...
(3) join(Any, C) == C
...

[ilevkivskyi]

@JukkaL

The philosophy is that replacing a type with an Any type should not generate additional errors if we can avoid that.

g2(a) in your example passes with both versions of join, so let us focus on g1(a). Indeed, for y: A it will pass, but will start failing if replaced with y: Any in the case of proposed join. However, there is something that I don't like here, namely:

• I intuitively feel that amount of false positives with proposed join will be smaller than amount of false negatives with current join (this is purely subjective of course, but see next point).
• I don't like "proliferation" of Any, let me explain my intuition: If I see a list of B and "something that always work", then I would expect that a user wanted to create a list of B, not a list of things that will work everywhere.

Of course, a user could always overrule the inference with an explicit annotation, but it seems to me it is better to silence an error with a: List[Any] (or even better with a: List[A] for the case of g1) rather than have a (possibly subtle and nasty) uncaught error. What do you think?

[ilevkivskyi]

@JukkaL
Also, note that in your example invariance is important, everything will still work with proposed join for

def g1(a: Sequence[A]) -> None:
    ...

You could argue that user-defined classes are invariant by default, we already have a section in "Common issues" about this, so that users will be prepared that sometimes explicit annotations are needed.

[JukkaL]

I may well disagree with the rules for meet as well, but this needs some thought as the issue is subtle so I'm focusing on join first. By the way, I'm not convinced that this is analogous to the union simplification fix and this needs to argued for based on its merits.

One of the reasons why Any types are 'contagious' is that that it can highlight code that is unsafe. If something has type Any, using the value is potentially unsafe. If using something is potentially unsafe, inferring Any is generally the right thing to do, unless the user overrides this with an explicit annotation. The proposed rules for join would make mypy less safe in that sense. Example:

class A:
    def f(self) -> None: pass

class B: pass

def f(a: A, b: Any) -> None:
    x = [a, b]
    x[1].f()   # unsafe if b is an instance of B, for example

With the current semantics, the receiver object on the final line has type Any, so it's clear that the method call is unsafe, which is correct. With the proposed semantics, the type would be A, and the call would look safe, even though it's not. We can argue that inferring List[Any] for x is safer than List[A], since the actual runtime type could well be a supertype of A.

[JukkaL]

Another issue with the rules for joins is the behavior with isinstance:

def f(a: str, b: Any) -> None:
    x = [a, b][0]
    if isinstance(x, str):
        ...
    else:
        x(1 + '')  # should be an error

If we infer str as the type of x, we get a false positive on the final line since mypy would think that the line unreachable because of the isinstance test.

Actually, it looks like inferring Union[str, Any] for x would actually conform to principles, but here the argument is different -- we try to avoid inferring union types since they are very unintuitive for users.

[ilevkivskyi]

One of the reasons why Any types are 'contagious' is that that it can highlight code that is unsafe

But the only way for a user to see this is to use reveal_type, or am I missing something? To me it looks quite opposite, with current semantics Any rather "hides" errors (leaves them unreported). For example, extending your example:

def f(a: A, b: Any) -> None:
    x = [a, b]
    x[1].f()
    x[1].never_had_this()
    if function_that_typically_returns_zero():
        x[0].this_will_fail_late()

Another issue with the rules for joins is the behavior with isinstance:

This example is interesting. Inferring Union[X, Any] for particular join(X, Any) is also interesting. Maybe we can just do this internally but simplify this in error messages?

[ddfisher]

I don't think this is an issue that should be resolved in isolation. We have a more thorough review of the type system on our roadmap for the next couple months -- we should make sure to consider the role of Any as part of that, but doing it beforehand would be duplicating work and could potentially lead us in the wrong direction.

[ilevkivskyi]

We have a more thorough review of the type system on our roadmap for the next couple months

Ah, thanks, I didn't know this. Then I propose to postpone this discussion, but leave the issue open just to be sure we will not forget about this.

[gvanrossum]

I wonder if the review should be done in public rather than as Dropbox meetings.

[ilevkivskyi]

I wonder if the review should be done in public rather than as Dropbox meetings.

I can't say for others, but I would very much like it if I had the chance to join :-)