WIP: unify [] and [1] to list[int] rather than object

[gvanrossum]

@JukkaL and/or @ddfisher Can you help me make this work? I'm trying to fix #2255, which has this example:

a = [[], [1]]

and the type inferred is list[object] rather than e.g. list[int].

[rwbarton]

This isn't really sound (List[UninhabitedType] isn't a subtype of List[int] for the same reason that List is not covariant in general), though it may actually be harmless if UninhabitedType can't appear in the type of a variable.

The right way to fix this would be at type inference time, though it's tricky because we need the result of type checking one argument in a function call to affect the type inferred for another argument of that call.

[elazarg]

@rwbarton but the case of list-literal is different, since the literal itself is immutable. Am I wrong?

[elazarg]

In other words, if hypothetically we had a "list literal" type - essentially a tuple - this was going naturally and smoothly.

We already have this type, but we don't give it its own class . Instead, we special-case it in multiple assignment and in other circumstances, thus being forced to carry syntax information to type checking.

[gvanrossum]

@rwbarton: I had hoped that the mechanism whereby [x, y] determines the item type is similar to that of x if <cond> else y. For example, the type of [] if bool() else [1] is list[int], as is the type of [1] if bool() else []. (IIRC I wrote the hack that made this work, and it works by trying it both ways, being careful not to let errors escape when the first try fails.) But apparently [x, y] does not use the same code path. (Perhaps I put the hack in the wrong place.)

We see the same issue occur with e.g. reveal_type([[0], [0.0]]). Again, reveal_type([0] if bool() else [0.0]) give the right answer (list[float]) but for [[0], [0.0]] we get list[object].

@elazarg: IIUC what we need is a way to say that the type of [x, y] is list[t] where t is the intersection type of the types of x and y. And also IIUC such type intersections are computed by join_types(). I believe what you are saying is that we should have a special way to represent the type of [] (and other list literals) so that join_types() understands that the join of the empty list's type and the type of some other (non-empty) list should always be the type of that other list. Essentially it should behave covariantly?? Then x if <cond> else y could just use join_types() instead of the above-mentioned hack.

Care would however have to be taken that whenever such a specially marked "coercible" list is assigned to a variable or passed to a function it is coerced to a regular (invariant) list type, since the following two examples are not the same:

b = [[], [1]]

vs.

a = []
b = [a, [1]]

In the first case the type of the empty list literal can be coerced to list[int]. But in the second case it should not be -- it should continue to complain "Need type annotation for variable" for the assignment to a.

[elazarg]

(I still have much to learn here, but I'll speak my mind anyway)

The join operation computes something related to a union, not an intersection. It's the operations allowed on the resulting types that are in the intersection of those allowed for each type. And IIUC this is what needed to the list, if not for the mutability/variance problem. There is some connection between literals and intersection types, but I fail to see it in this example.

Regarding your concerns, perhaps a better name to "literal type" is "temporary type" - as long as we know that the list cannot be mutated outside the inferred context (which does not hold in your last example), it should be fine[1]. I think this information is partially kept in Expression as .literal, instead of being part of the type information. So join.py does not seem to have access to this information.

Having this information about temporary-value-types (or literal types), maybe the conditional expression problem will just solve itself.

[1] Even things like list(x for x in ([], [1], [3]))

[gvanrossum]

If it's not the join, maybe it's the meet? They are each others opposites.

[elazarg]

No, it is the join. It's just that (IIUC) the function does not have the information to be sure it's sound unless t <: s or s <: t, even though it is sound in the case of e.g. literal.

Your patch hard coded this information in the case of UninhabitedType, and as @rwbarton and you pointed out it might be sound, as long as we reject UninhabitedType from being a type-argument in a type of something that can be mutated. It is the case in "pure" literals, but I am not sure it is the case in general.

(Meet is related to intersection, which means each element of the list is "both" s and t. As in a fallback, promotion or multiple inheritance. I can't see how it applies to this case; I will enjoy being proved shortsighted here though)

[gvanrossum]

My brain hurts. I'll close this PR.

[JukkaL]

In an early predecessor of mypy I actually had separate types for things like [], and they were kind of like existential types exists T: List[T]. For an expression like [1] we could have something like exists T :> int: List[T]. I don't remember all the specifics, but I believe that it was pretty complicated in general. I used it as an alternative to bidirectional type inference (i.e. for example type context in mypy speak), which wouldn't be the case any more.

However, just supporting this for empty collections could be more straightforward, though it seems like the benefit would be pretty marginal and better error messages would perhaps make the problem mostly go away.