mirrors/ruff
1
0
Fork 0
mirror of https://github.com/astral-sh/ruff.git synced 2025-08-04 10:48:32 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions 3

[ty] Type compendium (#18263)

Browse source 
## Summary

This is something I wrote a few months ago, and continued to update from
time to time. It was mostly written for my own education. I found a few
bugs while writing it at the time (there are still one or two TODOs in
the test assertions that are probably bugs). Our other tests are fairly
comprehensive, but they are usually structured around a certain
functionality or operation (subtyping, assignability, narrowing). The
idea here was to focus on individual *types and their properties*.

closes #197 (added `JustFloat` and `JustComplex` to `ty_extensions`).
This commit is contained in:
David Peter 2025-05-23 11:41:31 +02:00 • committed by GitHub
parent aae4482c55
commit 93ac0934dd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
11 changed files with 1210 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

20
crates/ty_python_semantic/resources/mdtest/type_compendium/README.md Normal file
View file

@ -0,0 +1,20 @@
# Type compendium
The type compendium contains "fact sheets" about important, interesting, and peculiar types in (ty's
interpretation of) Python's type system. It is meant to be an educational reference for developers
and users of ty. It is also a living document that ensures that our implementation of these types
and their properties is consistent with the specification.
## Table of contents
- [`Never`](never.md)
- [`Object`](object.md)
- [`None`](none.md)
- [Integer `Literal`s](integer_literals.md)
- String `Literal`s, `LiteralString`
- [`tuple` types](tuple.md)
- Class instance types
- [`Any`](any.md)
- Class literal types, `type[C]`, `type[object]`, `type[Any]`
- [`AlwaysTruthy`, `AlwaysFalsy`](always_truthy_falsy.md)
- [`Not[T]`](not_t.md)

175
crates/ty_python_semantic/resources/mdtest/type_compendium/always_truthy_falsy.md Normal file
View file

@ -0,0 +1,175 @@
# `AlwaysTruthy` and `AlwaysFalsy`
```toml
[environment]
python-version = "3.12"
```
The types `AlwaysTruthy` and `AlwaysFalsy` describe the set of values that are always truthy or
always falsy, respectively. More concretely, a value `at` is of type `AlwaysTruthy` if we can
statically infer that `bool(at)` is always `True`, i.e. that the expression `bool(at)` has type
`Literal[True]`. Conversely, a value `af` is of type `AlwaysFalsy` if we can statically infer that
`bool(af)` is always `False`, i.e. that `bool(af)` has type `Literal[False]`.
## Examples
Here, we give a few examples of values that belong to these types:
```py
from ty_extensions import AlwaysTruthy, AlwaysFalsy
from typing_extensions import Literal
class CustomAlwaysTruthyType:
def __bool__(self) -> Literal[True]:
return True
class CustomAlwaysFalsyType:
def __bool__(self) -> Literal[False]:
return False
at: AlwaysTruthy
at = True
at = 1
at = 123
at = -1
at = "non empty"
at = b"non empty"
at = CustomAlwaysTruthyType()
af: AlwaysFalsy
af = False
af = None
af = 0
af = ""
af = b""
af = CustomAlwaysFalsyType()
```
## `AlwaysTruthy` and `AlwaysFalsy` are disjoint
It follows directly from the definition that `AlwaysTruthy` and `AlwaysFalsy` are disjoint types:
```py
from ty_extensions import static_assert, is_disjoint_from, AlwaysTruthy, AlwaysFalsy
static_assert(is_disjoint_from(AlwaysTruthy, AlwaysFalsy))
```
## `Truthy` and `Falsy`
It is useful to also define the types `Truthy = ~AlwaysFalsy` and `Falsy = ~AlwaysTruthy`. These
types describe the set of values that *can* be truthy (`bool(t)` can return `True`) or falsy
(`bool(f)` can return `False`), respectively.
Finally, we can also define the type `AmbiguousTruthiness = Truthy & Falsy`, which describes the set
of values that can be truthy *and* falsy. This intersection is not empty. In the following, we give
examples for values that belong to these three types:
```py
from ty_extensions import static_assert, is_equivalent_to, is_disjoint_from, Not, Intersection, AlwaysTruthy, AlwaysFalsy
from typing_extensions import Never
from random import choice
type Truthy = Not[AlwaysFalsy]
type Falsy = Not[AlwaysTruthy]
type AmbiguousTruthiness = Intersection[Truthy, Falsy]
static_assert(is_disjoint_from(AlwaysTruthy, AmbiguousTruthiness))
static_assert(is_disjoint_from(AlwaysFalsy, AmbiguousTruthiness))
static_assert(not is_disjoint_from(Truthy, Falsy))
class CustomAmbiguousTruthinessType:
def __bool__(self) -> bool:
return choice((True, False))
def maybe_empty_list() -> list[int]:
return choice(([], [1, 2, 3]))
reveal_type(bool(maybe_empty_list())) # revealed: bool
reveal_type(bool(CustomAmbiguousTruthinessType())) # revealed: bool
t: Truthy
t = True
t = 1
# TODO: This assignment should be okay
t = maybe_empty_list() # error: [invalid-assignment]
# TODO: This assignment should be okay
t = CustomAmbiguousTruthinessType() # error: [invalid-assignment]
a: AmbiguousTruthiness
# TODO: This assignment should be okay
a = maybe_empty_list() # error: [invalid-assignment]
# TODO: This assignment should be okay
a = CustomAmbiguousTruthinessType() # error: [invalid-assignment]
f: Falsy
f = False
f = None
# TODO: This assignment should be okay
f = maybe_empty_list() # error: [invalid-assignment]
# TODO: This assignment should be okay
f = CustomAmbiguousTruthinessType() # error: [invalid-assignment]
```
## Subtypes of `AlwaysTruthy`, `AlwaysFalsy`
```py
from ty_extensions import static_assert, is_subtype_of, is_disjoint_from, AlwaysTruthy, AlwaysFalsy
from typing_extensions import Literal
```
These two types are disjoint, so types (that are not equivalent to Never) can only be a subtype of
either one of them.
```py
static_assert(is_disjoint_from(AlwaysTruthy, AlwaysFalsy))
```
Types that only contain always-truthy values
```py
static_assert(is_subtype_of(Literal[True], AlwaysTruthy))
static_assert(is_subtype_of(Literal[1], AlwaysTruthy))
static_assert(is_subtype_of(Literal[-1], AlwaysTruthy))
static_assert(is_subtype_of(Literal["non empty"], AlwaysTruthy))
static_assert(is_subtype_of(Literal[b"non empty"], AlwaysTruthy))
```
Types that only contain always-falsy values
```py
static_assert(is_subtype_of(None, AlwaysFalsy))
static_assert(is_subtype_of(Literal[False], AlwaysFalsy))
static_assert(is_subtype_of(Literal[0], AlwaysFalsy))
static_assert(is_subtype_of(Literal[""], AlwaysFalsy))
static_assert(is_subtype_of(Literal[b""], AlwaysFalsy))
static_assert(is_subtype_of(Literal[False] | Literal[0], AlwaysFalsy))
```
Ambiguous truthiness types
```py
static_assert(not is_subtype_of(bool, AlwaysTruthy))
static_assert(not is_subtype_of(bool, AlwaysFalsy))
static_assert(not is_subtype_of(list[int], AlwaysTruthy))
static_assert(not is_subtype_of(list[int], AlwaysFalsy))
```
## Open questions
Is `tuple[()]` always falsy? We currently model it this way, but this is
[under discussion](https://github.com/astral-sh/ruff/issues/15528).
```py
from ty_extensions import static_assert, is_subtype_of, AlwaysFalsy
static_assert(is_subtype_of(tuple[()], AlwaysFalsy))
```
## References
See also:
- Our test suite on [narrowing for `if x` and `if not x`](../narrow/truthiness.md).

141
crates/ty_python_semantic/resources/mdtest/type_compendium/any.md Normal file
View file

@ -0,0 +1,141 @@
# `Any`
## Introduction
The type `Any` is the dynamic type in Python's gradual type system. It represents an unknown
fully-static type, which means that it represents an *unknown* set of runtime values.
```py
from ty_extensions import static_assert, is_fully_static
from typing import Any
```
`Any` is a dynamic type:
```py
static_assert(not is_fully_static(Any))
```
## Every type is assignable to `Any`, and `Any` is assignable to every type
```py
from ty_extensions import static_assert, is_fully_static, is_assignable_to
from typing_extensions import Never, Any
class C: ...
static_assert(is_assignable_to(C, Any))
static_assert(is_assignable_to(Any, C))
static_assert(is_assignable_to(object, Any))
static_assert(is_assignable_to(Any, object))
static_assert(is_assignable_to(Never, Any))
static_assert(is_assignable_to(Any, Never))
static_assert(is_assignable_to(type, Any))
static_assert(is_assignable_to(Any, type))
static_assert(is_assignable_to(type[Any], Any))
static_assert(is_assignable_to(Any, type[Any]))
```
`Any` is also assignable to itself (like every type):
```py
static_assert(is_assignable_to(Any, Any))
```
## Unions with `Any`: `Any | T`
The union `Any | T` of `Any` with a fully static type `T` describes an unknown set of values that is
*at least as large* as the set of values described by `T`. It represents an unknown fully-static
type with *lower bound* `T`. Again, this can be demonstrated using the assignable-to relation:
```py
from ty_extensions import static_assert, is_assignable_to, is_equivalent_to
from typing_extensions import Any
# A class hierarchy Small <: Medium <: Big
class Big: ...
class Medium(Big): ...
class Small(Medium): ...
static_assert(is_assignable_to(Any | Medium, Big))
static_assert(is_assignable_to(Any | Medium, Medium))
# `Any | Medium` is at least as large as `Medium`, so we can not assign it to `Small`:
static_assert(not is_assignable_to(Any | Medium, Small))
```
The union `Any | object` is equivalent to `object`. This is true for every union with `object`, but
it is worth demonstrating:
```py
static_assert(is_equivalent_to(Any | object, object))
static_assert(is_equivalent_to(object | Any, object))
```
## Intersections with `Any`: `Any & T`
The intersection `Any & T` of `Any` with a fully static type `T` describes an unknown set of values
that is *no larger than* the set of values described by `T`. It represents an unknown fully-static
type with *upper bound* `T`:
```py
from ty_extensions import static_assert, is_assignable_to, Intersection, is_equivalent_to
from typing import Any
class Big: ...
class Medium(Big): ...
class Small(Medium): ...
static_assert(is_assignable_to(Small, Intersection[Any, Medium]))
static_assert(is_assignable_to(Medium, Intersection[Any, Medium]))
```
`Any & Medium` is no larger than `Medium`, so we can not assign `Big` to it. There is no possible
materialization of `Any & Medium` that would make it as big as `Big`:
```py
static_assert(not is_assignable_to(Big, Intersection[Any, Medium]))
```
`Any & Never` represents an "unknown" fully-static type which is no larger than `Never`. There is no
such fully-static type, except for `Never` itself. So `Any & Never` is equivalent to `Never`:
```py
from typing_extensions import Never
static_assert(is_equivalent_to(Intersection[Any, Never], Never))
static_assert(is_equivalent_to(Intersection[Never, Any], Never))
```
## Tuples with `Any`
This section demonstrates the following passage from the [type system concepts] documentation on
gradual types:
> A type such as `tuple[int, Any]` […] does not represent a single set of Python objects; rather, it
> represents a (bounded) range of possible sets of values. […] In the same way that `Any` does not
> represent "the set of all Python objects" but rather "an unknown set of objects",
> `tuple[int, Any]` does not represent "the set of all length-two tuples whose first element is an
> integer". That is a fully static type, spelled `tuple[int, object]`. By contrast,
> `tuple[int, Any]` represents some unknown set of tuple values; it might be the set of all tuples
> of two integers, or the set of all tuples of an integer and a string, or some other set of tuple
> values.
>
> In practice, this difference is seen (for example) in the fact that we can assign an expression of
> type `tuple[int, Any]` to a target typed as `tuple[int, int]`, whereas assigning
> `tuple[int, object]` to `tuple[int, int]` is a static type error.
```py
from ty_extensions import static_assert, is_assignable_to
from typing import Any
static_assert(is_assignable_to(tuple[int, Any], tuple[int, int]))
static_assert(not is_assignable_to(tuple[int, object], tuple[int, int]))
```
[type system concepts]: https://typing.readthedocs.io/en/latest/spec/concepts.html#gradual-types

234
crates/ty_python_semantic/resources/mdtest/type_compendium/integer_literals.md Normal file
View file

@ -0,0 +1,234 @@
# Integer `Literal`s
An integer literal type represents the set of all integer objects with one specific value. For
example, the type `Literal[54165]` represents the set of all integer objects with the value `54165`.
## Integer `Literal`s are not singleton types
This does not necessarily mean that the type is a singleton type, i.e., a type with only one
inhabitant. The reason for this is that there might be multiple Python runtime objects (at different
memory locations) that all represent the same integer value. For example, the following code snippet
may print `False`.
```py
x = 54165
y = 54165
print(x is y)
```
In practice, on CPython 3.13.0, this program prints `True` when executed as a script, but `False`
when executed in the REPL.
Since this is an implementation detail of the Python runtime, we model all integer literals as
non-singleton types:
```py
from ty_extensions import static_assert, is_singleton
from typing import Literal
static_assert(not is_singleton(Literal[0]))
static_assert(not is_singleton(Literal[1]))
static_assert(not is_singleton(Literal[54165]))
```
This has implications for type-narrowing. For example, you can not use the `is not` operator to
check whether a variable has a specific integer literal type, but this is not a recommended practice
anyway.
```py
def f(x: int):
if x is 54165:
# This works, because if `x` is the same object as that left-hand-side literal, then it
# must have the same value.
reveal_type(x) # revealed: Literal[54165]
if x is not 54165:
# But here, we can not narrow the type (to `int & ~Literal[54165]`), because `x` might also
# have the value `54165`, but a different object identity.
reveal_type(x) # revealed: int
```
## Integer `Literal`s are single-valued types
There is a slightly weaker property that integer literals have. They are single-valued types, which
means that all objects of the type have the same value, i.e. they compare equal to each other:
```py
from ty_extensions import static_assert, is_single_valued
from typing import Literal
static_assert(is_single_valued(Literal[0]))
static_assert(is_single_valued(Literal[1]))
static_assert(is_single_valued(Literal[54165]))
```
And this can be used for type-narrowing using not-equal comparisons:
```py
def f(x: int):
if x == 54165:
# The reason that no narrowing occurs here is that there might be subclasses of `int`
# that override `__eq__`. This is not specific to integer literals though, and generally
# applies to `==` comparisons.
reveal_type(x) # revealed: int
if x != 54165:
reveal_type(x) # revealed: int & ~Literal[54165]
```
## Subtyping relationships
### Subtypes of `int`
All integer literals are subtypes of `int`:
```py
from ty_extensions import static_assert, is_subtype_of
from typing import Literal
static_assert(is_subtype_of(Literal[0], int))
static_assert(is_subtype_of(Literal[1], int))
static_assert(is_subtype_of(Literal[54165], int))
```
It is tempting to think that `int` is equivalent to the union of all integer literals,
`… | Literal[-1] | Literal[0] | Literal[1] | …`, but this is not the case. `True` and `False` are
also inhabitants of the `int` type, but they are not inhabitants of any integer literal type:
```py
static_assert(is_subtype_of(Literal[True], int))
static_assert(is_subtype_of(Literal[False], int))
static_assert(not is_subtype_of(Literal[True], Literal[1]))
static_assert(not is_subtype_of(Literal[False], Literal[0]))
```
Also, `int` can be subclassed, and instances of that subclass are also subtypes of `int`:
```py
class CustomInt(int):
pass
static_assert(is_subtype_of(CustomInt, int))
```
### No subtypes of `float` and `complex`
```toml
[environment]
python-version = "3.12"
```
Integer literals are _not_ subtypes of `float`, but the typing spec describes a special case for
[`float` and `complex`] which accepts integers (and therefore also integer literals) in places where
a `float` or `complex` is expected. We use the types `JustFloat` and `JustComplex` below, because ty
recognizes an annotation of `float` as `int | float` to support that typing system special case.
```py
from ty_extensions import static_assert, is_subtype_of, JustFloat, JustComplex
from typing import Literal
# Not subtypes of `float` and `complex`
static_assert(not is_subtype_of(Literal[0], JustFloat) and not is_subtype_of(Literal[0], JustComplex))
static_assert(not is_subtype_of(Literal[1], JustFloat) and not is_subtype_of(Literal[1], JustComplex))
static_assert(not is_subtype_of(Literal[54165], JustFloat) and not is_subtype_of(Literal[54165], JustComplex))
```
The typing system special case can be seen in the following example:
```py
a: JustFloat = 1 # error: [invalid-assignment]
b: JustComplex = 1 # error: [invalid-assignment]
x: float = 1
y: complex = 1
```
### Subtypes of integer `Literal`s?
The only subtypes of an integer literal type _that can be named_ are the type itself and `Never`:
```py
from ty_extensions import static_assert, is_subtype_of
from typing_extensions import Never, Literal
static_assert(is_subtype_of(Literal[54165], Literal[54165]))
static_assert(is_subtype_of(Never, Literal[54165]))
```
## Disjointness of integer `Literal`s
Two integer literal types `Literal[a]` and `Literal[b]` are disjoint if `a != b`:
```py
from ty_extensions import static_assert, is_disjoint_from
from typing import Literal
static_assert(is_disjoint_from(Literal[0], Literal[1]))
static_assert(is_disjoint_from(Literal[0], Literal[54165]))
static_assert(not is_disjoint_from(Literal[0], Literal[0]))
static_assert(not is_disjoint_from(Literal[54165], Literal[54165]))
```
## Integer literal math
```toml
[environment]
python-version = "3.12"
```
We support a whole range of arithmetic operations on integer literal types. For example, we can
statically verify that (3, 4, 5) is a Pythagorean triple:
```py
from ty_extensions import static_assert
static_assert(3**2 + 4**2 == 5**2)
```
Using unions of integer literals, we can even use this to solve equations over a finite domain
(determine whether there is a solution or not):
```py
from typing import Literal, assert_type
type Nat = Literal[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
def pythagorean_triples(a: Nat, b: Nat, c: Nat):
# Answer is `bool`, because solutions do exist (3² + 4² = 5²)
assert_type(a**2 + b**2 == c**2, bool)
def fermats_last_theorem(a: Nat, b: Nat, c: Nat):
# Answer is `Literal[False]`, because no solutions exist
assert_type(a**3 + b**3 == c**3, Literal[False])
```
## Truthiness
Integer literals are always-truthy, except for `0`, which is always-falsy:
```py
from ty_extensions import static_assert
static_assert(-54165)
static_assert(-1)
static_assert(not 0)
static_assert(1)
static_assert(54165)
```
This can be used for type-narrowing:
```py
from typing_extensions import Literal, assert_type
def f(x: Literal[0, 1, 54365]):
if x:
assert_type(x, Literal[1, 54365])
else:
assert_type(x, Literal[0])
```
[`float` and `complex`]: https://typing.readthedocs.io/en/latest/spec/special-types.html#special-cases-for-float-and-complex

185
crates/ty_python_semantic/resources/mdtest/type_compendium/never.md Normal file
View file

@ -0,0 +1,185 @@
# `Never`
`Never` represents the empty set of values.
## `Never` is a subtype of every type
The `Never` type is the bottom type of Python's type system. It is a subtype of every type, but no
type is a subtype of `Never`, except for `Never` itself.
```py
from ty_extensions import static_assert, is_subtype_of
from typing_extensions import Never
class C: ...
static_assert(is_subtype_of(Never, int))
static_assert(is_subtype_of(Never, object))
static_assert(is_subtype_of(Never, C))
static_assert(is_subtype_of(Never, Never))
static_assert(not is_subtype_of(int, Never))
```
## `Never` is assignable to every type
`Never` is assignable to every type. This fact is useful when calling error-handling functions in a
context that requires a value of a specific type. For example, changing the `Never` return type to
`None` below would cause a type error:
```py
from ty_extensions import static_assert, is_assignable_to
from typing_extensions import Never, Any
static_assert(is_assignable_to(Never, int))
static_assert(is_assignable_to(Never, object))
static_assert(is_assignable_to(Never, Any))
static_assert(is_assignable_to(Never, Never))
def raise_error() -> Never:
raise Exception("...")
def f(divisor: int) -> None:
x: float = (1 / divisor) if divisor != 0 else raise_error()
```
## `Never` in annotations
`Never` can be used in functions to indicate that the function never returns. For example, if a
function always raises an exception, if it calls `sys.exit()`, if it enters an infinite loop, or if
it calls itself recursively. All of these functions "Never" return control back to the caller:
```py
from typing_extensions import Never
def raises_unconditionally() -> Never:
raise Exception("This function always raises an exception")
def exits_unconditionally() -> Never:
import sys
return sys.exit(1)
def loops_forever() -> Never:
while True:
pass
def recursive_never() -> Never:
return recursive_never()
```
Similarly, if `Never` is used in parameter positions, it indicates that the function can "Never" be
called, because it can never be passed a value of type `Never` (there are none):
```py
def can_not_be_called(n: Never) -> int:
return 0
```
## `Never` is disjoint from every other type
Two types `A` and `B` are disjoint if their intersection is empty. Since `Never` has no inhabitants,
it is disjoint from every other type:
```py
from ty_extensions import static_assert, is_disjoint_from
from typing_extensions import Never
class C: ...
static_assert(is_disjoint_from(Never, int))
static_assert(is_disjoint_from(Never, object))
static_assert(is_disjoint_from(Never, C))
static_assert(is_disjoint_from(Never, Never))
```
## Unions with `Never`
`Never` can always be removed from unions:
```py
from ty_extensions import static_assert, is_equivalent_to
from typing_extensions import Never
class P: ...
class Q: ...
static_assert(is_equivalent_to(P | Never | Q | None, P | Q | None))
```
## Intersections with `Never`
Intersecting with `Never` results in `Never`:
```py
from ty_extensions import static_assert, is_equivalent_to, Intersection
from typing_extensions import Never
class P: ...
class Q: ...
static_assert(is_equivalent_to(Intersection[P, Never, Q], Never))
```
## `Never` is the complement of `object`
`object` describes the set of all possible values, while `Never` describes the empty set. The two
types are complements of each other:
```py
from ty_extensions import static_assert, is_equivalent_to, Not
from typing_extensions import Never
static_assert(is_equivalent_to(Not[object], Never))
static_assert(is_equivalent_to(Not[Never], object))
```
This duality is also reflected in other facts:
- `Never` is a subtype of every type, while `object` is a supertype of every type.
- `Never` is assignable to every type, while `object` is assignable from every type.
- `Never` is disjoint from every type, while `object` overlaps with every type.
- Building a union with `Never` is a no-op, intersecting with `object` is a no-op.
- Interecting with `Never` results in `Never`, building a union with `object` results in `object`.
## Lists of `Never`
`list[Never]` is a reasonable type that is *not* equivalent to `Never`. The empty list inhabits this
type:
```py
from typing_extensions import Never
x: list[Never] = []
```
## Tuples involving `Never`
A type like `tuple[int, Never]` has no inhabitants, and so it is equivalent to `Never`:
```py
from ty_extensions import static_assert, is_equivalent_to
from typing_extensions import Never
static_assert(is_equivalent_to(tuple[int, Never], Never))
```
Note that this is not the case for the homogenous tuple type `tuple[Never, ...]` though, because
that type is inhabited by the empty tuple:
```py
static_assert(not is_equivalent_to(tuple[Never, ...], Never))
t: tuple[Never, ...] = ()
```
## `NoReturn` is the same as `Never`
The `NoReturn` type is a different name for `Never`:
```py
from ty_extensions import static_assert, is_equivalent_to
from typing_extensions import NoReturn, Never
static_assert(is_equivalent_to(NoReturn, Never))
```

80
crates/ty_python_semantic/resources/mdtest/type_compendium/none.md Normal file
View file

@ -0,0 +1,80 @@
# `None`
## `None` as a singleton type
The type `None` (or `NoneType`, see below) is a singleton type that has only one inhabitant: the
object `None`.
```py
from ty_extensions import static_assert, is_singleton, is_equivalent_to
n: None = None
static_assert(is_singleton(None))
```
Just like for other singleton types, the only subtypes of `None` are `None` itself and `Never`:
```py
from ty_extensions import static_assert, is_subtype_of
from typing_extensions import Never
static_assert(is_subtype_of(None, None))
static_assert(is_subtype_of(Never, None))
```
## Relationship to `Optional[T]`
The type `Optional[T]` is an alias for `T | None` (or `Union[T, None]`):
```py
from ty_extensions import static_assert, is_equivalent_to
from typing import Optional, Union
class T: ...
static_assert(is_equivalent_to(Optional[T], T | None))
static_assert(is_equivalent_to(Optional[T], Union[T, None]))
```
## Type narrowing using `is`
Just like for other singleton types, we support type narrowing using `is` or `is not` checks:
```py
from typing_extensions import assert_type
class T: ...
def f(x: T | None):
if x is None:
assert_type(x, None)
else:
assert_type(x, T)
assert_type(x, T | None)
if x is not None:
assert_type(x, T)
else:
assert_type(x, None)
```
## `NoneType`
`None` is special in that the name of the instance at runtime can be used as a type as well: The
object `None` is an instance of type `None`. When a distinction between the two is needed, the
spelling `NoneType` can be used, which is available since Python 3.10. `NoneType` is equivalent to
`None`:
```toml
[environment]
python-version = "3.10"
```
```py
from ty_extensions import static_assert, is_equivalent_to
from types import NoneType
static_assert(is_equivalent_to(NoneType, None))
```

120
crates/ty_python_semantic/resources/mdtest/type_compendium/not_t.md Normal file
View file

@ -0,0 +1,120 @@
# `Not[T]`
The type `Not[T]` is the complement of the type `T`. It describes the set of all values that are
*not* in `T`.
## `Not[T]` is disjoint from `T`
`Not[T]` is disjoint from `T`:
```py
from ty_extensions import Not, static_assert, is_disjoint_from
class T: ...
class S(T): ...
static_assert(is_disjoint_from(Not[T], T))
static_assert(is_disjoint_from(Not[T], S))
```
## The union of `T` and `Not[T]` is equivalent to `object`
Together, `T` and `Not[T]` describe the set of all values. So the union of both types is equivalent
to `object`:
```py
from ty_extensions import Not, static_assert, is_equivalent_to
class T: ...
static_assert(is_equivalent_to(T | Not[T], object))
```
## `Not[T]` reverses subtyping relationships
If `S <: T`, then `Not[T] <: Not[S]`:, similar to how negation in logic reverses the order of `<=`:
```py
from ty_extensions import Not, static_assert, is_subtype_of
class T: ...
class S(T): ...
static_assert(is_subtype_of(S, T))
static_assert(is_subtype_of(Not[T], Not[S]))
```
## `Not[T]` reverses assignability relationships
Assignability relationships are similarly reversed:
```py
from ty_extensions import Not, Intersection, static_assert, is_assignable_to
from typing import Any
class T: ...
class S(T): ...
static_assert(is_assignable_to(S, T))
static_assert(is_assignable_to(Not[T], Not[S]))
static_assert(is_assignable_to(Intersection[Any, S], Intersection[Any, T]))
static_assert(is_assignable_to(Not[Intersection[Any, S]], Not[Intersection[Any, T]]))
```
## Subtyping and disjointness
If two types `P` and `Q` are disjoint, then `P` must be a subtype of `Not[Q]`, and vice versa:
```py
from ty_extensions import Not, static_assert, is_subtype_of, is_disjoint_from
from typing import final
@final
class P: ...
@final
class Q: ...
static_assert(is_disjoint_from(P, Q))
static_assert(is_subtype_of(P, Not[Q]))
static_assert(is_subtype_of(Q, Not[P]))
```
## De-Morgan's laws
Given two unrelated types `P` and `Q`, we can demonstrate De-Morgan's laws in the context of
set-theoretic types:
```py
from ty_extensions import Not, static_assert, is_equivalent_to, Intersection
class P: ...
class Q: ...
```
The negation of a union is the intersection of the negations:
```py
static_assert(is_equivalent_to(Not[P | Q], Intersection[Not[P], Not[Q]]))
```
Conversely, the negation of an intersection is the union of the negations:
```py
static_assert(is_equivalent_to(Not[Intersection[P, Q]], Not[P] | Not[Q]))
```
## Negation of gradual types
`Any` represents an unknown set of values. So `Not[Any]` also represents an unknown set of values.
The two gradual types are equivalent:
```py
from ty_extensions import static_assert, is_gradual_equivalent_to, Not
from typing import Any
static_assert(is_gradual_equivalent_to(Not[Any], Any))
```

78
crates/ty_python_semantic/resources/mdtest/type_compendium/object.md Normal file
View file

@ -0,0 +1,78 @@
# `object`
The `object` type represents the set of all Python objects.
## `object` is a supertype of all types
It is the top type in Python's type system, i.e., it is a supertype of all other types:
```py
from ty_extensions import static_assert, is_subtype_of
static_assert(is_subtype_of(int, object))
static_assert(is_subtype_of(str, object))
static_assert(is_subtype_of(type, object))
static_assert(is_subtype_of(object, object))
```
## Every type is assignable to `object`
Everything can be assigned to the type `object`. This fact can be used to create heterogeneous
collections of objects (but also erases more specific type information):
```py
from ty_extensions import static_assert, is_assignable_to
from typing_extensions import Any, Never
static_assert(is_assignable_to(int, object))
static_assert(is_assignable_to(str | bytes, object))
static_assert(is_assignable_to(type, object))
static_assert(is_assignable_to(object, object))
static_assert(is_assignable_to(Never, object))
static_assert(is_assignable_to(Any, object))
x: list[object] = [1, "a", ()]
```
## `object` overlaps with all types
There is no type that is disjoint from `object` except for `Never`:
```py
from ty_extensions import static_assert, is_disjoint_from
from typing_extensions import Any, Never
static_assert(not is_disjoint_from(int, object))
static_assert(not is_disjoint_from(str, object))
static_assert(not is_disjoint_from(type, object))
static_assert(not is_disjoint_from(object, object))
static_assert(not is_disjoint_from(Any, object))
static_assert(is_disjoint_from(Never, object))
```
## Unions with `object`
Unions with `object` are equivalent to `object`:
```py
from ty_extensions import static_assert, is_equivalent_to
static_assert(is_equivalent_to(int | object | None, object))
```
## Intersections with `object`
Intersecting with `object` is equivalent to the original type:
```py
from ty_extensions import static_assert, is_equivalent_to, Intersection
class P: ...
class Q: ...
static_assert(is_equivalent_to(Intersection[P, object, Q], Intersection[P, Q]))
```
## `object` is the complement of `Never`
See corresponding section in the fact sheet for [`Never`](never.md).

166
crates/ty_python_semantic/resources/mdtest/type_compendium/tuple.md Normal file
View file

@ -0,0 +1,166 @@
# Tuples
## Tuples as product types
Tuples can be used to construct product types. Inhabitants of the type `tuple[P, Q]` are ordered
pairs `(p, q)` where `p` is an inhabitant of `P` and `q` is an inhabitant of `Q`, analogous to the
Cartesian product of sets.
```py
from typing_extensions import assert_type
class P: ...
class Q: ...
def _(p: P, q: Q):
assert_type((p, q), tuple[P, Q])
```
## Subtyping relationships
The type `tuple[S1, S2]` is a subtype of `tuple[T1, T2]` if and only if `S1` is a subtype of `T1`
and `S2` is a subtype of `T2`, and similar for other lengths of tuples:
```py
from ty_extensions import static_assert, is_subtype_of
class T1: ...
class S1(T1): ...
class T2: ...
class S2(T2): ...
static_assert(is_subtype_of(tuple[S1], tuple[T1]))
static_assert(not is_subtype_of(tuple[T1], tuple[S1]))
static_assert(is_subtype_of(tuple[S1, S2], tuple[T1, T2]))
static_assert(not is_subtype_of(tuple[T1, S2], tuple[S1, T2]))
static_assert(not is_subtype_of(tuple[S1, T2], tuple[T1, S2]))
```
Different-length tuples are not related via subtyping:
```py
static_assert(not is_subtype_of(tuple[S1], tuple[T1, T2]))
```
## The empty tuple
The type of the empty tuple `()` is spelled `tuple[()]`. It is [not a singleton type], because
different instances of `()` are not guaranteed to be the same object (even if this is the case in
CPython at the time of writing).
The empty tuple can also be subclassed (further clarifying that it is not a singleton type):
```py
from ty_extensions import static_assert, is_singleton, is_subtype_of, is_equivalent_to, is_assignable_to
static_assert(not is_singleton(tuple[()]))
class AnotherEmptyTuple(tuple[()]): ...
static_assert(not is_equivalent_to(AnotherEmptyTuple, tuple[()]))
# TODO: These should not be errors
# error: [static-assert-error]
static_assert(is_subtype_of(AnotherEmptyTuple, tuple[()]))
# error: [static-assert-error]
static_assert(is_assignable_to(AnotherEmptyTuple, tuple[()]))
```
## Non-empty tuples
For the same reason as above (two instances of a tuple with the same elements might not be the same
object), non-empty tuples are also not singleton types — even if all their elements are singletons:
```py
from ty_extensions import static_assert, is_singleton
static_assert(is_singleton(None))
static_assert(not is_singleton(tuple[None]))
```
## Disjointness
A tuple `tuple[P1, P2]` is disjoint from a tuple `tuple[Q1, Q2]` if either `P1` is disjoint from
`Q1` or if `P2` is disjoint from `Q2`:
```py
from ty_extensions import static_assert, is_disjoint_from
from typing import final
@final
class F1: ...
@final
class F2: ...
class N1: ...
class N2: ...
static_assert(is_disjoint_from(F1, F2))
static_assert(not is_disjoint_from(N1, N2))
static_assert(is_disjoint_from(tuple[F1, F2], tuple[F2, F1]))
static_assert(is_disjoint_from(tuple[F1, N1], tuple[F2, N2]))
static_assert(is_disjoint_from(tuple[N1, F1], tuple[N2, F2]))
static_assert(not is_disjoint_from(tuple[N1, N2], tuple[N2, N1]))
```
We currently model tuple types to *not* be disjoint from arbitrary instance types, because we allow
for the possibility of `tuple` to be subclassed
```py
class C: ...
static_assert(not is_disjoint_from(tuple[int, str], C))
class CommonSubtype(tuple[int, str], C): ...
```
Note: This is inconsistent with the fact that we model heterogeneous tuples to be disjoint from
other heterogeneous tuples above:
```py
class I1(tuple[F1, F2]): ...
class I2(tuple[F2, F1]): ...
# TODO
# This is a subtype of both `tuple[F1, F2]` and `tuple[F2, F1]`, so those two heterogeneous tuples
# should not be disjoint from each other (see conflicting test above).
class CommonSubtypeOfTuples(I1, I2): ...
```
## Truthiness
The truthiness of the empty tuple is `False`:
```py
from typing_extensions import assert_type, Literal
assert_type(bool(()), Literal[False])
```
The truthiness of non-empty tuples is always `True`, even if all elements are falsy:
```py
from typing_extensions import assert_type, Literal
assert_type(bool((False,)), Literal[True])
assert_type(bool((False, False)), Literal[True])
```
Both of these results are conflicting with the fact that tuples can be subclassed, and that we
currently allow subclasses of `tuple` to overwrite `__bool__` (or `__len__`):
```py
class NotAlwaysTruthyTuple(tuple[int]):
def __bool__(self) -> bool:
return False
# TODO: This assignment should be allowed
# error: [invalid-assignment]
t: tuple[int] = NotAlwaysTruthyTuple((1,))
```
[not a singleton type]: https://discuss.python.org/t/should-we-specify-in-the-language-reference-that-the-empty-tuple-is-a-singleton/67957

9
crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
View file

@ -21,10 +21,7 @@ See the [typing documentation] for more information.
as `int | float` and `int | float | complex`, respectively.
```py
from ty_extensions import is_subtype_of, static_assert, TypeOf
type JustFloat = TypeOf[1.0]
type JustComplex = TypeOf[1j]
from ty_extensions import is_subtype_of, static_assert, JustFloat, JustComplex
static_assert(is_subtype_of(bool, bool))
static_assert(is_subtype_of(bool, int))
@ -88,9 +85,7 @@ static_assert(is_subtype_of(C, object))
```py
from typing_extensions import Literal, LiteralString
from ty_extensions import is_subtype_of, static_assert, TypeOf
type JustFloat = TypeOf[1.0]
from ty_extensions import is_subtype_of, static_assert, TypeOf, JustFloat
# Boolean literals
static_assert(is_subtype_of(Literal[True], bool))

9
crates/ty_vendored/ty_extensions/ty_extensions.pyi
View file

@ -14,6 +14,15 @@ Intersection: _SpecialForm
TypeOf: _SpecialForm
CallableTypeOf: _SpecialForm
# ty treats annotations of `float` to mean `float | int`, and annotations of `complex`
# to mean `complex | float | int`. This is to support a typing-system special case [1].
# We therefore provide `JustFloat` and `JustComplex` to represent the "bare" `float` and
# `complex` types, respectively.
#
# [1]: https://typing.readthedocs.io/en/latest/spec/special-types.html#special-cases-for-float-and-complex
type JustFloat = TypeOf[1.0]
type JustComplex = TypeOf[1.0j]
# Predicates on types
#
# Ideally, these would be annotated using `TypeForm`, but that has not been