Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

union distrubution of calls doesn't apply to constraints #831

Open
KotlinIsland opened this issue Dec 1, 2024 · 7 comments
Open

union distrubution of calls doesn't apply to constraints #831

KotlinIsland opened this issue Dec 1, 2024 · 7 comments

Comments

@KotlinIsland
Copy link
Owner

KotlinIsland commented Dec 1, 2024

from typing import overload

@overload
def f1(a: int) -> list[int]: ...

@overload
def f1(a: str) -> list[str]: ...

def f1(a):
    return [a]


def f2[T: (int, str)](a: T) -> list[T]:
    return [a]
    
    
data: int | str
reveal_type(f1(data))  # Revealed type is "Union[builtins.list[builtins.int], builtins.list[builtins.str]]"
reveal_type(f2(data))  # Value of type variable "T" of "f2" cannot be "int | str"  [type-var]
@jorenham
Copy link
Collaborator

jorenham commented Dec 1, 2024

int | str is equivalent to (int ^ str) - (int & str) (where ^ denotes the exclusive/disjoint union, and - has the same meaning as it has for a set).

So on other words, int | str must be either:

  • int
  • str
  • int & str

But in you example you only cover the first two cases -- the int & str is ignored.

This means that int | str isn't assignable to a: T in f2 here.

(many of these issues around "typevars with constraints" can be solved with a disjoint union, i.e. str ^ int)

@KotlinIsland
Copy link
Owner Author

KotlinIsland commented Dec 1, 2024

So on other words, int | str must be either:

  • int
  • str
  • int & str

and

  • int | str
  • any concrete subclass/subtype of int & str
  • Never
    and probs other stuff, but that's just pedantics 🙂

But in you example you only cover the first two cases -- the int & str is ignored.

This means that int | str isn't assignable to a: T in f2 here.

int | str isn't assignable to a, it is an invalid value for T. T can only be int or str

for the case of intersections, it will just match the first (for overloads) or closest (for constraints) and not distribute:

class A: ...
class B: ...
class AB(A, B): ...

def f1(x: A) -> list[A]: ...
def f1(x: B) -> list[B]: ...
def f1(x): return [x]

def f2[T: (A, B)](x: T) -> list[T]: return [x]

a_and_b: A & B
f1(a_and_b)  # list[A] match first overload
f2(a_and_b)  # list[A] T=A

ab: AB
f1(ab)  # list[A] match first overload
f2(ab)  # list[A] T=A

can you break these semantics and cause a runtime type error?

@jorenham
Copy link
Collaborator

jorenham commented Dec 2, 2024

Ok ok I understand what you're saying, and I probably wasn't explaining it well enough.

So the main assumption I'm making with all this, is that a T: (A1, A2, ..., An) (n contraints) that's bound to a function, can equivalently be written as n overloads.
And that's why I've been calling it syntactic sugar and also a *bidirectional type-mapping.

So in the case of f2[T: (A, B)](x: T) -> list[T], we can desugar it as

@overload
def f2(x: A) -> list[A]: ...
@overload
def f2(x: B) -> list[B]: ...

So if we try to pass A | B to f2, it'll be rejected. Because A | B isn't assignable to A, and also isn't assignable to B.

...

So I checked this, and apparently I don't understand overloads:

image

the same stuff happens with your list[A] | list[B] example 🤔

So where did the str & bytes (or A & B)part of the union go? I really don't get why this should be valid. Because otherwise, it'll be impossible to include an overload forstr | bytesthat returns e.g.Literal["something else"]`, even though the first two overloads are narrower.

Any idea what I'm missing here?

@jorenham
Copy link
Collaborator

jorenham commented Dec 2, 2024

image

This really isn't making any sense so me...

@KotlinIsland
Copy link
Owner Author

KotlinIsland commented Dec 2, 2024

mypys logic is:

  1. try to match an overload from top to bottom
  2. if no match, then match each entry from the union and create separate calls for each entry
    f2(y) == (f2[str](y) | f2[bytes](y))
  3. combine all separate calls into a union return type
    PathLike[str] | Pathlike[bytes]

mypy calls this 'union math', i call it 'union distribution'

@KotlinIsland
Copy link
Owner Author

KotlinIsland commented Dec 2, 2024

And that's why I've been calling it syntactic sugar

annoyingly, constraints behave slightly differently to overloads, in that the constraints themselves have different ordering rules to overloads:

@overload
def f1(x: int | str) -> int | str: ...

@overload
def f1(x: int) -> int: ...

def f2[T: (int | str, int)](t: T) -> T: ...

data: int
f1(data)  # int | str
f2(data)  # int

@jorenham
Copy link
Collaborator

jorenham commented Dec 2, 2024

And that's why I've been calling it syntactic sugar

annoyingly, constraints behave slightly differently to overloads, in that the constraints themselves have different ordering rules to overloads:

@overload
def f1(x: int | str) -> int | str: ...

@overload
def f1(x: int) -> int: ...

def f2[T: (int | str, int)](t: T) -> T: ...

data: int
f1(data)  # int | str
f2(data)  # int

I guess that fits in my "framework" if you first do a topological-ish sorting (order by specificity) of the of the constraints before converting them

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants