-
Notifications
You must be signed in to change notification settings - Fork 5
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
overloads and intersections; research and analysis #860
Comments
Technically speaking, this is only valid if you define I think that's unintuitive, and that it makes a lot more sense that |
i disagree with this, if this was the semantics, how could an implementation possibly conform to that overload? @overload
def f(a: int) -> int: ...
@overload
def f(a: str) -> str: ...
@overload
def f(a: str | int) -> complex: ...
def f(a):
if isinstance(a, int):
return 1
if isinstance(a, str):
return ""
def fn(x: int | str):
f(x) # expected: complex, actual: 1
fn(1) additionally, you should receive an error: def f(a: str | int) -> complex: ... # error: overload overlaps |
type ⊤ = object
type ⊥ = Never
type Sets[InT] = Callable[[InT], None]
type Gets[OutT] = Callable[[], OutT]
type Maps[InT, OutT] = Callable[[InT], OutT]
class A: ...
class B: ... %%{
init: {
"themeVariables": {"wrap": "false"},
"flowchart": {
"curve": "linear",
"markdownAutoWrap":"false",
"wrappingWidth": "600"
}
}
}%%
graph BT
N["⊥"]
N --> SO["Sets[⊤]"]
SO --> SAuB["Sets[A | B]"]
SAuB --> SA["Sets[A]"]
SA --> SAnB["Sets[A & B]"]
SAuB --> SB["Sets[B]"]
SB --> SAnB
SAnB --> SN["Sets[⊥]"]
SN --> O["⊤"]
N --> MON["Maps[⊤, ⊥]"]
MON --> MAuBAnB["Maps[A | B, A & B]"]
MAuBAnB --> MAA["Maps[A, A]"]
MAA --> MAnBAuB["Maps[A & B, A | B]"]
MAuBAnB --> MAB["Maps[A, B]"]
MAB --> MAnBAuB
MAuBAnB --> MBA["Maps[B, A]"]
MBA --> MAnBAuB
MAuBAnB --> MBB["Maps[B, B]"]
MBB --> MAnBAuB
MAnBAuB --> MNO["Maps[⊥, ⊤]"]
MNO --> O
N --> GN["Gets[⊥]"]
GN --> GAnB["Gets[A & B]"]
GAnB --> GA["Gets[A]"]
GA --> GAuB["Gets[A | B]"]
GAnB --> GB["Gets[B]"]
GB --> GAuB
GAuB --> GO["Gets[⊤]"]
GO --> O
|
It can't! That's why non-disjoint unions are stupid |
the point
preconditions
all code samples can be assumed to use these definitions:
primer
overloads match by signature order:
overload invocation should distribute unions
when a call can be split into multiple parts via distribution of union,
a valid/more specific return type can be derived:
this is safe and correct because each signature of the overload is valid with all portions of the union
and the implementation should be guaranteed to return each correctly
this isn't unique to overloads though, and also applies to generic functions:
i suppose this is because one way of thinking of generic functions is that they (kind of) represent an overload of every possible type
overload implementations need to follow the semantics of the signature matching
therefore we can deduce that any overload signature matching semantics cannot be invalidated by hypothetical implementations, because they must follow the same rules
shorthand proposal
i propose an
Overload
type that would be equivalent to aProtocol
with the equivalent overloads:the problem
overloaded functions are often referred to as intersections, but this is not true.
overloads are neither supertypes nor subtypes of a corresponding intersection
this is true for many reasons, primarily:
here we demonstrate that
Overload[FInt, FStr]
is not a subtype ofFInt & FStr
additionally, if intersections of callables were considered as overloads:
if this were the case, then intersections could not be commutative. this is so absurd that it won't be considered
within this document i will examine these two ideas:
option 1: overloads aren't the same as intersections
callable intersection return type
intersections of callables should follow normal intersection rules and return intersections:
regarding synthesis of overloads from an intersection:
Option 2: overload semantics that don't depend on order
given this scenario:
if we were to apply some hypothetical non-ordered matching semantics,
then regarding implementations of
f
, we could say:considering this invocation:
traditional overload semantics would suggest that the return type would be
A
,but if we apply these non-ordered semantics, then the call with match both overloads and return
A & B
regarding synthesis of overloads from an intersection:
The text was updated successfully, but these errors were encountered: