Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
145 changes: 142 additions & 3 deletions crates/ty_python_semantic/resources/mdtest/pep695_type_aliases.md
Original file line number Diff line number Diff line change
Expand Up @@ -930,6 +930,141 @@ type WrappedRight[T] = tuple[Box[Box[WrappedRight[list[T]]]]]
static_assert(not is_subtype_of(WrappedLeft[int], WrappedRight[int]))
```

### Recursive alias relations with finite specialization orbits

A recursive specialization can change its arguments while still reaching an exact repetition after
finitely many expansions. This includes shifting arguments to the left and resetting arguments to
types that do not depend on the current specialization.

```py
from typing import Protocol

from ty_extensions import Intersection, static_assert
from ty_extensions._internal import is_subtype_of

# Resetting the recursive argument makes these aliases reach a fixed specialization.
type L[T] = tuple[T] | tuple[T, L[int]]
type R[T] = tuple[T] | tuple[T, R[int]]

def _(left: L[str], right: R[str]):
right = left
left = right

type ShiftingLeft[A, B, C, D, E, F, G, H, I, J, K, L] = tuple[A, ShiftingLeft[B, C, D, E, F, G, H, I, J, K, L, None]]
type ShiftingRight[A, B, C, D, E, F, G, H, I, J, K, L] = tuple[A, ShiftingRight[B, C, D, E, F, G, H, I, J, K, L, None]]

static_assert(
is_subtype_of(
ShiftingLeft[int, int, int, int, int, int, int, int, int, int, int, int],
ShiftingRight[int, int, int, int, int, int, int, int, int, int, int, int],
)
)

type ShiftingSource = ShiftingLeft[int, int, int, int, int, int, int, int, int, int, int, int]
type ShiftingRightAfterTwo = ShiftingRight[int, int, int, int, int, int, int, int, int, int, None, None]
type ShiftingShortcut = tuple[int, tuple[int, ShiftingRightAfterTwo]]
type ShiftingLongPath = ShiftingRight[int, int, int, int, int, int, int, int, int, int, int, int]

static_assert(is_subtype_of(ShiftingSource, ShiftingShortcut))
static_assert(is_subtype_of(ShiftingSource, ShiftingShortcut | ShiftingLongPath))
static_assert(is_subtype_of(ShiftingSource, ShiftingLongPath | ShiftingShortcut))

type MutualLeft[T] = tuple[T, MutualLeftHelper[list[T]]]
type MutualLeftHelper[U] = tuple[U, MutualLeft[int]]
type MutualRight[T] = tuple[T, MutualRightHelper[list[T]]]
type MutualRightHelper[U] = tuple[U, MutualRight[int]]

static_assert(is_subtype_of(MutualLeft[str], MutualRight[str]))

# Repeatedly adding the same union element reaches a fixed point after one expansion.
type SaturatingLeft[T] = tuple[T, SaturatingLeft[T | int]]
type SaturatingRight[T] = tuple[T, SaturatingRight[T | int]]

static_assert(is_subtype_of(SaturatingLeft[bytes], SaturatingRight[bytes]))

# Repeatedly intersecting with the same type also reaches a fixed point.
type IntersectingLeft[T] = tuple[T, IntersectingLeft[Intersection[T, int]]]
type IntersectingRight[T] = tuple[T, IntersectingRight[Intersection[T, int]]]

static_assert(is_subtype_of(IntersectingLeft[object], IntersectingRight[object]))

# A structural wrapper still grows when it appears alongside or outside a saturating union.
type MixedGrowingLeft[T] = tuple[T, MixedGrowingLeft[T | list[T]]]
type MixedGrowingRight[T] = tuple[T, MixedGrowingRight[T | list[T]]]
type NestedSetGrowingLeft[T] = tuple[T, NestedSetGrowingLeft[list[T | int]]]
type NestedSetGrowingRight[T] = tuple[T, NestedSetGrowingRight[list[T | int]]]

# TODO: These structurally equivalent aliases should be recognized as subtypes.
static_assert(not is_subtype_of(MixedGrowingLeft[int], MixedGrowingRight[int]))
# TODO: These structurally equivalent aliases should be recognized as subtypes.
static_assert(not is_subtype_of(NestedSetGrowingLeft[int], NestedSetGrowingRight[int]))

# Alternating normalized set operations also reach a fixed point.
class SetElementA(Protocol):
a: int

class SetElementB(Protocol):
b: int

class SetElementC(Protocol):
c: int

type AlternatingSetLeft[T] = tuple[T, AlternatingSetLeftHelper[T | SetElementB]]
type AlternatingSetLeftHelper[U] = tuple[U, AlternatingSetLeft[Intersection[U, SetElementC]]]
type AlternatingSetRight[T] = tuple[T, AlternatingSetRightHelper[T | SetElementB]]
type AlternatingSetRightHelper[U] = tuple[U, AlternatingSetRight[Intersection[U, SetElementC]]]

static_assert(is_subtype_of(AlternatingSetLeft[SetElementA], AlternatingSetRight[SetElementA]))

# A specialization can also have a finite period greater than one.
type PeriodicLeft[A, B] = tuple[A, B, PeriodicLeft[B, A | int]]
type PeriodicRight[A, B] = tuple[A, B, PeriodicRight[B, A | int]]

static_assert(is_subtype_of(PeriodicLeft[bytes, str], PeriodicRight[bytes, str]))

# Neither recursive occurrence grows indefinitely by itself, but alternating between them adds
# another list layer on every cycle.
type AlternatingLeft[X, Y] = tuple[
AlternatingLeft[Y, None],
AlternatingLeft[None, list[X]],
]
type AlternatingRight[X, Y] = tuple[
AlternatingRight[Y, None],
AlternatingRight[None, list[X]],
]

# TODO: These structurally equivalent aliases should be recognized as subtypes.
static_assert(not is_subtype_of(AlternatingLeft[int, str], AlternatingRight[int, str]))

# The nested aliases grow their first argument, but the references back to the outer aliases erase
# that argument. The outer specialization orbits are therefore finite.
type OuterLeft[A, B] = NodeLeft[A, B]
type NodeLeft[A, B] = tuple[A, NodeLeft[list[A], B], OuterLeft[B, None]]
type OuterRight[A, B] = NodeRight[A, B]
type NodeRight[A, B] = tuple[A, NodeRight[list[A], B], OuterRight[None, B]]

# TODO: These structurally equivalent aliases should be recognized as subtypes.
static_assert(not is_subtype_of(OuterLeft[int, str], OuterRight[int, str]))

# If the reference back to the outer alias retains the growing argument, the outer specialization
# can grow transitively.
type TransitiveOuterLeft[T] = TransitiveNodeLeft[T]
type TransitiveNodeLeft[T] = tuple[
T,
TransitiveNodeLeft[list[T]],
TransitiveOuterLeft[T],
]
type TransitiveOuterRight[T] = TransitiveNodeRight[T]
type TransitiveNodeRight[T] = tuple[
T,
TransitiveNodeRight[list[T]],
TransitiveOuterRight[T],
]

# TODO: These structurally equivalent aliases should be recognized as subtypes.
static_assert(not is_subtype_of(TransitiveOuterLeft[int], TransitiveOuterRight[int]))
```

### Non-recursive nested generic aliases

A repeated use of the same generic alias can be a finite alias application instead of recursion.
Expand Down Expand Up @@ -1023,17 +1158,21 @@ def growing_callable(x: GrowingCallable[int]):
reveal_type(x())
```

Non-growing recursive aliases should continue to preserve distinct specializations.
If a type parameter never appears outside an unchanged recursive reference, different
specializations satisfy the same recursive equation and are equivalent.

```py
from ty_extensions import static_assert
from ty_extensions._internal import is_equivalent_to

type StableWrapped[T] = list[StableWrapped[T]]

static_assert(is_equivalent_to(StableWrapped[int], StableWrapped[str]))

def stable_wrapped(x: StableWrapped[int], y: StableWrapped[str]):
reveal_type(x) # revealed: list[StableWrapped[int]]
reveal_type(y) # revealed: list[StableWrapped[str]]
# error: [invalid-assignment] "Object of type `StableWrapped[str]` is not assignable to `StableWrapped[int]`"
x = y
# error: [invalid-assignment] "Object of type `StableWrapped[int]` is not assignable to `StableWrapped[str]`"
y = x
```

Expand Down
36 changes: 36 additions & 0 deletions crates/ty_python_semantic/resources/mdtest/protocols.md
Original file line number Diff line number Diff line change
Expand Up @@ -5631,6 +5631,42 @@ static_assert(not is_subtype_of(LeftAlias[int], RightAlias[int]))
# A conservative cycle fallback must not accept structurally different recursive protocols.
static_assert(not is_subtype_of(LeftProtocol[int], DifferentProtocol[int]))

class ShiftingLeftProtocol[A, B, C](Protocol):
@property
def value(self) -> A: ...
@property
def child(self) -> ShiftingLeftProtocol[B, C, None]: ...

class ShiftingRightProtocol[A, B, C](Protocol):
@property
def value(self) -> A: ...
@property
def child(self) -> ShiftingRightProtocol[B, C, None]: ...

# These recursive specializations reach an exact repetition after shifting out every initial
# argument.
static_assert(
is_subtype_of(
ShiftingLeftProtocol[int, str, bytes],
ShiftingRightProtocol[int, str, bytes],
)
)

class SaturatingLeftProtocol[T](Protocol):
@property
def value(self) -> T: ...
@property
def child(self) -> SaturatingLeftProtocol[T | int]: ...

class SaturatingRightProtocol[T](Protocol):
@property
def value(self) -> T: ...
@property
def child(self) -> SaturatingRightProtocol[T | int]: ...

# Repeatedly adding the same union element also reaches an exact repetition.
static_assert(is_subtype_of(SaturatingLeftProtocol[str], SaturatingRightProtocol[str]))

class FiniteLeft[T](Protocol):
value: T

Expand Down
28 changes: 28 additions & 0 deletions crates/ty_python_semantic/resources/mdtest/typed_dict.md
Original file line number Diff line number Diff line change
Expand Up @@ -2119,6 +2119,34 @@ static_assert(not is_subtype_of(LeftRecursiveDict[int], RightRecursiveDict[int])
# A conservative cycle fallback must not accept structurally different recursive TypedDicts.
static_assert(not is_subtype_of(LeftRecursiveDict[int], DifferentRecursiveDict[int]))

class ShiftingLeftDict[A, B, C](TypedDict):
value: A
child: ShiftingLeftDict[B, C, None]

class ShiftingRightDict[A, B, C](TypedDict):
value: A
child: ShiftingRightDict[B, C, None]

# These recursive specializations reach an exact repetition after shifting out every initial
# argument.
static_assert(
is_subtype_of(
ShiftingLeftDict[int, str, bytes],
ShiftingRightDict[int, str, bytes],
)
)

class SaturatingLeftDict[T](TypedDict):
value: T
child: SaturatingLeftDict[T | int]

class SaturatingRightDict[T](TypedDict):
value: T
child: SaturatingRightDict[T | int]

# Repeatedly adding the same union element also reaches an exact repetition.
static_assert(is_subtype_of(SaturatingLeftDict[str], SaturatingRightDict[str]))

class FiniteLeftDict[T](TypedDict):
value: T

Expand Down
Loading
Loading