Inference on Literal Types

Typing
1

@erictraut and I have a disagreement on how objects declared as Literal should be propagated in collections. See pyright does not infer list of Literals, but mypy does · Issue #9491 · microsoft/pyright · GitHub

I thought I would ask the community here their opinion, as my colleagues and I disagree with how pyright is interpreting the code in question, with us agreeing with the output of mypy.

Here’s a complex example from that discussion:

from typing import Literal, TypeAlias

Days: TypeAlias = Literal["Mon", "Tue", "Wed", "Thu", "Fri", "Sat", "Sun"]

def myfunc(y: Days):
    print(y)

def iterate_this(daylist: list[Days], adict: dict[Days, Days]):
    for x in set([adict[x] for x in daylist]):
        myfunc(x)

pyright will report that the call to myfunc is incorrect because it has inferred the type of x to be str rather than Days. mypy will infer x to be Days. To work around this so that pyright accepts the code, one has to change iterate_this() to iterate_this2():

def iterate_this2(daylist: list[Days], adict: dict[Days, Days]):
    theset: set[Days] = set([adict[x] for x in daylist])
    for x in theset:
        myfunc(x)

We find the former code more natural to write.

More details in the discussion in the link. For me, the question is whether a type that is Literal should be interpreted as a class with restricted values and thus it propagates in comprehensions and loops, versus having it get promoted to a wider type.

I’d like to hear the opinions of the wider community of whether they prefer the current mypy behavior in this case, or if the choices made by pyright could be considered correct as well.

2 Likes
2

Is it the goal of this question to update the typing specification in case of a community consensus?

If it is, please follow the process specified here, including providing an explanation of what the current behaviours are, what your recommendation is and why the latter is better.

If it isn’t, then this is really just about the pros and cons of implementation details and design choices. Such a discussion is unlikely to have a satisfying conclusion for any parties involved.

3

It’s really to get a community opinion on the design choices of mypy versus pyright . If this isn’t the proper forum, I’m fine to move the discussion to a different place.

2 Likes
4

pyright appears to be entirely in the wrong from a type theory perspective here, as well as being less generally useful.

The type that went in was Days, not str. While Days is a subtype of str[1], in every position a type variable exists under the hood here, it is invariant. There isn’t room for interpretation.

  1. The most useful understanding from theory is that Literals are refinement types, but in set-theoretic typing, those must abide by subtyping of the type being refined. ↩︎

5 Likes
5

Is it common to use Literal like this to type variables like x that are not actually bound to literals?

I thought that the purpose of Literal was really just for use with @overload so that the type system has a way to express/model the fact that a function’s return type might depend on the value of certain parameters.

6

I think it is common. It’s a way to say that not all strings are valid for this variable, only these specific strings.
I use it a lot. There’s a lot of Literal in typeshed that isn’t used for overloads.

3 Likes
7

I think it’s more useful to pay attention to the declared type.
Inference is basically guessing what the code author cares about. If there’s an annotation, then you don’t need to guess, because the author is telling you.

a = [1]
# The type checker has to guess whether the author cares about object, or int, or Literal[1]...

one: Literal[1] = 1
a = [one]
# Now the type checker doesn't need to guess. The information is there.
2 Likes
8

so you’re saying that what mypy does, inferring a is list[Literal[1]] is preferred over the pyright behavior, inferring a is list[int] ? (the mypy behavior is what I think should be done)

1 Like
9

You can do

for x in set[Days](...):
    myfunc(x)

to avoid the variable declaration.
Also, fyi sets have comprehensions too:

{adict[x] for x in daylist}
10

FWIW my expectation is that, as one type is explicitly marked as Literal[1], a should be inferred as a list[Literal[1]].

I am however interested to understand the rationale behind pyright behavior, as I’m assuming is intentional.

11

It’s important to first clarify the distinction between the declared type of a symbol and the locally-narrowed type of a symbol. The declared type of a symbol defines the upper bound of the types that are allowed to be assigned to it. In addition to a symbol’s declared type, a type checker tracks its locally-narrowed type. This is the type that is revealed when you use reveal_type. It’s also the type that is used when the symbol appears within an expression, and the type checker is evaluating the type of that expression.

x: Literal[1, 2, 3]  # Declared type is `Literal[1, 2, 3]`
x = 1
reveal_type(x)  # Locally-narrowed type is `Literal[1]`
x = 2
reveal_type(x)  # Locally-narrowed type is `Literal[2]`

Pyright is more aggressive than mypy about retaining literal types when narrowing. There are many advantages to this, including the ability to perform literal math, which allows for more aggressive narrowing and various forms of meta-programming.

x: int  # Declared type is `int`
x = 1
reveal_type(x)  # Mypy: int, pyright: Literal[1]
x = 2 * 4 + 2 ** 2
reveal_type(x)  # Mypy: int, pyright: Literal[12]

I understand why one might intuit that the original declared type of a symbol should influence the inferred type of an expression in which the symbol appears, but this isn’t how type checkers work. The declared type is largely irrelevant when evaluating expressions. We need to look at the locally-narrowed types to explain the differences between mypy and pyright.

Consider the following example.

from typing import Final, Literal, cast

# Assign `1` to a bunch of variables
a: int
a = 1
b = 1
c: Final = 1
d: Literal[1, 2, 3]
d = 1

reveal_type(1)  # Pyright: Literal[1], Mypy: Literal[1]?
reveal_type([1])  # list[int]

reveal_type(cast(Literal[1], 1))  # Pyright: Literal[1], Mypy: Literal[1]
reveal_type([cast(Literal[1], 1)])  # Pyright: list[int], Mypy: list[Literal[1]]

reveal_type(a)  # Pyright: Literal[1], Mypy: int
reveal_type([a])  # list[int]

reveal_type(b)  # Pyright: Literal[1], Mypy: int
reveal_type([b])  # list[int]

reveal_type(c)  # Pyright: Literal[1], Mypy: Literal[1]?
reveal_type([c])  # list[int]

reveal_type(d)  # Pyright: Literal[1], Mypy: Literal[1]
reveal_type([d])  # Pyright: list[int], Mypy: list[Literal[1]]

reveal_type(d * 1)  # Pyright: Literal[1], Mypy: int
reveal_type([d * 1])  # list[int]

Note that mypy’s revealed type for the expression 1 is Literal[1]?. Notably, there is a question mark displayed. Mypy internally treats some Literal types differently than others. There is no such distinction in the typing spec. I personally find this inconsistent handling of literals undesirable and confusing, but I understand why mypy authors chose this approach. Pyright takes a different approach.

The behavioral differences you’re seeing here between pyright and mypy can be summarized as:

  1. Pyright is more aggressive at narrowing to literal types (and generally retaining literal types) than mypy.
  2. Mypy distinguishes internally between two different types of literals whereas pyright treats all literals the same.
  3. In list, set and dictionary expressions (including comprehensions), pyright does not retain literals by default. Mypy retains literals conditionally based on internal flags that differentiate between different variants of literals.

Contrary to what @mikeshardmind asserted above, both type checkers are correct from a type theory perspective. Both approaches have different tradeoffs. In my experience, pyright’s rules lead to better and more consistent behavior and fewer false positives overall, but there are always tradeoffs.

Inference behaviors for type checkers are intentionally not dictated by the typing spec. Regardless of the inference behavior chosen by a type checker, there will always be situations where there’s a need to override the default inference behavior. With the right set of rules and behaviors, this can be kept to a minimum.

Both mypy and pyright have established their own sets of narrowing rules and inference behaviors, and each set works together cohesively. Changing one rule or behavior in that set typically affects the others. It’s therefore unlikely that either mypy or pyright would change these behaviors at this point. Such a change would create significant churn for users.

@Dr-Irv, if you prefer mypy’s behaviors to pyright’s, then you should use mypy for your projects. The benefit of having multiple type checkers in the Python ecosystem is that you can choose the one that best suits your needs.

4 Likes
12

This is not a reasonable suggestion.

I prefer Visual Studio Code for python development. One advantage is its tight integration with pyright. Moving to mypy is a loss of productivity for me and my staff.

You can see from this discussion that others agree with my point of view. You widen Literal types in some cases to other Literal values (which, by the way, my staff finds really odd), but you don’t do it when having collections of values that you know are Literal types.

1 Like
13

If we had actual rules here that followed from theory, it wouldn’t be inconsistent. Pyright is also doing something inconsistent here.

Code sample in pyright playground


from typing import Literal, reveal_type


s: list[Literal[1, 2, 3]] = [1, 2, 3]

wrap_with_list = list(s)  # Type of "wrap_with_list" is "list[Literal[1, 2, 3]]"
generator_expression = (i for i in s)  # Type of "generator_expression" is "Generator[int, None, None]"

def generator():  # Type of "generator" is "() -> Generator[Literal[1, 2, 3], Unknown, None]"
    yield from s

generator_expression_list = list(generator_expression)  # Type of "generator_expression_list" is "list[int]"

# this one in particular is very bad, as the inferred type of generator is thrown away by pyright
# because of Unknown Recv types on the generator not used by list, and not inferred properly with program flow
generator_list = list(generator)  #  Type of "generator_list" is "list[Unknown]"


# Why is unpacking not using a TypeVarTuple here?
unpack = [*s]  # Type of "unpack" is "list[int]"
sliced = s[:]  # # Type of "sliced" is "list[Literal[1, 2, 3]]"

# reveal_types used
reveal_type(wrap_with_list)
reveal_type(generator_expression)
reveal_type(generator)
reveal_type(generator_expression_list)
reveal_type(generator_list)
reveal_type(unpack)
reveal_type(sliced)

I stand by what I said. by my view of soundness is much stricter than yours. Both are unsound here as they discard relevant type information that changes the semantic meaning of a type and what is allowed, namely, that the programmer has expressed is a constraint on the type.

Throwing away value constraints may not always result in a crash, but resulting in the wrong inferred type and allowing more than what a developer wrote is unsafe in other ways. Python’s type system has this problem in a lot of places of being information lossy, and I’ve brought some of those up before.

They reach incorrect handling in multiple ways, and this case shouldn’t even involve inference, we should define Comprehensions and Generator expressions to retain type information. More broadly, (expr for val in iterable) should have a type of Generator[?] as if it was inlining

def inlined_gen(Iterable[T]) -> ?:
    for val in iterable
        yield expr

as this is the intended purpose of such comprehensions and generator expressions. One can note that this part might look like a place where variance is now covariant here in this exact scope, but that’s another point of unsoundness we’ve gone over before with structural types losing variance information.

4 Likes
14

(post for the benefit of mailing list users)

I’ve made minor edits to the above that fix what was listed as the inferred type for slicing (an obvious copy/paste fail, as it was referring to the unpacking example still) and made a small change to how prose about expanding generator expressions referred to an example without changing the example or it’s intent.

I normally try to avoid editing significant edits, especially after the mailing list delay or someone after has responded on discourse, but missed these.

15

Isn’t all of what follows this just wrong? You can’t narrow a Literal[1] to an int, you can’t narrow Literal[“a”] to a str, these are already more narrow types, and while some things can accept a wider type, inference shouldn’t widen types.

3 Likes
16

mypy is paying attention to the declared type, and its inference is better because of it.

class B:
    pass


class C(B):
    pass


b: B = C()
a = [b]
reveal_type(a)  # mypy list[B]  pyright list[C]

x = C()
y = [x]
reveal_type(y)  # mypy list[C]  pyright list[C]
3 Likes
17

This shows better inference from pyright. The actual type at runtime is list[C]. If you want the list to be a mutable list constrained to elements of type B then that is where the annotation should have been:

b = C()
a: list[B] = [b]

What you are asking for here is not for the type checkers to infer the type but to guess what type constraint you intended for the elements of the mutable container.

1 Like
18

I disagree with this. The annotated type is correct, and an expression of developer intent. Ignoring a correct expression of developer intent because the runtime is more specific is a tool making an opinionated choice that goes against the stated intent. When a stated annotation is wrong, raise an error and point out what can be changed. don’t silently insert a different intent than was expressed.

4 Likes
19

for what it’s worth, I’m aware of why pyright does this and the other problems it can prevent, but I think pyright does this wrong in an attempt to have better speed.

There’s a better way: using the stated developer intent for type inference, while tracking known runtime specifics to check for if and where it leads to a total consistency problem later on.

Also, pyright is also inconsistent about this and only applies it like this for local inference you can change constructing C to being inside a function annotate as returning B, and pyright no longer does this “for and in spite of the developer”

Instead of checking the full graph of program flow, pyright in some cases ignores developer intent, making typing more arduous for users.

20

I don’t think it is inserting a different intent. The intent is that you can only assign type B to b and pyright honours that:

class B: pass
class C(B): pass
b: B = C() # fine
b = B() # fine
b = 1 # error

If you want to state an intent about what is allowed to be included in the list a = [b] then that should be stated as a constraint on the list a, not a constraint on the name of the object that is first put in the list.

It does it if you don’t annotate the function as returning anything. If you do annotate a return type then that is respected which is important if you imagine wanting to be able to change exactly what the function returns in future.

Doing this for local inference seems best to me. The mypy version doesn’t allow something like this for example:

def f(a: int|str):
    if isinstance(a, int):
        b = [a]
        b.append(3)
    else:
        b = [a]
        b.append("123")
    return len(b)

The only thing I would prefer is if there was a way to distinguish between constraints on function parameters vs constraints on the local variable that receives the argument e.g.:

def f(a: list[int]):
    a = set(a) # pyright rejects this