Skip to content
Draft
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
160 changes: 156 additions & 4 deletions crates/ty_python_semantic/resources/mdtest/generics/set_theoretic.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,14 @@ This test suite explores the interplay between generics and set theoretic gradua
python-version = "3.14"
```

## Derivations and general results

This section concentrates on deriving the main results while the next section covers some more edge
cases.

```pyi
from typing import Any
from ty_extensions import static_assert, is_equivalent_to, is_subtype_of
from ty_extensions import Bottom, static_assert, is_equivalent_to, is_subtype_of
```

Throughout the document, we use the following classes as canonical examples for covariant,
Expand Down Expand Up @@ -192,12 +197,19 @@ Contra[P] & Contra[Any] = Contra[P | Any] (5b)
We can encode all of these in ty assertions:

```pyi
# TODO: all of these should pass
# TODO: both should pass
static_assert(is_equivalent_to(Co[P] | Co[Any], Co[P | Any])) # error: [static-assert-error]
static_assert(is_equivalent_to(Co[P] & Co[Any], Co[P & Any])) # error: [static-assert-error]
static_assert(is_equivalent_to(Co[Any] | Co[P], Co[P | Any])) # error: [static-assert-error]

static_assert(is_equivalent_to(Co[P] & Co[Any], Co[P & Any]))
static_assert(is_equivalent_to(Co[Any] & Co[P], Co[P & Any]))

# TODO: both should pass
static_assert(is_equivalent_to(Contra[P] | Contra[Any], Contra[P & Any])) # error: [static-assert-error]
static_assert(is_equivalent_to(Contra[P] & Contra[Any], Contra[P | Any])) # error: [static-assert-error]
static_assert(is_equivalent_to(Contra[Any] | Contra[P], Contra[P & Any])) # error: [static-assert-error]

static_assert(is_equivalent_to(Contra[P] & Contra[Any], Contra[P | Any]))
static_assert(is_equivalent_to(Contra[Any] & Contra[P], Contra[P | Any]))
```

What about invariance? We can naively write `Invariant[Any]` in its interval representation:
Expand Down Expand Up @@ -285,3 +297,143 @@ static_assert(is_equivalent_to(Invariant[P] & Invariant[Any], Invariant[P]))

static_assert(not is_equivalent_to(Invariant[P] | Invariant[Any], Invariant[P]))
```

We can also consider intersections with the negation of an `Any`-specialized generic class. For all
of the generic classes `C` above, we can negate the canonical interval representation of `C[Any]`:

```ignore
~C[Any]
= ~(Bottom[C[Any]] | Top[C[Any]] & Any)
= ~Bottom[C[Any]] & (~Top[C[Any]] | Any)
= ~Top[C[Any]] | ~Bottom[C[Any]] & Any
```

Every fully-static specialization `C[P]` is a subtype of `Top[C[Any]]`, therefore:

```ignore
C[P] & ~C[Any]
= C[P] & (~Top[C[Any]] | ~Bottom[C[Any]] & Any)
= C[P] & ~Bottom[C[Any]] & Any
```

For covariant and contravariant classes, we can simplify the bottom materializations as in (3a) and
(3b):

```ignore
Co[P] & ~Co[Any] = Co[P] & ~Co[Never] & Any
Contra[P] & ~Contra[Any] = Contra[P] & ~Contra[object] & Any
Invariant[P] & ~Invariant[Any] = Invariant[P] & ~Bottom[Invariant[Any]] & Any
```

We can verify all three relations in ty:

```pyi
static_assert(is_equivalent_to(Co[P] & ~Co[Any], Co[P] & ~Bottom[Co[Any]] & Any))
static_assert(is_equivalent_to(~Co[Any] & Co[P], Co[P] & ~Bottom[Co[Any]] & Any))

static_assert(is_equivalent_to(Contra[P] & ~Contra[Any], Contra[P] & ~Bottom[Contra[Any]] & Any))
static_assert(is_equivalent_to(~Contra[Any] & Contra[P], Contra[P] & ~Bottom[Contra[Any]] & Any))

static_assert(is_equivalent_to(Invariant[P] & ~Invariant[Any], Invariant[P] & ~Bottom[Invariant[Any]] & Any))
static_assert(is_equivalent_to(~Invariant[Any] & Invariant[P], Invariant[P] & ~Bottom[Invariant[Any]] & Any))
```

## Edge cases

### Multi-parameter and mixed-variance generics

The results above naturally extend to multi-parameter generics and mixed variances:

```pyi
from typing import Any, Generic, TypeVar
from ty_extensions import Bottom, static_assert, is_equivalent_to

class P: ...
class Q: ...
class R: ...

T_co = TypeVar("T_co", covariant=True)
T_contra = TypeVar("T_contra", contravariant=True)
T_invariant = TypeVar("T_invariant")

class Mixed(Generic[T_co, T_contra, T_invariant]): ...

static_assert(is_equivalent_to(Mixed[P, Q, R] & Mixed[Any, Any, Any], Mixed[P & Any, Q | Any, R]))
```

### Tuples

Tuple types are covariant in every type parameter, so the results derived for `Co[T]` above apply to
`tuple` at every position:

```pyi
from typing import Any, Never
from ty_extensions import static_assert, is_equivalent_to

class P: ...
class Q: ...

static_assert(is_equivalent_to(tuple[P] & tuple[Any], tuple[P & Any]))
static_assert(is_equivalent_to(tuple[Any] & tuple[P], tuple[P & Any]))

static_assert(is_equivalent_to(tuple[P] & ~tuple[Any], tuple[P] & ~tuple[Never] & Any))
static_assert(is_equivalent_to(~tuple[Any] & tuple[P], tuple[P] & ~tuple[Never] & Any))

static_assert(is_equivalent_to(tuple[P, Q] & tuple[Any, Q], tuple[P & Any, Q]))
static_assert(is_equivalent_to(tuple[Any, Q] & tuple[P, Q], tuple[P & Any, Q]))

static_assert(is_equivalent_to(tuple[P, Q] & tuple[P, Any], tuple[P, Q & Any]))
static_assert(is_equivalent_to(tuple[P, Any] & tuple[P, Q], tuple[P, Q & Any]))

static_assert(is_equivalent_to(tuple[P, Q] & tuple[Any, Any], tuple[P & Any, Q & Any]))
static_assert(is_equivalent_to(tuple[Any, Any] & tuple[P, Q], tuple[P & Any, Q & Any]))
```

Intersections with tuples of different length are not affected:

```pyi
static_assert(is_equivalent_to(tuple[int, str] & ~tuple[Any], tuple[int, str]))
static_assert(is_equivalent_to(tuple[int, str] & ~tuple[int, str, Any], tuple[int, str]))
```

### `type[...]`

`type[..]` can also be seen as a covariant type constructor, so the results also hold here:

```pyi
from typing import Any, Never
from ty_extensions import static_assert, is_equivalent_to

class P: ...
class Q: ...

static_assert(is_equivalent_to(type[P] & type[Any], type[P & Any]))
static_assert(is_equivalent_to(type[Any] & type[P], type[P & Any]))

static_assert(is_equivalent_to(type[P] & ~type[Any], type[P] & ~type[Never] & Any))
static_assert(is_equivalent_to(~type[Any] & type[P], type[P] & ~type[Never] & Any))
Comment on lines +413 to +414

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

type[Never] is probably Never? So ~type[Never] could be removed from the intersection. It seemed orthogonal to the PR here, so I left it for now.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

type[Never] is probably Never?

Yup

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

```

### Type var bounds and `NewTypes`

The simplification preserve the identities of type variables and `NewType` instances:

```pyi
from typing import Any, NewType
from ty_extensions import is_equivalent_to, static_assert

class P: ...
class Q: ...

class Co[T]:
def get(self) -> T:
raise NotImplementedError

CoId = NewType("CoId", Co[P])

def preserve_typevar[T: Co[P]](value: T & Co[Any]) -> T:
return value

def preserve_newtype(value: CoId & Co[Any]) -> CoId:
return value
```
Original file line number Diff line number Diff line change
Expand Up @@ -1455,7 +1455,7 @@ def expects_named_tuple(x: typing.NamedTuple):
reveal_type(x.__iter__)

def _(y: type[typing.NamedTuple]):
reveal_type(y) # revealed: @Todo(unsupported type[X] special form)
reveal_type(y) # revealed: type[tuple[object, ...]] & type[NamedTupleLike]

# error: [invalid-type-form] "Special form `typing.NamedTuple` expected no type parameter"
def _(z: typing.NamedTuple[int]): ...
Expand Down
2 changes: 1 addition & 1 deletion crates/ty_python_semantic/src/types/generics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1723,7 +1723,7 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
}
}

fn specialization_variance<'db>(
pub(super) fn specialization_variance<'db>(
db: &'db dyn Db,
bound_typevar: BoundTypeVarInstance<'db>,
) -> TypeVarVariance {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1244,7 +1244,9 @@ impl<'db> TypeInferenceBuilder<'db, '_> {
ast::Expr::Name(_) | ast::Expr::Attribute(_) | ast::Expr::StringLiteral(_) => {
infer_type_argument(self, slice)
}
ast::Expr::BinOp(binary) if binary.op == ast::Operator::BitOr => {
ast::Expr::BinOp(binary)
if matches!(binary.op, ast::Operator::BitOr | ast::Operator::BitAnd) =>
{
infer_type_argument(self, slice)
}
ast::Expr::Tuple(_) => {
Expand Down
1 change: 1 addition & 0 deletions crates/ty_python_semantic/src/types/set_theoretic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ use crate::types::{TypeVarBoundOrConstraints, visitor};
use crate::{Db, FxOrderSet};

pub(crate) mod builder;
mod generic_gradual_intersections;

pub(crate) use builder::{IntersectionBuilder, UnionBuilder};

Expand Down
Loading
Loading