Clarify the rules for sparam matching
types and dispatch
This is possibly a duplicate of #52992, but I wanted to give a clean presentation to avoid some confounders:
Consider these methods:
```
f1(t::Type{E}) where E = @isdefined(E)
f2(t::Type{T}) where {E, T<:E} = @isdefined(E)
f3(t::Type{T}) where {E, E<:T<:E} = @isdefined(E)
```
What is the rule for when `@isdefined(E)`?
The currently observed behavior is `true` for all three if `t` is a concrete type and `true` for f1 only in all other cases.
I don't think this is particularly coherent rule. In particular, I find it hard to come up with a clear rule that should
treat f1 and f3 differently.
There are a few candidate rules that have been proposed, none of which match the current behavior:
1. `E` should be defined if there is a unique value of `E` for which the signature matches
This would imply that f1 and f3 should be true in all cases and f2 should be false for everything except `Any`. However, this is clearly not a good rule by itself, because `f(x::T) where T = x` should always be `typeof(x)`
2. `E` should be some least upper bound over its range
I think this is closer to what we do, but it doesn't give a clear answer to the question of definedness. It is tempting to define definedness as the existence of a unique (up to type equality) infimum, but that's not really what we do. E.g. when we match nothing again `::Union{T, Nothing}`, `T` is undefined, not `Union{}`. Possibly, we could semantically extend the lattice for this purpose to have an `Undefined` element below bottom. This would imply that `f1`, `f2` and `f3` are all `true`.
However, even that is not quite as simple, because there is some structural aspect to this. Ideally, we would like to define sparam extraction at least partially structurally, but what if the same sparam matches twice with different structural identities:
```
julia> f(::Type{E}, ::Type{E}) where E = E
f (generic function with 1 method)
julia> f(Int, Union{T, S} where {T<:Int, S<:Int})
Union{T, S} where {T<:Int64, S<:Int64}
julia> f(Int, Int)
Union{T, S} where {T<:Int64, S<:Int64}
```
The caching part here is partly a separate issue (I'm just including it here to show that because of the caching and because we don't have a clear answer on how the sparam extraction is computed, random type-equal values could be synthesized out of fresh air).
I don't know that I have a full answer to this, but I wanted to have a place to write this up coherently and also have a place to discuss possible tweaks and experiments.
0 条评论