add quantification test cases
This commit is contained in:
Douglas Creager
@@ -416,19 +416,44 @@ def mutually_bound[T: Base, U]():
|
||||
|
||||
## Nested typevars
|
||||
|
||||
A typevar's constraint can _mention_ another typevar without _constraining_ it. In this example, `U`
|
||||
must be specialized to `list[T]`, but it cannot affect what `T` is specialized to.
|
||||
The specialization of one typevar can affect the specialization of another, even if it is not a
|
||||
"top-level" type in the bounds. (That is, if it appears as inside the specialization of a generic
|
||||
class.)
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions import ConstraintSet, generic_context
|
||||
|
||||
def mentions[T, U]():
|
||||
# (T@mentions ≤ int) ∧ (U@mentions = list[T@mentions])
|
||||
constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(list[T], U, list[T])
|
||||
# TODO: revealed: ty_extensions.Specialization[T@mentions = int, U@mentions = list[int]]
|
||||
# revealed: ty_extensions.Specialization[T@mentions = int, U@mentions = Unknown]
|
||||
reveal_type(generic_context(mentions).specialize_constrained(constraints))
|
||||
class Covariant[T]:
|
||||
def get(self) -> T:
|
||||
raise NotImplementedError
|
||||
|
||||
class Contravariant[T]:
|
||||
def receive(self, input: T): ...
|
||||
|
||||
class Invariant[T]:
|
||||
mutable_attribute: T
|
||||
|
||||
def mentions_covariant[T, U]():
|
||||
# (T@mentions_covariant ≤ int) ∧ (U@mentions_covariant ≤ Covariant[T@mentions_covariant])
|
||||
constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Never, U, Covariant[T])
|
||||
# TODO: revealed: ty_extensions.Specialization[T@mentions_covariant = int, U@mentions_covariant = Covariant[int]]
|
||||
# revealed: ty_extensions.Specialization[T@mentions_covariant = int, U@mentions_covariant = Unknown]
|
||||
reveal_type(generic_context(mentions_covariant).specialize_constrained(constraints))
|
||||
|
||||
def mentions_contravariant[T, U]():
|
||||
# (T@mentions_contravariant ≤ int) ∧ (Contravariant[T@mentions_contravariant] ≤ U@mentions_contravariant)
|
||||
constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Contravariant[T], U, object)
|
||||
# TODO: revealed: ty_extensions.Specialization[T@mentions_contravariant = int, U@mentions_contravariant = Contravariant[int]]
|
||||
# revealed: ty_extensions.Specialization[T@mentions_contravariant = int, U@mentions_contravariant = Unknown]
|
||||
reveal_type(generic_context(mentions_contravariant).specialize_constrained(constraints))
|
||||
|
||||
def mentions_invariant[T, U]():
|
||||
# (T@mentions_invariant ≤ int) ∧ (U@mentions_invariant = Invariant[T@mentions_invariant])
|
||||
constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Invariant[T], U, Invariant[T])
|
||||
# TODO: revealed: ty_extensions.Specialization[T@mentions_invariant = int, U@mentions_invariant = Invariant[int]]
|
||||
# revealed: ty_extensions.Specialization[T@mentions_invariant = int, U@mentions_invariant = Unknown]
|
||||
reveal_type(generic_context(mentions_invariant).specialize_constrained(constraints))
|
||||
```
|
||||
|
||||
If the constraint set contains mutually recursive bounds, specialization inference will not
|
||||
@@ -437,8 +462,8 @@ this case.
|
||||
|
||||
```py
|
||||
def divergent[T, U]():
|
||||
# (T@divergent = list[U@divergent]) ∧ (U@divergent = list[T@divergent]))
|
||||
constraints = ConstraintSet.range(list[U], T, list[U]) & ConstraintSet.range(list[T], U, list[T])
|
||||
# (T@divergent = Invariant[U@divergent]) ∧ (U@divergent = Invariant[T@divergent]))
|
||||
constraints = ConstraintSet.range(Invariant[U], T, Invariant[U]) & ConstraintSet.range(Invariant[T], U, Invariant[T])
|
||||
# revealed: None
|
||||
reveal_type(generic_context(divergent).specialize_constrained(constraints))
|
||||
```
|
||||
|
||||
@@ -0,0 +1,279 @@
|
||||
# Constraint set quantification
|
||||
|
||||
```toml
|
||||
[environment]
|
||||
python-version = "3.12"
|
||||
```
|
||||
|
||||
We can _existentially quantify_ a constraint set over a type variable. The result is a copy of the
|
||||
constraint set that only mentions the requested typevar. All constraints mentioning any other
|
||||
typevars are removed. Importantly, they are removed "safely", with their constraints propagated
|
||||
through to the remaining constraints as needed.
|
||||
|
||||
## Keeping a single typevar
|
||||
|
||||
If a constraint set only mentions a single typevar, and we keep that typevar when quantifying, the
|
||||
result is unchanged.
|
||||
|
||||
```py
|
||||
from ty_extensions import ConstraintSet, static_assert
|
||||
|
||||
class Base: ...
|
||||
class Sub(Base): ...
|
||||
|
||||
def keep_single[T]():
|
||||
constraints = ConstraintSet.always()
|
||||
quantified = ConstraintSet.always()
|
||||
static_assert(constraints.retain_one(T) == quantified)
|
||||
|
||||
constraints = ConstraintSet.never()
|
||||
quantified = ConstraintSet.never()
|
||||
static_assert(constraints.retain_one(T) == quantified)
|
||||
|
||||
constraints = ConstraintSet.range(Sub, T, Base)
|
||||
quantified = ConstraintSet.range(Sub, T, Base)
|
||||
static_assert(constraints.retain_one(T) == quantified)
|
||||
```
|
||||
|
||||
## Removing a single typevar
|
||||
|
||||
If a constraint set only mentions a single typevar, and we remove that typevar when quantifying,
|
||||
the result is usually "always". The only exception is if the original constraint set has no
|
||||
solution. In that case, the result is also unsatisfiable.
|
||||
|
||||
```py
|
||||
from ty_extensions import ConstraintSet, static_assert
|
||||
|
||||
class Base: ...
|
||||
class Sub(Base): ...
|
||||
|
||||
def remove_single[T]():
|
||||
constraints = ConstraintSet.always()
|
||||
quantified = ConstraintSet.always()
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
constraints = ConstraintSet.never()
|
||||
quantified = ConstraintSet.never()
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
constraints = ConstraintSet.range(Sub, T, Base)
|
||||
quantified = ConstraintSet.always()
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
```
|
||||
|
||||
This also holds when the constraint set contains multiple typevars. In the cases below, we are
|
||||
keeping `U`, and the constraints on `T` do not ever affect what `U` can specialize to — `U` can
|
||||
specialize to anything (unless the original constraint set is unsatisfiable).
|
||||
|
||||
```py
|
||||
from ty_extensions import ConstraintSet, static_assert
|
||||
|
||||
class Base: ...
|
||||
class Sub(Base): ...
|
||||
|
||||
def remove_other[T, U]():
|
||||
constraints = ConstraintSet.always()
|
||||
quantified = ConstraintSet.always()
|
||||
static_assert(constraints.retain_one(U) == quantified)
|
||||
|
||||
constraints = ConstraintSet.never()
|
||||
quantified = ConstraintSet.never()
|
||||
static_assert(constraints.retain_one(U) == quantified)
|
||||
|
||||
constraints = ConstraintSet.range(Sub, T, Base)
|
||||
quantified = ConstraintSet.always()
|
||||
static_assert(constraints.retain_one(U) == quantified)
|
||||
```
|
||||
|
||||
## Transitivity
|
||||
|
||||
When a constraint set mentions two typevars, and compares them directly, then we can use
|
||||
transitivity to propagate the other constraints when quantifying.
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions import ConstraintSet, static_assert
|
||||
|
||||
class Super: ...
|
||||
class Base(Super): ...
|
||||
class Sub(Base): ...
|
||||
|
||||
def transitivity[T, U]():
|
||||
# (Base ≤ T) ∧ (T ≤ U) → (Base ≤ U)
|
||||
constraints = ConstraintSet.range(Base, T, object) & ConstraintSet.range(T, U, object)
|
||||
quantified = ConstraintSet.range(Base, U, object)
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
# (Base ≤ T ≤ Super) ∧ (T ≤ U) → (Base ≤ U)
|
||||
constraints = ConstraintSet.range(Base, T, Super) & ConstraintSet.range(T, U, object)
|
||||
quantified = ConstraintSet.range(Base, U, object)
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
# (T ≤ Base) ∧ (U ≤ T) → (U ≤ Base)
|
||||
constraints = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, U, T)
|
||||
quantified = ConstraintSet.range(Never, U, Base)
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
# (Sub ≤ T ≤ Base) ∧ (U ≤ T) → (U ≤ Base)
|
||||
constraints = ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Never, U, T)
|
||||
quantified = ConstraintSet.range(Never, U, Base)
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
```
|
||||
|
||||
## Covariant transitivity
|
||||
|
||||
The same applies when one of the typevars is used covariantly in a bound of the other typevar.
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions import ConstraintSet, static_assert
|
||||
|
||||
class Super: ...
|
||||
class Base(Super): ...
|
||||
class Sub(Base): ...
|
||||
|
||||
class Covariant[T]:
|
||||
def get(self) -> T:
|
||||
raise NotImplementedError
|
||||
|
||||
def covariant_transitivity[T, U]():
|
||||
# (Base ≤ T) ∧ (Covariant[T] ≤ U) → (Covariant[Base] ≤ U)
|
||||
constraints = ConstraintSet.range(Base, T, object) & ConstraintSet.range(Covariant[T], U, object)
|
||||
quantified = ConstraintSet.range(Covariant[Base], U, object)
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
# (Base ≤ T ≤ Super) ∧ (Covariant[T] ≤ U) → (Covariant[Base] ≤ U)
|
||||
constraints = ConstraintSet.range(Base, T, Super) & ConstraintSet.range(Covariant[T], U, object)
|
||||
quantified = ConstraintSet.range(Covariant[Base], U, object)
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
# (T ≤ Base) ∧ (U ≤ Covariant[T]) → (U ≤ Covariant[Base])
|
||||
constraints = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, U, Covariant[T])
|
||||
quantified = ConstraintSet.range(Never, U, Covariant[Base])
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
# (Sub ≤ T ≤ Base) ∧ (U ≤ Covariant[T]) → (U ≤ Covariant[Base])
|
||||
constraints = ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Never, U, Covariant[T])
|
||||
quantified = ConstraintSet.range(Never, U, Covariant[Base])
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
```
|
||||
|
||||
## Contravariant transitivity
|
||||
|
||||
Similar rules apply, but in reverse, when one of the typevars is used contravariantly in a bound of
|
||||
the other typevar.
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions import ConstraintSet, static_assert
|
||||
|
||||
class Super: ...
|
||||
class Base(Super): ...
|
||||
class Sub(Base): ...
|
||||
|
||||
class Contravariant[T]:
|
||||
def receive(self, input: T): ...
|
||||
|
||||
def contravariant_transitivity[T, U]():
|
||||
# (Base ≤ T) ∧ (U ≤ Contravariant[T]) → (U ≤ Contravariant[Base])
|
||||
constraints = ConstraintSet.range(Base, T, object) & ConstraintSet.range(Never, U, Contravariant[T])
|
||||
quantified = ConstraintSet.range(Never, U, Contravariant[Base])
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
# (Base ≤ T ≤ Super) ∧ (U ≤ Contravariant[T]) → (U ≤ Contravariant[Base])
|
||||
constraints = ConstraintSet.range(Base, T, Super) & ConstraintSet.range(Never, U, Contravariant[T])
|
||||
quantified = ConstraintSet.range(Never, U, Contravariant[Base])
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
# (T ≤ Base) ∧ (Contravariant[T] ≤ U) → (Contravariant[Base] ≤ U)
|
||||
constraints = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Contravariant[T], U, object)
|
||||
quantified = ConstraintSet.range(Contravariant[Base], U, object)
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
# (Sub ≤ T ≤ Base) ∧ (Contravariant[T] ≤ U) → (Contravariant[Base] ≤ U)
|
||||
constraints = ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Contravariant[T], U, object)
|
||||
quantified = ConstraintSet.range(Contravariant[Base], U, object)
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
```
|
||||
|
||||
## Invariant transitivity involving equality constraints
|
||||
|
||||
Invariant uses of a typevar are more subtle. The simplest case is when there is an _equality_
|
||||
constraint on the invariant typevar. In that case, we know precisely which specialization is
|
||||
required.
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions import ConstraintSet, static_assert
|
||||
|
||||
class Base: ...
|
||||
|
||||
class Invariant[T]:
|
||||
mutable_attribute: T
|
||||
|
||||
def invariant_equality_transitivity[T, U]():
|
||||
# (T = Base) ∧ (U ≤ Invariant[T]) → (U ≤ Invariant[Base])
|
||||
constraints = ConstraintSet.range(Base, T, Base) & ConstraintSet.range(Never, U, Invariant[T])
|
||||
quantified = ConstraintSet.range(Never, U, Invariant[Base])
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
# (T = Base) ∧ (Invariant[T] ≤ U) → (Invariant[Base] ≤ U)
|
||||
constraints = ConstraintSet.range(Base, T, Base) & ConstraintSet.range(Invariant[T], U, object)
|
||||
quantified = ConstraintSet.range(Invariant[Base], U, object)
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
```
|
||||
|
||||
## Invariant transitivity involving range constraints
|
||||
|
||||
When there is a _range_ constraint on the invariant typevar, we still have to retain information
|
||||
about which range of types the quantified-away typevar can specialize to, since this affects which
|
||||
types the remaining typevar can specialize to, and invariant typevars are not monotonic like
|
||||
covariant and contravariant typevars.
|
||||
|
||||
```py
|
||||
from typing import Never
|
||||
from ty_extensions import ConstraintSet, static_assert
|
||||
|
||||
class Base: ...
|
||||
class Sub(Base): ...
|
||||
|
||||
class Invariant[T]:
|
||||
mutable_attribute: T
|
||||
|
||||
def invariant_range_transitivity[T, U]():
|
||||
# (Sub ≤ T ≤ Base) ∧ (U ≤ Invariant[T]) → (U ≤ Invariant[Exists[Sub, Base]])
|
||||
constraints = ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Never, U, Invariant[T])
|
||||
# TODO: The existential that we need doesn't exist yet.
|
||||
quantified = ConstraintSet.never()
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
|
||||
# (Sub ≤ T ≤ Base) ∧ (Invariant[T] ≤ U) → (Invariant[Exists[Sub, Base]] ≤ U)
|
||||
constraints = ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Invariant[T], U, object)
|
||||
# TODO: The existential that we need doesn't exist yet.
|
||||
quantified = ConstraintSet.never()
|
||||
# TODO: no error
|
||||
# error: [static-assert-error]
|
||||
static_assert(constraints.exists(T) == quantified)
|
||||
```
|
||||
Reference in New Issue
Block a user