Skip to content

Commit 18eaa65

Browse files
[ty] Introduce a representation for the top/bottom materialization of an invariant generic (#20076)
Part of #994. This adds a new field to the Specialization struct to record when we're dealing with the top or bottom materialization of an invariant generic. It also implements subtyping and assignability for these objects. Next planned steps after this is done are to implement other operations on top/bottom materializations; probably attribute access is an important one. --------- Co-authored-by: Carl Meyer <[email protected]>
1 parent af259fa commit 18eaa65

File tree

10 files changed

+696
-191
lines changed

10 files changed

+696
-191
lines changed

crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md

Lines changed: 228 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ The invariant position is replaced with an unresolved type variable.
4747

4848
```py
4949
def _(top_list: Top[list[Any]]):
50-
reveal_type(top_list) # revealed: list[T_all]
50+
reveal_type(top_list) # revealed: Top[list[Any]]
5151
```
5252

5353
### Bottom materialization
@@ -75,7 +75,7 @@ type variable.
7575

7676
```py
7777
def _(bottom_list: Bottom[list[Any]]):
78-
reveal_type(bottom_list) # revealed: list[T_all]
78+
reveal_type(bottom_list) # revealed: Bottom[list[Any]]
7979
```
8080

8181
## Fully static types
@@ -230,14 +230,14 @@ def _(
230230
top_aiu: Top[LTAnyIntUnknown],
231231
bottom_aiu: Bottom[LTAnyIntUnknown],
232232
):
233-
reveal_type(top_ai) # revealed: list[tuple[T_all, int]]
234-
reveal_type(bottom_ai) # revealed: list[tuple[T_all, int]]
233+
reveal_type(top_ai) # revealed: Top[list[tuple[Any, int]]]
234+
reveal_type(bottom_ai) # revealed: Bottom[list[tuple[Any, int]]]
235235

236-
reveal_type(top_su) # revealed: list[tuple[str, T_all]]
237-
reveal_type(bottom_su) # revealed: list[tuple[str, T_all]]
236+
reveal_type(top_su) # revealed: Top[list[tuple[str, Unknown]]]
237+
reveal_type(bottom_su) # revealed: Bottom[list[tuple[str, Unknown]]]
238238

239-
reveal_type(top_aiu) # revealed: list[tuple[T_all, int, T_all]]
240-
reveal_type(bottom_aiu) # revealed: list[tuple[T_all, int, T_all]]
239+
reveal_type(top_aiu) # revealed: Top[list[tuple[Any, int, Unknown]]]
240+
reveal_type(bottom_aiu) # revealed: Bottom[list[tuple[Any, int, Unknown]]]
241241
```
242242

243243
## Union
@@ -286,14 +286,14 @@ def _(
286286
top_aiu: Top[list[Any | int | Unknown]],
287287
bottom_aiu: Bottom[list[Any | int | Unknown]],
288288
):
289-
reveal_type(top_ai) # revealed: list[T_all | int]
290-
reveal_type(bottom_ai) # revealed: list[T_all | int]
289+
reveal_type(top_ai) # revealed: Top[list[Any | int]]
290+
reveal_type(bottom_ai) # revealed: Bottom[list[Any | int]]
291291

292-
reveal_type(top_su) # revealed: list[str | T_all]
293-
reveal_type(bottom_su) # revealed: list[str | T_all]
292+
reveal_type(top_su) # revealed: Top[list[str | Unknown]]
293+
reveal_type(bottom_su) # revealed: Bottom[list[str | Unknown]]
294294

295-
reveal_type(top_aiu) # revealed: list[T_all | int]
296-
reveal_type(bottom_aiu) # revealed: list[T_all | int]
295+
reveal_type(top_aiu) # revealed: Top[list[Any | int]]
296+
reveal_type(bottom_aiu) # revealed: Bottom[list[Any | int]]
297297
```
298298

299299
## Intersection
@@ -320,8 +320,10 @@ def _(
320320
top: Top[Intersection[list[Any], list[int]]],
321321
bottom: Bottom[Intersection[list[Any], list[int]]],
322322
):
323-
reveal_type(top) # revealed: list[T_all] & list[int]
324-
reveal_type(bottom) # revealed: list[T_all] & list[int]
323+
# Top[list[Any] & list[int]] = Top[list[Any]] & list[int] = list[int]
324+
reveal_type(top) # revealed: list[int]
325+
# Bottom[list[Any] & list[int]] = Bottom[list[Any]] & list[int] = Bottom[list[Any]]
326+
reveal_type(bottom) # revealed: Bottom[list[Any]]
325327
```
326328

327329
## Negation (via `Not`)
@@ -366,8 +368,8 @@ static_assert(is_equivalent_to(Bottom[type[int | Any]], type[int]))
366368

367369
# Here, `T` has an upper bound of `type`
368370
def _(top: Top[list[type[Any]]], bottom: Bottom[list[type[Any]]]):
369-
reveal_type(top) # revealed: list[T_all]
370-
reveal_type(bottom) # revealed: list[T_all]
371+
reveal_type(top) # revealed: Top[list[type[Any]]]
372+
reveal_type(bottom) # revealed: Bottom[list[type[Any]]]
371373
```
372374

373375
## Type variables
@@ -427,8 +429,8 @@ class GenericContravariant(Generic[T_contra]):
427429
pass
428430

429431
def _(top: Top[GenericInvariant[Any]], bottom: Bottom[GenericInvariant[Any]]):
430-
reveal_type(top) # revealed: GenericInvariant[T_all]
431-
reveal_type(bottom) # revealed: GenericInvariant[T_all]
432+
reveal_type(top) # revealed: Top[GenericInvariant[Any]]
433+
reveal_type(bottom) # revealed: Bottom[GenericInvariant[Any]]
432434

433435
static_assert(is_equivalent_to(Top[GenericCovariant[Any]], GenericCovariant[object]))
434436
static_assert(is_equivalent_to(Bottom[GenericCovariant[Any]], GenericCovariant[Never]))
@@ -448,8 +450,8 @@ type CovariantCallable = Callable[[GenericCovariant[Any]], None]
448450
type ContravariantCallable = Callable[[GenericContravariant[Any]], None]
449451

450452
def invariant(top: Top[InvariantCallable], bottom: Bottom[InvariantCallable]) -> None:
451-
reveal_type(top) # revealed: (GenericInvariant[T_all], /) -> None
452-
reveal_type(bottom) # revealed: (GenericInvariant[T_all], /) -> None
453+
reveal_type(top) # revealed: (Bottom[GenericInvariant[Any]], /) -> None
454+
reveal_type(bottom) # revealed: (Top[GenericInvariant[Any]], /) -> None
453455

454456
def covariant(top: Top[CovariantCallable], bottom: Bottom[CovariantCallable]) -> None:
455457
reveal_type(top) # revealed: (GenericCovariant[Never], /) -> None
@@ -492,3 +494,207 @@ def _(
492494
bottom_1: Bottom[1], # error: [invalid-type-form]
493495
): ...
494496
```
497+
498+
## Nested use
499+
500+
`Top[T]` and `Bottom[T]` are always fully static types. Therefore, they have only one
501+
materialization (themselves) and applying `Top` or `Bottom` again does nothing.
502+
503+
```py
504+
from typing import Any
505+
from ty_extensions import Top, Bottom, static_assert, is_equivalent_to
506+
507+
static_assert(is_equivalent_to(Top[Top[list[Any]]], Top[list[Any]]))
508+
static_assert(is_equivalent_to(Bottom[Top[list[Any]]], Top[list[Any]]))
509+
510+
static_assert(is_equivalent_to(Bottom[Bottom[list[Any]]], Bottom[list[Any]]))
511+
static_assert(is_equivalent_to(Top[Bottom[list[Any]]], Bottom[list[Any]]))
512+
```
513+
514+
## Subtyping
515+
516+
Any `list[T]` is a subtype of `Top[list[Any]]`, but with more restrictive gradual types, not all
517+
other specializations are subtypes.
518+
519+
```py
520+
from typing import Any, Literal
521+
from ty_extensions import is_subtype_of, static_assert, Top, Intersection, Bottom
522+
523+
# None and Top
524+
static_assert(is_subtype_of(list[int], Top[list[Any]]))
525+
static_assert(not is_subtype_of(Top[list[Any]], list[int]))
526+
static_assert(is_subtype_of(list[bool], Top[list[Intersection[int, Any]]]))
527+
static_assert(is_subtype_of(list[int], Top[list[Intersection[int, Any]]]))
528+
static_assert(not is_subtype_of(list[int | str], Top[list[Intersection[int, Any]]]))
529+
static_assert(not is_subtype_of(list[object], Top[list[Intersection[int, Any]]]))
530+
static_assert(not is_subtype_of(list[str], Top[list[Intersection[int, Any]]]))
531+
static_assert(not is_subtype_of(list[str | bool], Top[list[Intersection[int, Any]]]))
532+
533+
# Top and Top
534+
static_assert(is_subtype_of(Top[list[int | Any]], Top[list[Any]]))
535+
static_assert(not is_subtype_of(Top[list[Any]], Top[list[int | Any]]))
536+
static_assert(is_subtype_of(Top[list[Intersection[int, Any]]], Top[list[Any]]))
537+
static_assert(not is_subtype_of(Top[list[Any]], Top[list[Intersection[int, Any]]]))
538+
static_assert(not is_subtype_of(Top[list[Intersection[int, Any]]], Top[list[int | Any]]))
539+
static_assert(not is_subtype_of(Top[list[int | Any]], Top[list[Intersection[int, Any]]]))
540+
static_assert(not is_subtype_of(Top[list[str | Any]], Top[list[int | Any]]))
541+
static_assert(is_subtype_of(Top[list[str | int | Any]], Top[list[int | Any]]))
542+
static_assert(not is_subtype_of(Top[list[int | Any]], Top[list[str | int | Any]]))
543+
544+
# Bottom and Top
545+
static_assert(is_subtype_of(Bottom[list[Any]], Top[list[Any]]))
546+
static_assert(is_subtype_of(Bottom[list[Any]], Top[list[int | Any]]))
547+
static_assert(is_subtype_of(Bottom[list[int | Any]], Top[list[Any]]))
548+
static_assert(is_subtype_of(Bottom[list[int | Any]], Top[list[int | str]]))
549+
static_assert(is_subtype_of(Bottom[list[Intersection[int, Any]]], Top[list[Intersection[str, Any]]]))
550+
static_assert(not is_subtype_of(Bottom[list[Intersection[int, bool | Any]]], Bottom[list[Intersection[str, Literal["x"] | Any]]]))
551+
552+
# None and None
553+
static_assert(not is_subtype_of(list[int], list[Any]))
554+
static_assert(not is_subtype_of(list[Any], list[int]))
555+
static_assert(is_subtype_of(list[int], list[int]))
556+
static_assert(not is_subtype_of(list[int], list[object]))
557+
static_assert(not is_subtype_of(list[object], list[int]))
558+
559+
# Top and None
560+
static_assert(not is_subtype_of(Top[list[Any]], list[Any]))
561+
static_assert(not is_subtype_of(Top[list[Any]], list[int]))
562+
static_assert(is_subtype_of(Top[list[int]], list[int]))
563+
564+
# Bottom and None
565+
static_assert(is_subtype_of(Bottom[list[Any]], list[object]))
566+
static_assert(is_subtype_of(Bottom[list[int | Any]], list[str | int]))
567+
static_assert(not is_subtype_of(Bottom[list[str | Any]], list[Intersection[int, bool | Any]]))
568+
569+
# None and Bottom
570+
static_assert(not is_subtype_of(list[int], Bottom[list[Any]]))
571+
static_assert(not is_subtype_of(list[int], Bottom[list[int | Any]]))
572+
static_assert(is_subtype_of(list[int], Bottom[list[int]]))
573+
574+
# Top and Bottom
575+
static_assert(not is_subtype_of(Top[list[Any]], Bottom[list[Any]]))
576+
static_assert(not is_subtype_of(Top[list[int | Any]], Bottom[list[int | Any]]))
577+
static_assert(is_subtype_of(Top[list[int]], Bottom[list[int]]))
578+
579+
# Bottom and Bottom
580+
static_assert(is_subtype_of(Bottom[list[Any]], Bottom[list[int | str | Any]]))
581+
static_assert(is_subtype_of(Bottom[list[int | Any]], Bottom[list[int | str | Any]]))
582+
static_assert(is_subtype_of(Bottom[list[bool | Any]], Bottom[list[int | Any]]))
583+
static_assert(not is_subtype_of(Bottom[list[int | Any]], Bottom[list[bool | Any]]))
584+
static_assert(not is_subtype_of(Bottom[list[int | Any]], Bottom[list[Any]]))
585+
```
586+
587+
## Assignability
588+
589+
### General
590+
591+
Assignability is the same as subtyping for top and bottom materializations, because those are fully
592+
static types, but some gradual types are assignable even if they are not subtypes.
593+
594+
```py
595+
from typing import Any, Literal
596+
from ty_extensions import is_assignable_to, static_assert, Top, Intersection, Bottom
597+
598+
# None and Top
599+
static_assert(is_assignable_to(list[Any], Top[list[Any]]))
600+
static_assert(is_assignable_to(list[int], Top[list[Any]]))
601+
static_assert(not is_assignable_to(Top[list[Any]], list[int]))
602+
static_assert(is_assignable_to(list[bool], Top[list[Intersection[int, Any]]]))
603+
static_assert(is_assignable_to(list[int], Top[list[Intersection[int, Any]]]))
604+
static_assert(is_assignable_to(list[Any], Top[list[Intersection[int, Any]]]))
605+
static_assert(not is_assignable_to(list[int | str], Top[list[Intersection[int, Any]]]))
606+
static_assert(not is_assignable_to(list[object], Top[list[Intersection[int, Any]]]))
607+
static_assert(not is_assignable_to(list[str], Top[list[Intersection[int, Any]]]))
608+
static_assert(not is_assignable_to(list[str | bool], Top[list[Intersection[int, Any]]]))
609+
610+
# Top and Top
611+
static_assert(is_assignable_to(Top[list[int | Any]], Top[list[Any]]))
612+
static_assert(not is_assignable_to(Top[list[Any]], Top[list[int | Any]]))
613+
static_assert(is_assignable_to(Top[list[Intersection[int, Any]]], Top[list[Any]]))
614+
static_assert(not is_assignable_to(Top[list[Any]], Top[list[Intersection[int, Any]]]))
615+
static_assert(not is_assignable_to(Top[list[Intersection[int, Any]]], Top[list[int | Any]]))
616+
static_assert(not is_assignable_to(Top[list[int | Any]], Top[list[Intersection[int, Any]]]))
617+
static_assert(not is_assignable_to(Top[list[str | Any]], Top[list[int | Any]]))
618+
static_assert(is_assignable_to(Top[list[str | int | Any]], Top[list[int | Any]]))
619+
static_assert(not is_assignable_to(Top[list[int | Any]], Top[list[str | int | Any]]))
620+
621+
# Bottom and Top
622+
static_assert(is_assignable_to(Bottom[list[Any]], Top[list[Any]]))
623+
static_assert(is_assignable_to(Bottom[list[Any]], Top[list[int | Any]]))
624+
static_assert(is_assignable_to(Bottom[list[int | Any]], Top[list[Any]]))
625+
static_assert(is_assignable_to(Bottom[list[Intersection[int, Any]]], Top[list[Intersection[str, Any]]]))
626+
static_assert(
627+
not is_assignable_to(Bottom[list[Intersection[int, bool | Any]]], Bottom[list[Intersection[str, Literal["x"] | Any]]])
628+
)
629+
630+
# None and None
631+
static_assert(is_assignable_to(list[int], list[Any]))
632+
static_assert(is_assignable_to(list[Any], list[int]))
633+
static_assert(is_assignable_to(list[int], list[int]))
634+
static_assert(not is_assignable_to(list[int], list[object]))
635+
static_assert(not is_assignable_to(list[object], list[int]))
636+
637+
# Top and None
638+
static_assert(is_assignable_to(Top[list[Any]], list[Any]))
639+
static_assert(not is_assignable_to(Top[list[Any]], list[int]))
640+
static_assert(is_assignable_to(Top[list[int]], list[int]))
641+
642+
# Bottom and None
643+
static_assert(is_assignable_to(Bottom[list[Any]], list[object]))
644+
static_assert(is_assignable_to(Bottom[list[int | Any]], Top[list[str | int]]))
645+
static_assert(not is_assignable_to(Bottom[list[str | Any]], list[Intersection[int, bool | Any]]))
646+
647+
# None and Bottom
648+
static_assert(is_assignable_to(list[Any], Bottom[list[Any]]))
649+
static_assert(not is_assignable_to(list[int], Bottom[list[Any]]))
650+
static_assert(not is_assignable_to(list[int], Bottom[list[int | Any]]))
651+
static_assert(is_assignable_to(list[int], Bottom[list[int]]))
652+
653+
# Top and Bottom
654+
static_assert(not is_assignable_to(Top[list[Any]], Bottom[list[Any]]))
655+
static_assert(not is_assignable_to(Top[list[int | Any]], Bottom[list[int | Any]]))
656+
static_assert(is_assignable_to(Top[list[int]], Bottom[list[int]]))
657+
658+
# Bottom and Bottom
659+
static_assert(is_assignable_to(Bottom[list[Any]], Bottom[list[int | str | Any]]))
660+
static_assert(is_assignable_to(Bottom[list[int | Any]], Bottom[list[int | str | Any]]))
661+
static_assert(is_assignable_to(Bottom[list[bool | Any]], Bottom[list[int | Any]]))
662+
static_assert(not is_assignable_to(Bottom[list[int | Any]], Bottom[list[bool | Any]]))
663+
static_assert(not is_assignable_to(Bottom[list[int | Any]], Bottom[list[Any]]))
664+
```
665+
666+
### Subclasses with different variance
667+
668+
We need to take special care when an invariant class inherits from a covariant or contravariant one.
669+
This comes up frequently in practice because `list` (invariant) inherits from `Sequence` and a
670+
number of other covariant ABCs, but we'll use a synthetic example.
671+
672+
```py
673+
from typing import Generic, TypeVar, Any
674+
from ty_extensions import static_assert, is_assignable_to, is_equivalent_to, Top
675+
676+
class A:
677+
pass
678+
679+
class B(A):
680+
pass
681+
682+
T_co = TypeVar("T_co", covariant=True)
683+
T = TypeVar("T")
684+
685+
class CovariantBase(Generic[T_co]):
686+
def get(self) -> T_co:
687+
raise NotImplementedError
688+
689+
class InvariantChild(CovariantBase[T]):
690+
def push(self, obj: T) -> None: ...
691+
692+
static_assert(is_assignable_to(InvariantChild[A], CovariantBase[A]))
693+
static_assert(is_assignable_to(InvariantChild[B], CovariantBase[A]))
694+
static_assert(not is_assignable_to(InvariantChild[A], CovariantBase[B]))
695+
static_assert(not is_assignable_to(InvariantChild[B], InvariantChild[A]))
696+
static_assert(is_equivalent_to(Top[CovariantBase[Any]], CovariantBase[object]))
697+
static_assert(is_assignable_to(InvariantChild[Any], CovariantBase[A]))
698+
699+
static_assert(not is_assignable_to(Top[InvariantChild[Any]], CovariantBase[A]))
700+
```

0 commit comments

Comments
 (0)