From a user's perspective, I think pyright's behaviour on the first one (keep around both types, use the broader type for future assignments) is the friendliest. In general, I think it's surprising when x: T = ... differs from x: T; x = ... I think the Any examples should be consistent in this respect, and beyond that it matters less. I don't think narrowing is bad (assuming all future assignments are allowed), since you can always cast your value to Any (arguably the clearest way of making a type disappear for a value).

That latter case doesn't surprise me personally; if the type checker can prove that the variable is an int (which appears to be true for the checkers listed, ignoring the difference between decls and decls that also preassign a value), why wouldn't it be allowed at that point?

On 2 Sep 2020, at 21:54, eric@traut.com wrote:

Pyright uses the following principles consistently:

1. Variable type annotations can be specified anywhere within the scope, and the location of the type annotation does not affect other aspects of type checking.

x = 42 x: int # This is fine

y = 42 # This should produce an error y: str

2. A variable can be annotated more than once, but the annotations need to be consistent.

x: int x: int # This is fine

y: int y: str # This should produce an error

3. Type narrowing is always applied within the current execution scope using code flow analysis. (The location of the variable’s type annotation does not change this.)

4. The Any type is never narrowed. “Any” indicates that the type checker should not apply any type consistency rules to that symbol, so narrowing doesn’t make sense in this case.

These principles are consistent with static type checkers in other languages that I’m familiar with, and I think they are consistent with most users’ expectations.

-Eric

Eric Traut Microsoft Corp.

For what it’s worth as a heavy static typing/type hint user I'd expect the exact opposite of the points 1-3 to happen, namely: * an error in case of multiple annotations, regardless of their consistency * no type narrowing in case of explicit type annotation like in the OP Jakub

I found Jukka’s referenced comment to be valuable, so here’s a direct link: https://github.com/python/mypy/issues/2008#issuecomment-296213676 Eg, I believe pyright’s narrowing to Animal corresponds in part to Jukka’s Proposal 2 (or Proposal 4), which he mentions is TypeScript’s behaviour: when narrowing a Union, narrow to a member of the Union. My view on the invariance issue is the most natural flow is to start with: ``` def g(x: Foo[Union[int, str]]): ... def f() -> None: y = 1 a = Foo(y) g(a) ``` Then get an error (with a very clear message / suggestion) and add: ``` def f() -> None: y = 1 a: Foo[Union[int, str]] = Foo(y) g(a) ``` Which is fine in the presence of type narrowing, because obviously we shouldn’t narrow to an incompatible type. (It’s also my opinion that this is the type annotation that best helps describe what’s happening) I don’t know that I’d be so quick to write off always narrowing (modulo Any), which I believe corresponds to Jukka’s Proposal 3. I’d be curious to know more about the significant number of false positives you’d expect; that seems contra my intuition and the results on the sample corpus Jukka described. It also feels wrong to mandate that all future type checkers can’t narrow in part because a majority of our current ones do not. It feels like if a type checker can prove something about a value, it should be fair game (and that as long as users can see that proof is possible, we’ll get bug reports). Generally speaking, it’s surprising to me to make a usability argument for a distinction that most end users wouldn’t notice or weren’t making with intention. But maybe this is a case where if the behaviour is PEP-ed users will no longer find it surprising. On Tue, 8 Sep 2020 at 09:28, dimvar--- via Typing-sig <typing-sig@python.org> wrote:

I also prefer form (1) to respect the declared type and not use the rhs type. Keeping the declared type can avoid a spurious warning in cases where type invariance matters, e.g., with generics.

T = TypeVar('T')

class Foo(Generic[T]): def __init__(self, x: T) -> None: self.attr = x

def g(x: Foo[Union[int, str]]): return x

def f(x: int): y: Union[int, str] = 1 a = Foo(y) g(a) # no warning

y = 2 b = Foo(y) reveal_type(b) g(b) # warning _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: hauntsaninja@gmail.com

Some more follow up :-) First, I attached a file that contains six functions we care about and the behaviours of the four checkers + some of Jukka's proposals (previously linked). This assumes that things are subject to flow control and that checkers allow reassignments based on the declared type. I was going a little cross eyed, hopefully it helps clarify the state of things. (Apologies if I got something wrong!) Next, the question was brought up as to why TypeScript behaves the way it does. I’m not particularly familiar with TypeScript, so I can’t claim to know for sure, but I did some digging: tldr; I'm not convinced there's a good reason. It seems like they just went from always using the annotation to always using the annotation except for unions in order to have a better null story. It looks like they implemented flow based narrowing in 2016, notably narrowing for unions: https://github.com/microsoft/TypeScript/pull/8010 Shortly after, they receive a complaint and discuss other narrowing. The variance narrowing issue gets brought up (along with optional properties, which I think don't matter to us): https://github.com/microsoft/TypeScript/issues/8513#issuecomment-217733352 It’s then mentioned as a thing they’re still talking about. But null is a reason for wanting to have something in place for unions: https://github.com/microsoft/TypeScript/issues/8513#issuecomment-217871478 It seems to still get brought up from time to time: https://github.com/microsoft/TypeScript/issues/36579#issuecomment-617311386 https://github.com/microsoft/TypeScript/issues/16976 It's also worth asking why mypy currently doesn't abide by PEP 526. It's possible this is just a quirk of history, stemming from the evolution of type comments. mypy's behaviour appears to be the same as Proposal 4, except for not narrowing unions. I think that’s why Proposal 4 exists: it’s the most conservative change for mypy that would help with the original issue report in issue #2008. Finally, some discussion of arguments against narrowing. Naturally these apply most to Proposal 3, which always narrows, but they do also apply to various status quos. These arguments are presented in Jukka's cons of Proposal 3 (I'd be curious if other arguments surface). As discussed previously, I’m not fazed by the invariance argument (assuming you narrow to a compatible type). I think I’ve also made my peace with the Sequence / disallowing local mutability argument, since it seems a little too treacherous to be relied on / you can always be explicit and cast / maybe use Final. I’d also want to see usage in real world code here. I do think the interactions with Any are something that need some thought. However, if there isn’t a particularly easy way of doing things cleverly, I’m not that worried about inconsistency. People use Any to stop type checkers from trying to be too clever, so preserving the current behaviour of listening to the user in the presence of Any seems fine. I think users who would complain about not narrowing in the presence of Any would also complain about not narrowing at other times. On Wed, 9 Sep 2020 at 11:17, Dimitris Vardoulakis <dimvar@google.com> wrote:

On Tue, Sep 8, 2020 at 7:00 PM Shantanu Jain <hauntsaninja@gmail.com> wrote:

...

I found Jukka’s referenced comment to be valuable, so here’s a direct link: https://github.com/python/mypy/issues/2008#issuecomment-296213676 Eg, I believe pyright’s narrowing to Animal corresponds in part to Jukka’s Proposal 2 (or Proposal 4), which he mentions is TypeScript’s behaviour: when narrowing a Union, narrow to a member of the Union.

My view on the invariance issue is the most natural flow is to start with: ``` def g(x: Foo[Union[int, str]]): ...

def f() -> None: y = 1 a = Foo(y) g(a) ``` Then get an error (with a very clear message / suggestion) and add: ``` def f() -> None: y = 1 a: Foo[Union[int, str]] = Foo(y) g(a) ``` Which is fine in the presence of type narrowing, because obviously we shouldn’t narrow to an incompatible type. (It’s also my opinion that this is the type annotation that best helps describe what’s happening)

I don’t know that I’d be so quick to write off always narrowing (modulo Any), which I believe corresponds to Jukka’s Proposal 3. I’d be curious to know more about the significant number of false positives you’d expect; that seems contra my intuition and the results on the sample corpus Jukka described. It also feels wrong to mandate that all future type checkers can’t narrow in part because a majority of our current ones do not. It feels like if a type checker can prove something about a value, it should be fair game (and that as long as users can see that proof is possible, we’ll get bug reports).

Generally speaking, it’s surprising to me to make a usability argument for a distinction that most end users wouldn’t notice or weren’t making with intention. But maybe this is a case where if the behaviour is PEP-ed users will no longer find it surprising.

These are all good points. I remember that in Closure Compiler, we used to have the semantics where we keep the rhs type. We ran into issues occasionally where the user needed to use the value with the declared type, so they had to cast to that, which was annoying. We ended up changing the semantics to use the declared type. Unfortunately I can't remember the examples anymore though; just the generics one I already mentioned.

...

On Tue, 8 Sep 2020 at 09:28, dimvar--- via Typing-sig < typing-sig@python.org> wrote:

...

I also prefer form (1) to respect the declared type and not use the rhs type. Keeping the declared type can avoid a spurious warning in cases where type invariance matters, e.g., with generics.

T = TypeVar('T')

class Foo(Generic[T]): def __init__(self, x: T) -> None: self.attr = x

def g(x: Foo[Union[int, str]]): return x

def f(x: int): y: Union[int, str] = 1 a = Foo(y) g(a) # no warning

y = 2 b = Foo(y) reveal_type(b) g(b) # warning _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://mail.python.org/mailman3/lists/typing-sig.python.org/ Member address: hauntsaninja@gmail.com

-- Dimitris

Weighing in on Eric's last post with regards to Pyre's current behavior and plans:

In short, should these two cases be treated in a consistent manner?

The current pyre behavior does not refine on same-line type declaration but does when assignment happens later. However, afaik this is a bug and we support consistency as per Eric's post here. Our plan is to change this so Pyre also refines to a narrower type on same-line assignments, while keeping the broader type around to prevent assignments incompatible with the explicit annotation further on. For more context, all of Pyre's planned follow-ups/fixes from this discussion include: 1. Stop refining variables explicitly typed as `Any` to allow for an escape hatch. 2. Be consistent about refining `x: Union[int, str] = 42` and `x: Union[int, str] \n x = 42` 3. Stop allowing explicit re-annotations of variables with the same name. Pyre is also treating typed parameters as explicitly annotated locals, so allowing re-annotation was originally supported for naming flexibility. However, this seems like a reasonable sacrifice to support Eric's Point #2. Overall Eric's set of points aligns with Pyre's intended behavior. The one example that may be worth clarifying: ``` a: Union[int, str] = 1 # Type is a is narrowed to int b = [a] # Currently Pyre is using the broader type of 'a', and types 'b' as List[Union[int, str]] here. ``` The narrowed type of `int` is still useful if passing or returning `a` where `int` is required. On 9/18/20, 1:06 PM, "Eric Traut" <eric@traut.com> wrote: A few thoughts here (and apologies for the long post). First, I think we should try to avoid conflating _when_ to apply type narrowing with _how_ to apply type narrowing (i.e. the resulting type when narrowing is applied). We may want to standardize aspects of both the _when_ and the _how_, but it will help the discussion if we keep these two issues separate as much as possible. I will first focus on _when_ type narrowing should be applied. It appears that we have one primary point of contention — whether narrowing should be applied for all assignments. Some have argued that narrowing should be skipped if the assignment statement includes a variable type annotation. In short, should these two cases be treated in a consistent manner? ```python # (1) a: T = x # (2) a: T a = x ``` We (the maintainers of pyright) have a strong conviction that type narrowing should not be tied in any way with the location of type declarations. The two code samples above should be treated in a consistent manner, and narrowing should be applied in both cases. Here’s the thought process behind this position. I’m hopeful that most of these points (at least through point 5) will be uncontentious and will form a solid basis for our point of view. **Point 1**: A type annotation provided for a variable declares that the variable should be assigned only values whose types are compatible with the declared type. Any attempt to assign a value whose type is not compatible with a variable’s declared type should be flagged as an error by a type checker. **Point 2**: A symbol can have only one declared type. A symbol can’t be declared as a function and in the same scope redeclared as a variable of type “str”. An instance variable cannot be declared as an `int` in one method but a `str` in another. A local variable cannot be declared as an `int` within an “if” clause and declared as a `str` within the “else” clause. Any attempt to redeclare a symbol in an incompatible manner should be flagged as an error. **Point 3**: PEP 526 does not (nor should it) dictate that a variable’s type declaration must be provided upon “first use” of that variable. In fact, there’s no clear definition of “first use” in Python. An instance variable (e.g. “self.foo”) might be assigned a value in two different methods, and the order in which these methods are called at runtime cannot be known statically. A variable’s type declaration can therefore appear anywhere, in any order, and it must apply to all uses of that variable. ```python # These are semantically equivalent. class C1: def f1(self): self.var: Optional[int] = None def f2(self): self.var = 4 class C1: def f1(self): self.var = None def f2(self): self.var: Optional[int] = 4 ``` **Point 4**: Absent any additional information about a variable whose type has been declared, a type checker should assume that it contains a value with the declared type. ```python def foo(a: Optional[int]): reveal_type(a) # “Optional[int]” at this point class C1: def __init__(self): self.var: Optional[str] = None def f1(self): reveal_type(self.var) # “Optional[str]” at this point ``` **Point 5**: Type narrowing is a process by which a type checker can use additional contextual knowledge within a control flow graph to understand more detailed information about a variable’s contents _at a particular point in the code flow_. Knowledge of narrower types is beneficial because it allows the type checker to perform more accurate check, minimize false positives, and provide more accurate completion suggestions for developers. Additional knowledge about a variable’s type that can be discerned from the control flow graph should not be discarded or ignored! **Point 6**: Type narrowing should be independent of (and not influenced by) the location of a variable’s type declaration. As we noted above, the location of a variable’s declaration is incidental, and the type declaration is independent of code flow considerations. Any other interpretation results in inconsistent behaviors, an inconsistent mental model for developers — especially those who are new to type annotations, and hard-to-explain edge cases. Alternate interpretations also result in false-positive errors because they ignore valuable information derived from narrowing. Some have argued that applying type narrowing in an inconsistent manner can be a useful technique for handling cases where the assigned variable is subsequently used to infer an invariant type argument for a generic type. ```python a: Union[int, str] = 1 # Type is a is narrowed to int b = [a] # Inferred type of b is List[int] c: List[Union[int, str]] = b # Error ``` In this example, `b` does not have a declared type, so its type needs to be inferred. There are cases (like this) where a type cannot be inferred in an unambiguous manner, and the normal heuristics for type inference can produce an answer that is inconsistent with the programmer’s intent. The appropriate fix for removing this ambiguity is to introduce a type declaration and eliminate the need for type inference. In this case, the ambiguity is with the inference of `b`, so a type declaration should be added as follows: ```python a: Union[int, str] = 1 b: List[Union[int, str]] = [a] c = b ``` Solving the inference ambiguity for `b` by introducing an inconsistent type narrowing rule for `a` is not the right solution! Finally, it’s worth noting that there are many different conditions where type narrowing can be applied, involving a variety of techniques. For example, pyright currently applies type narrowing in the following cases: 1. Assignments 2. Positive (“if”) and negative (“else”) conditional code flow constructs where the conditional expression contains: * A combination of “and”, “or” or “not” boolean operators * “is None” or “is not None” tests * “type(X) is Y” or “type(X) is not Y” tests * “X.Y == <literal>” or “X.Y != <literal>” tests where Y is used to discriminate among subtypes * “X is Y” or “X is not Y” enum tests * “X in Y” tests * isinstance() tests * issubclass() tests * callable() tests * Truthy or Falsy tests Standardizing this list is going to be challenging because different type checkers implement different techniques, and this list will undoubtedly continue to grow over time as new innovations are introduced. It may still be worth trying to standardize some aspects of assignment-based narrowing, but this will invariably leave behavioral differences between type checkers. We should collectively decide on whether the benefits of standardizing these behaviors outweigh the downsides. Now, I’ll focus on _how_ type narrowing is applied, specifically for assignments. We seem to have reached some level of agreement about the following: 1. Narrowing should eliminate subtypes within a union where possible 2. Narrowing should replace base classes and protocols with derived classes and derived protocols where possible 3. Narrowing should not be applied if the declared type is “Any” Guido identified a bug in pyright where rule #2 was not being applied when the RHS of the assignment was a call to a constructor. This is a regression that I introduced recently. I’m working on a fix as well as a more comprehensive test suite that should prevent similar regressions in the future. As I started to fill out this test suite, I ran across additional cases that are not covered by the list above. The most notable case involves a type declaration that includes a generic type (or a generic protocol) where one or more type arguments is specified as “Any”. For example: ```python def func(p: List[int]): a: List[Any] = p reveal_type(a) # ? ``` If we agree that “Any” is meant as a way to disable further type checking, then it probably follows that the `reveal_type` in the above example should indicate that `a` is type `List[Any]` rather than `List[int]`. Do others agree? If so, how far do we take this? Should it apply to derived classes and protocols? I think the answer is probably yes, but I’m not fully convicted. Should this nest arbitrarily or apply only to the first level of type arguments? I’m not sure. ```python def func(p: List[int]): a: Iterable[Any] = p reveal_type(a) # List[Any]? ``` ```python def func(p: List[List[int]]): a: Iterable[List[Any]] = p reveal_type(a) # List[List[Any]]? List[List[int]]? ``` There are also interesting cases involving unions that include Any. I think these are straightforward if we apply the rules consistently. ```python def func(p: List[int]): a: Union[Any, Iterable[int]] = p reveal_type(a) # Union[Any, List[int]]? ``` ```python def func(p: Union[Any, List[int]]): a: Iterable[int] = p reveal_type(a) # Union[Any, List[int]]? ``` Based on this exploration, I propose that we add the following fourth rule: 4. If a declared type contains an “Any” type argument, the corresponding type argument(s) in the narrowed type must also be “Any” Here’s a partial test suite that I’ve started to compile based on these four rules. It builds on Guido’s examples using an `Animal` base class. Do these test cases look correct? ```python from typing import Any, Dict, Generic, Iterable, List, Literal, Protocol, TypeVar, Union _T1 = TypeVar("_T1") _T2 = TypeVar("_T2") _T3 = TypeVar("_T3") class Animal(Generic[_T1, _T2]): pass class Bear(Animal[_T3, int]): pass class Donkey(Animal[int, int], Generic[_T3]): pass class Flyer(Protocol[_T1]): def get_wingspan(self, p1: _T1) -> float: raise NotImplemented class CaveDweller(Generic[_T1]): pass class Bat(Animal[int, int], CaveDweller[int]): def get_wingspan(self, p1: int) -> float: raise NotImplemented def s1(): b: Bear[str] = Bear() a: Animal[str, int] = b t: Literal["Bear[str]"] = reveal_type(a) def s2(): a: Animal[str, int] = Bear() t: Literal["Bear[str]"] = reveal_type(a) def s3(): a: Animal[str, int] = Bear() t: Literal["Bear[str]"] = reveal_type(a) def s4(): a: Bear[Any] = Bear[int]() t: Literal["Bear[Any]"] = reveal_type(a) def s5(): a: Animal[Any, Any] = Bear[int]() t: Literal["Bear[Any]"] = reveal_type(a) def s6(): a: Union[Bat, Bear[str]] = Bear() t: Literal["Bear[str]"] = reveal_type(a) def s7(p: Union[Bat, Bear[int]]): a: Animal[int, int] = p t: Literal["Bat | Bear[int]"] = reveal_type(a) def s8(): a: Animal[int, int] = Bear[int]() t: Literal["Bear[int]"] = reveal_type(a) def s9(p: Dict[str, str]): a: Dict[str, Any] = p t: Literal["Dict[str, Any]"] = reveal_type(a) def s10(p: List[str]): a: Iterable[Any] = p t1: Literal["List[Any]"] = reveal_type(a) b: Iterable[str] = [] t2: Literal["List[str]"] = reveal_type(b) c: Iterable[str] = list() t3: Literal["list[str]"] = reveal_type(c) def s11(): a: Animal[Any, Any] = Donkey[int]() t: Literal["Donkey[int]"] = reveal_type(a) def s12(p: Bear[_T1]): a: Animal[Any, int] = p t: Literal["Bear[Any]"] = reveal_type(a) def s13(p: Bat): a: Flyer[int] = p t: Literal["Bat"] = reveal_type(a) def s14(p: Bat): a: CaveDweller[int] = p t: Literal["Bat"] = reveal_type(a) ``` --- Eric Traut Microsoft _______________________________________________ Typing-sig mailing list -- typing-sig@python.org To unsubscribe send an email to typing-sig-leave@python.org https://urldefense.proofpoint.com/v2/url?u=https-3A__mail.python.org_mailman3_lists_typing-2Dsig.python.org_&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=j6-YRB8UY9YIqi5vSSyJ-A&m=ubs0-apyddHxYXcNM_VKjqjq1NYu_xeRMKGzCJjOhfA&s=q39sx_ByPr2K3qjOETPCA9IlF0cEbHiQFrU9fAgwllQ&e= Member address: szhu@fb.com