Skip to content
Closed
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
Original file line number Diff line number Diff line change
Expand Up @@ -481,22 +481,99 @@ reveal_type(g(f("a"))) # revealed: tuple[Literal["a"], int] | None

## Passing generic functions to generic functions

```py
`functions.pyi`:

```pyi
from typing import Callable

def invoke[A, B](fn: Callable[[A], B], value: A) -> B:
return fn(value)
def invoke[A, B](fn: Callable[[A], B], value: A) -> B: ...

def identity[T](x: T) -> T:
return x
def identity[T](x: T) -> T: ...

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

def head[T](xs: list[T]) -> T:
return xs[0]
def head_covariant[T](xs: Covariant[T]) -> T: ...
def lift_covariant[T](xs: T) -> Covariant[T]: ...

class Contravariant[T]:
def receive(self, input: T): ...

def head_contravariant[T](xs: Contravariant[T]) -> T: ...
def lift_contravariant[T](xs: T) -> Contravariant[T]: ...

class Invariant[T]:
mutable_attribute: T

def head_invariant[T](xs: Invariant[T]) -> T: ...
def lift_invariant[T](xs: T) -> Invariant[T]: ...
```

A simple function that passes through its parameter type unchanged:

`simple.py`:

```py
from functions import invoke, identity

reveal_type(invoke(identity, 1)) # revealed: Literal[1]
```

When the either the parameter or the return type is a generic alias referring to the typevar, we
should still be able to propagate the specializations through. This should work regardless of the
typevar's variance in the generic alias.

TODO: This currently only works for the `lift` functions (TODO: and only currently for the covariant
case). For the `lift` functions, the parameter type is a bare typevar, resulting in us inferring a
type mapping of `A = int, B = Class[A]`. When specializing, we can substitute the mapping of `A`
into the mapping of `B`, giving the correct return type.

For the `head` functions, the parameter type is a generic alias, resulting in us inferring a type
mapping of `A = Class[int], A = Class[B]`. At this point, the old solver is not able to unify the
two mappings for `A`, and we have no mapping for `B`. As a result, we infer `Unknown` for the return
type.

As part of migrating to the new solver, we will generate a single constraint set combining all of
the facts that we learn while checking the arguments. And the constraint set implementation should
be able to unify the two assignments to `A`.

# TODO: this should be `Unknown | int`
reveal_type(invoke(head, [1, 2, 3])) # revealed: Unknown
`covariant.py`:

```py
from functions import invoke, Covariant, head_covariant, lift_covariant

# TODO: revealed: `int`
# revealed: Unknown
reveal_type(invoke(head_covariant, Covariant[int]()))
# revealed: Covariant[Literal[1]]
reveal_type(invoke(lift_covariant, 1))
```

`contravariant.py`:

```py
from functions import invoke, Contravariant, head_contravariant, lift_contravariant

# TODO: revealed: `int`
# revealed: Unknown
reveal_type(invoke(head_contravariant, Contravariant[int]()))
# TODO: revealed: Contravariant[int]
# revealed: Unknown
reveal_type(invoke(lift_contravariant, 1))
```

`invariant.py`:

```py
from functions import invoke, Invariant, head_invariant, lift_invariant

# TODO: revealed: `int`
# revealed: Unknown
reveal_type(invoke(head_invariant, Invariant[int]()))
# TODO: revealed: `Invariant[int]`
# revealed: Unknown
reveal_type(invoke(lift_invariant, 1))
```

## Protocols as TypeVar bounds
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -416,19 +416,43 @@ 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])
# revealed: ty_extensions.Specialization[T@mentions_covariant = int, U@mentions_covariant = Covariant[int]]
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
Expand All @@ -437,8 +461,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))
```
Loading
Loading