What does "set of potential runtime values" mean in the context of fully static types.

[doeblerh]

According to the official python typing documentation "A fully static type denotes a set of potential runtime values.", which reads like being a definition or at least explanation. But what is meant by "potential runtime values"?

Consider the following snippet:

class A: pass

class B(A): pass

def list_consumer(list_of_a: list[A]) -> None:
    list_of_a.append(A())

b = B()

l_a: list[A] = [b]
l_b: list[B] = [b]
l_inf = [b]

list_consumer(l_a)
list_consumer(l_b)  # type error (pyright 1.1.406)
list_consumer(l_inf)  # type error (pyright 1.1.406)

(Note: I fully agree with the type checker. list's type argument is invariant, thus list[B] is not assignable to declared type list[A]. No problem with that.)

My question is: The tree variables l_a, l_b, and l_inf are all bound (at runtime) to values [b], which are equal but mutually non-identical. Yet, only l_a is assignable to type list[A]. So in how far can we talk about the fully static type list[A] as "denoting a set of potential runtime values"? There are multiple equal runtime values, who differ only in the declared or inferred static type, some of which are members of this set, while others are not?

As far as I understand, the static type information list[A] vs. list[B] is a quality of the variable itself and not the runtime value it is bound to.

Do we consider the static type information associated to a variable to be part of the runtime value it holds even though the object that constitutes this value has no connection at all to the static type?

[JelleZijlstra]

Yes, this is a place where the "set of runtime values" definition becomes problematic. The way I think of it is that a generic conceptually carries around not only its value, but a "tag" representing its type argument, which is erased at runtime ("type erasure" is a well-known concept in some other languages). We might represent it with <T> before the value. So your different [b] lists are to the type checker <A>[b] (of type list[A]) and <B>[b] (of type list[B]).

It follows that it is impossible to tell at runtime what the static type of a list object is, so any type narrowing (e.g., TypeIs) that purports to narrow the type of a list is inherently unsound.

[doeblerh]

What you write makes sense. But therefore I am still not convinced that static type ::= set of possible runtime values is a sound definition that connects the concept of static types to runtime values. Even if the language did allow values to carry a tag for type arguments (with the tags themselves being objects representing static types), the definition of "fully static type" would become self-referential / cyclic: We would define a fully static type as a set of values, where a "value" would (in case of generic types) comprise an attribute referring to a fully static type.

Might it be that the "set of runtime values" definition simply does not apply to fully static types in python? Because the question if a value is member of a given fully static type is not just undecidable but rather "not well-defined" at runtime. Making the definition as a set of possible values contradict itself.

To make a more abstract argument independent of the code example an the special case of list literals:
The "Type system concepts" page states that

1. fully static types denotes sets of possible runtime values
2. if (the set of values represented by) a type TB is a subset of (the set of values represented by) type TA, => TB is subtype of TA, => TB is assignable to TA

If we look at the possible values (who do not carry the static type information) of list[B], each of these values is an element of of list[A] too, i.e., list[B] is a subtype of list[A] according to (2.).

But we know for sure that list must be an invariant generic, i.e., list[B] must not be assignable to list[A]. Hence (1.) and (2.) cannot be used to define a consistent static type system that is capable of describing python's list appropriately.

[carljm]

I agree that the wording in the "core concepts" page should better capture this nuance. But I don't think that the current description is so far from workable as you imply; I think some added wording about what is meant by "runtime value" in the context of generics is sufficient. That is, by "runtime value" for instances of generic classes, we mean "a runtime value with implied tags for type parameters, although these are erased at runtime," as Jelle says.

This does mean that it is not necessarily possible to make a runtime determination of which static type(s) a given runtime object inhabits; that is, the type system tracks information in static types which is erased from the inhabitants of those types at runtime. But this does not imply a problematic circularity or that static types are "undecidable" or "not well-defined". (It is in fact the case that the Python type system is Turing complete, and thus Python types are in some sense statically undecidable, but that's sort of a separate issue and not really a problem in practice.)