Skip to content

RFC: Widen less aggressively in tmerge #23077

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.

Sign up for GitHub

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

Closed
wants to merge 2 commits into from
Closed

RFC: Widen less aggressively in tmerge #23077

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cfd039b
Widen unions less agressively during inference
martinholters Jul 24, 2017
7a26e18
Remove special treatment of Tuples from tmerge
martinholters Jul 27, 2017
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
20 changes: 6 additions & 14 deletions base/inference.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2798,21 +2798,13 @@ function tmerge(@nospecialize(typea), @nospecialize(typeb))
if !(isa(typea,Type) || isa(typea,TypeVar)) || !(isa(typeb,Type) || isa(typeb,TypeVar))
return Any
end
if (typea <: Tuple) && (typeb <: Tuple)
if isa(typea, DataType) && isa(typeb, DataType) && length(typea.parameters) == length(typeb.parameters) && !isvatuple(typea) && !isvatuple(typeb)
return typejoin(typea, typeb)
end
if isa(typea, Union) || isa(typeb, Union) || (isa(typea,DataType) && length(typea.parameters)>3) ||
(isa(typeb,DataType) && length(typeb.parameters)>3)
# widen tuples faster (see #6704), but not too much, to make sure we can infer
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I assume removing this doesn't reintroduce #6704? (it's partially handled by #21933 now, but I also don't handle Tuple correctly there – don't widen it fast enough – partially due to assuming that this code here existed)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I assume removing this doesn't reintroduce #6704?

It doesn't, at least not the code as posted there. I didn't try to find variations that might still cause problems, though.

(it's partially handled by #21933 now, but I also don't handle Tuple correctly there – don't widen it fast enough – partially due to assuming that this code here existed)

Ah, I wasn't aware of that.

# e.g. (t::Union{Tuple{Bool},Tuple{Bool,Int}})[1]
return Tuple
end
end
u = Union{typea, typeb}
if unionlen(u) > MAX_TYPEUNION_LEN || type_too_complex(u, MAX_TYPE_DEPTH)
# don't let type unions get too big
# TODO: something smarter, like a common supertype
if unionlen(u) > MAX_TYPEUNION_LEN
u = typejoin(typea, typeb)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

perhaps do u = typejoin(u.a, u.b) – it might as well get some benefit out of already having computed the union of a and b

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To make this case convergent however, I think typejoin would need to be reordered to handle Union first (even before checking subtyping). Thus, it might be better to do foldl(typejoin, Union{}, uniontypes(u)).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure I completely understand the problem... if typea <: typeb or vice verse, we don't get here. Now if say typea is a Union, surely neither type.a <: typea.b nor vice verse, so in the recursive call of typejoin, the subtype test should always be false. Likewise for typeb, of course. But admittedly, if say typea is a TypeVar and typeb is a Union, things get a little trickier to reason about. So no matter whether it's actually necessary, your proposed version is much easier to reason about :)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Monotonicity here seems like it may depend on typejoin being associative, such that typejoin(A, typejoin(B, C)) == typejoin(typejoin(A, B), C), but I'm not sure that's true. And my version may actually be worse at assuming that. I think we may want typejoin(remove_unions(typea), remove_unions(typeb)), which is what your version does.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm, then typea <: typea′ would need to imply remove_unions(typea) <: remove_unions(typea′) (monotonicity) and I had simply assumed remove_unions(u::Union) = typejoin(u.a, u.b) to fulfill that... but it's not that obvious...

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we can see from the implementation that at least remove_unions(u::Union) is typejoin(u.a, u.b); the case that I'm not sure about is where one of the types isn't a union (remove_unions(x::ANY) = x).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Making typejoin associative would be another option – I think any failure of associativity would be pretty awful. Not sure how to go about assuring that, but it climbs up the type lattice and lattice operations are, by definition, associative, so hopefully that can help.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Correct me if I'm wrong, but ensuring convergence requires monotonicity in the sense that a <: a´ && b <: b´ implies tmerge(a, b) <: tmerge(a´, b´), right? Then indeed we cannot let typejoin do the core work because of e.g. this:

julia> a´ = a = Ref{Int}
Ref{Int64}

julia> b = Ref{UInt}
Ref{UInt64}

julia> b´ = Ref{<:Integer}
Ref{#s1} where #s1<:Integer

julia> typejoin(a, b)
Ref

julia> typejoin(a, b´)
Ref{#s1} where #s1<:Integer

julia> a <: a´ && b <: b´
true

julia> typejoin(a, b) <: typejoin(a, b´)
false

But turns out we're already using typejoin in tmerge for (certain) tuples. And indeed (on master and 0.6):

julia> a´ = a = Tuple{Int32, Ref{Int}}
Tuple{Int32,Ref{Int64}}

julia> b = Tuple{Int64, Ref{UInt}}
Tuple{Int64,Ref{UInt64}}

julia> b´ = Tuple{Int64, Ref{<:Integer}}
Tuple{Int64,Ref{#s30} where #s30<:Integer}

julia> Core.Inference.tmerge(a, b)
Tuple{Signed,Ref}

julia> Core.Inference.tmerge(a, b´)
Tuple{Signed,Ref{#s30} where #s30<:Integer}

julia> a <: a´ && b <: b´
true

julia> Core.Inference.tmerge(a, b) <: Core.Inference.tmerge(a, b´)
false

Unless someone tells me I'm off track here and this is not an issue, my idea would be to first rethink typejoin and depending on the outcome either go ahead with this PR or move in the other direction and completely remove typejoin from tmerge.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, that cannot be the right interpretation of "monotonicity" in this context, there are too many cases where tmerge violates that. Is it sufficient that the sequence of xs obtained by repeatedly doing x = tmerge(x, ...) is monotonic? Then obviously x >: tmerge(x, ...) suffices, but also using typejoin should be kosher then. @vtjnash, you brought up monotonicity, could you clarify what you meant and what potential problems with typejoin you fear exactly?

end
if type_too_complex(u, MAX_TYPE_DEPTH)
# helps convergence speed (large types that are changing value become very slow to
# work with very quickly)
return Any
end
return u
Expand Down
5 changes: 5 additions & 0 deletions test/inference.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1291,3 +1291,8 @@ let T1 = Array{Float64}, T2 = Array{_1,2} where _1
rt = Base.return_types(g, (Union{Ref{Array{Float64}}, Ref{Array{Float32}}},))[1]
@test rt >: Union{Type{Array{Float64}}, Type{Array{Float32}}}
end

f_23077(x) = (Int8(0), Int16(0), Int32(0), Int64(0))[x]
@test Base.return_types(f_23077, Tuple{Int})[1] <: Signed
g_23077(x,y,z) = x ? y ? z ? (1,) : (1,1.0) : (1,1) : (1,1.0,1)
@test Base.return_types(g_23077, Tuple{Bool,Bool,Bool})[1] <: Tuple{Int,Vararg{Real}}