Subtype: Improve simple_meet resolution for Union inputs
#49376
Conversation
|
To be backported to 1.9? |
src/jltypes.c
Outdated
| } | ||
| if (subab && !subba) { | ||
| stemp[j] = -1; | ||
| temp[j] = temp[i]; |
There was a problem hiding this comment.
Does this make the algorithm slightly unstable to ordering? Eventually, for !overesi, this algorithm could return Union{a, b} for all a and b from the original a and b for which it could prove that element is a <: of the other union. That may often be Union{}, but doesn't have to be.
Secondly for overesi, it similarly can return any type that is both <:a and <:b but >:intersect(a,b). I don't think that is quite the same as removing any element from b that is potentially a subtype of an element a. For example, if it had Tuple{E1} and Tuple{E2} in a, but had Tuple{Union{E1,E2}} in b, it may be incorrect to "forget" that Tuple{E2} was in the union (unless !overesi)
There was a problem hiding this comment.
I'm afraid that I didn’t get the 1st concern, simple_intersectonly joins preserved types in a, or preserved and substituted ones inb, thus it seems unlikely to return Union{a,b}?
But the 2nd concern is correct, the current algorithm works well only for injective elements. We’d better perform the “substitution” after the subtyping
There was a problem hiding this comment.
For !overesi, it isn't a concern, but an observation that this can return the Union of all provably preservable elements (all elements of a that are definite subtypes of b and all elements of b that are definitely subtypes of a)
There was a problem hiding this comment.
IIUC, this is exactly what we want?
The result should >: all elements from a if it <:b and all elements from b if it <:a.
I think there's no need to worry about Union{Int, Real} ∩ Integer (a[i] <: b[j] <: a[k]) as all other path should have normalized it.
There was a problem hiding this comment.
It may already be doing much of this, and I just haven't fully understood that part of the algorithm. The example I am thinking here is that if you had a=Union{Int32, Int64, AbstractString} and b=Union{Integer, String}, then the !overesi intersection can be any type that is <:Union{Int32, Int64, String} (often chosen as Union{} currently) while the overesi intersection is any value that is >:Union{Int32, Int64, String}, which might be chosen as either of a or b currently.
There was a problem hiding this comment.
For !overesi, the algorithm requires all undisjointable part in a(b) <: b(a), otherwise it would always return Union{}.
Since the "Subtitution" has been replaced with an elimination with partiality, elements in a would be removed if we can't prove it <:ₛb, while elements in b would be removed only if we can prove it >:ₛa. (ₛ means strick)
N5N3
force-pushed
the
subtype-tuning
branch
2 times, most recently
from
8156ee8
to
249e819
Compare
ans make sure the duplicated elements in `a` get removed
N5N3
force-pushed
the
subtype-tuning
branch
2 times, most recently
from
249e819
to
c9d1ab2
Compare
This should be fast, as it has an `obviously_disjoint`-based fast path.
* Improve `simple_meet` resolution. * Fix for many-to-one cases. * Test disjoint via `jl_has_empty_intersection`
|
Thanks @N5N3! |
|
@N5N3, this seems to fail |
|
Sorry, didn’t notice that. Looks like there’re some GC mark change on master. |
…ng#49376) * Improve `simple_meet` resolution. * Fix for many-to-one cases. * Test disjoint via `jl_has_empty_intersection`
close #49354. (The fix is somehow limited as
obviously_disjointis simple to deceive.)