Making Final assignment non-narrowing

[ajasmin]

Background

For some background refer to typing-sig discussion and the corresponding discussion on, python/mypy#2008.

pyright allows mutating objects through a variable declared as an immutable superclass and mypy will soon follow suit.

For instance:

L: Final[Sequence[int]] = [1,2,3]  # "Sequence" was narrowed to assigned type "list"
L.append(4)  # this allows for mutation

def f() -> None:
    L.append(5)  # This works too

The rationale for the change is that assignment at declaration should behave the same as a separate assignment statement, such as:

L: Sequence[int]
L = [1,2,3]  # narrows down type to list
L.append(4)  # This works on mypy today

I agree that assigning a variable on the same line as its declaration should behave like assigning it on the following line.

That said, having a way to declare a constant with a restricted immutable type like Mapping or Sequence would still be helpful to improve program correctness. It's also common to use immutable types for function arguments for the same reason.

A workaround is to put constants in a separate module as the type checker will use the declared type in this case.

Proposal

What would you think of a proposal that treats initialization with Final (specifically) as non-narrowing so that the first example still prevents mutability?

My rationale is that:

• Final variables can only be assigned at declaration, so consistency with later assignments is less of a concern. Though, it would differ from the non-final case.
• Final is used to declare "constants" and that is typically where you want to enforce immutability also.
• Semantically this seems somewhat coherent. Final assignment, final type.
• If you don't need to constrain the type, Final without a type argument can still be used to infer the assigned type.
• This isn't likely to break much code out there. In fact, mypy still has to adopt the new behaviour.

[erictraut]

I think this would be an inappropriate use of Final, which means that the symbol cannot be reassigned, not that its type cannot be narrowed or that the object referenced by the symbol is immutable. Type narrowing is an orthogonal concept to Final, and IMO the two should not be conflated.

There are cases where Final can safely allow for additional type narrowing. For example, x: Final = 3 allows the inferred type of x to be Literal[3] rather than int.

[ajasmin]

From what I understand, the main reason for narrowing on assignment is to allow things like:

s: Shape = Shape()
if foo:
    s = Circle()
    print(s.radius)

print(s.area)

But, Final doesn't allow such patterns since reassignment is forbidden.

In my code (at least), the case where I want to declare things as an immutable supertype also seems to coincide with those where I want to restrict assignment with Final:

from collections.abc import Set, Sequence
LOCAL_DEPENDENCIES: Final[Set[str]] = ...
EMPTY_ENV: Final[Mapping[str, str]] = {}

Introducing another qualifier could work but would be even more verbose:

LOCAL_DEPENDENCIES: Final[NoNarrow[Set[str]]] = ...

I wouldn't want to change the behaviour with no explicit type where x: Final = 3 has the type Literal[3].

And even though I would keep such declarations as x: Final, I concede that narrowing x: Final[int] = 3 to Litteral[3] is probably best...

[erictraut]

The main reason to narrow on assignment is that narrower types are almost always preferable to wider types. They are more precise, so type checkers should prefer narrower types wherever possible.

[sobolevn]

Your example looks wrong to me.
x: Final[Sequence] means a very specific thing:

1. x cannot be reassigned
2. x has Sequence[Any] type

I don't see why we should special case this to explicitly contradict annotation and allow list or whatever to be narrowed here.

[ajasmin]

You're very right about Sequence[Any], I usually check things with disallow_any_generics but didn't do so here.

For context: my original post was using Sequence (no type argument). I've rewritten it for clarity. But this does show how this feature could easily make things more confusing.