Method ambiguity involving diagonal types

General Usage
, ,
1

MWE:

julia> f1(argL::T, argR::T) where {T} = 1
f1 (generic function with 1 method)

julia> f1(argL::T1, argR::T2) where {T, T1<:AbstractArray{T}, T2<:AbstractArray{T}} = 2
f1 (generic function with 2 methods)

julia> f1([1], [1])
2

Shouldn’t f1([1], [1]) throw a MethodError since neither method is more specific than the other (i.e., the set of argument types of one method is a proper subset of another) when the input argument types are (::T, ::T) where T==Vector{Int}?

I would imagine that one needs to implement the following method to avoid the ambiguity:

f1(argL::T, argR::T) where {T<:AbstractArray} = 3
1 Like
2

The implementation thinks otherwise. I think Julia just weighs the T<:Any before whether arguments share a type via a static parameter.

julia> methods(f1)
# 2 methods for generic function "f1" from Main:
 [1] f1(argL::T1, argR::T2) where {T, T1<:(AbstractArray{T}), T2<:(AbstractArray{T})}
     @ REPL[2]:1
 [2] f1(argL::T, argR::T) where T
     @ REPL[1]:1

julia> Base.morespecific(methods(f1)...)
true

julia> invoke(f1, Tuple{T, T} where T, [1], [1]) # checking the other method works
1

It flips if you restricted T<:AbstractArray, of course.

julia> methods(f2)
# 2 methods for generic function "f2" from Main:
 [1] f2(argL::T, argR::T) where T<:AbstractArray
     @ REPL[8]:1
 [2] f2(argL::T1, argR::T2) where {T, T1<:(AbstractArray{T}), T2<:(AbstractArray{T})}
     @ REPL[9]:1

julia> Base.morespecific(methods(f2)...)
true
2 Likes
3

Thanks for mentioning Base.morespecific! Unfortunately, it seems to be a non-public function (as of 1.12). If I try to use it in 1.11, I will even get the following error:

julia> Base.morespecific(methods(f1)...)
ERROR: TypeError: in typeassert, expected Type, got a value of type Method

So, I’m not sure if there’s a proper way to determine whether a method is more specific than another.

Ironically, I thought the mental model for determining method ambiguity was well established by the language, but upon checking the official documentation, I found only an example without a formally defined criterion for what is deemed a “unique most specific method.” There are some practical suggestions on method design to avoid ambiguities, but still no formal definition of a “method ambiguity”. I can only imagine how beginners in Julia can feel confused or develop their own “understanding” regarding method ambiguity.

Since there is no formal definition, I shall share my understanding of what method ambiguity is. Please point out any “misconception” you think I might have.

For each method corresponding to the same function name (inspected by nameof, or its type if it is acutally a callable object of Function), a set of all possible combinations of argument types (in the form of a Tuple of Type) that are covariantly subtyping the argument types specified by that method forms a “method specificity set”. For example, for method f1(argL::T, argR::T) where {T}, its “method specificity set” is

M = {(T, T) | T }

where T iterates through all the possible concrete types.

When a function is called, a tuple of argument types argType is formed. For example, for foo(a::T1, b::T2), argType = (T1, T2). When argType belongs to more than one method specificity set:

MS = {M_i | M_i is a valid “method specificity set”} and |MS| > 1

but MS cannot form a strict chain of inclusion (i.e., M_i ⊊ M_j ⊊ …).

This is my mental model of how “method ambiguity” is defined, which is also consistent with the example in the official documentation, where the term “intersection” is used to indicate the “cause” of “method ambiguity”:

You can avoid method ambiguities by specifying an appropriate method for the intersection case

However, if that is the case, the example I showed in OP directly violates this criterion, as the method specificity set of one method is not a proper subset of another. Therefore, I think in principle, f1([1], [1]) should have thrown a MethodError.

4

It used to require a more public type-tuple method (as opposed to call) signature:

julia> Base.morespecific(Tuple{typeof(f1), AbstractArray, AbstractArray}, Tuple{typeof(f1), T, T} where T)
true

though it’s obviously simpler to reference an internal Method directly.

AFAIK there’s no public reflection API for Methods other than simply viewing them with methods. morespecific is just a relatively convenient internal function, I’d have to dig deeper for something more direct and reliable.

I haven’t seen a full specification either, there’s a More About Types page in the devdocs but that doesn’t describe a straightforward dispatch algorithm either.

It seems like you’re trying to formalize set theory-based rules based on the documentation’s examples, but while reasonable for a tuple of unrelated types, they evidently fell apart at diagonal types that restrict the method specificity set in a different way from independent abstract type annotations. It’s not feasible to infer rules from runtime to begin with, you’ll need to communicate with the developer community. Hopefully some can jump in this thread, I’ll try to move this up in the feed.

1 Like
5

Yeah, the diagonal rule of UnionAll types definitely complicates the detection for method ambiguity. Thanks for the explanation and the help!

I don’t mean to completely disregard the current solutions for the dispatch system, but I do hope there is a clearer explanation and guidelines from the core language developer team. This will be more helpful to downstream developers and future users.

6

I also think it’s strange, that the most important concept of the language is not specified in the official documentation. In the absence of an official specification, I hope the explanations from Jameson Nash do help you.

2 Likes
7

Hmm, that’s an interesting example. With the method signatures A and B, we have

julia> A = Tuple{T1,T2} where {T, T1<:AbstractArray{T}, T2<:AbstractArray{T}}
Tuple{T1, T2} where {T, T1<:(AbstractArray{T}), T2<:(AbstractArray{T})}

julia> B = Tuple{T,T} where T
Tuple{T, T} where T

julia> A <: B
false

julia> B <: A
false

julia> typeintersect(A,B)
Tuple{T1, T1} where {T, T1<:(AbstractArray{T})}

julia> Base.morespecific(A, B)
true

My idea of A more specific than B is that typeintersect(A, B) == A, or A <: B && !(B <: A), but this is not true in this example. It seems the definitive definition is inside subtype.c in the julia source, and not anywhere else. And the subtype comparision is just part of it, the called type_morespecific_ is a bit involved:

1 Like
8

My understanding is the following:

  1. If only one method matches (in the isa sense), then this method is unambiguously chosen
  2. If there are multiple matching methods, and one of them is most specific, in the sense of the partial issubtype order, then this is chosen
  3. If there is no most specific method, then we have a kind of ambiguity: The set of isa-matching (ie applicable) methods have multiple incomparable issubtype elements.
  4. The julia runtime then may choose to throw a MethodAmbiguity error.
  5. Alternatively, the julia runtime may choose one of the minimal applicable methods, according to weird undocumented heuristics that happened to produce “intuitive” results in the past (aka: read the C code, may change in every minor version)

The set-theoretic interpretation of “a UnionAll type is the set of all instantiations” is not the real type system; instead the type system is designed to give that impression and to allow many intuitions from the set-theoretical (“extensional”) interpretation to be true; but the system is actually intensional. Unfortunately it is complex and hard to reason about. Also, subtyping is undecidable.

If one doesn’t go fancy with types, then the type system works pretty well and intuitively. If you do get fancy with types, then you will encounter bugs, surprising corner cases, and hangs/endless loops (due to the undecidability).

This situation is not ideal. But afaiu nobody knows whether a sound + decideable + intuitive type system that has all features that people want is even possible. (I think we could get better by ruthlessly cutting features – abstract types are not meant for correctness, they are only meant for dispatch)

1 Like
9

But how do we determine if one method is more “specific” than the other without following the set-theoretic interpretation? The official documentation for types has already heavily adopted the set-theory terms like “union”, “set”, and “subset” to describe the relation between types.

Moreover, regardless of whether the type system should operate strictly under the convention of set theory, the central problem IMO is that the way the criterion for subtyping computation is not even consistent with the determination of method specificity. This is precisely captured by the example provided by @sgaure:

Since Base.morespecific is not public, the user should not use it to determine which method is more specific. Yet, the subtype computation, which currently seems to be the only quantitative way to do type analysis within Julia, also does not provide a helpful indication in this regard. This is counterproductive, if not dangerous, as users may (and often do) base their understanding of method ambiguities on the hierarchy of types using set-theory notions.

I sincerely hope that any core developers involved in the type and dispatch systems of Julia can see this thread and provide an official/concrete guideline on resolving this issue. I don’t want to be rude by mistakenly pinning the wrong people, so I’m also happy to open an issue on GitHub if one isn’t already open.

1 Like
10

That is a typical issue when coming at it from the mathematics side, that took me embarrassingly long to figure out. Best way for me to state it:

issubtype(A,B) is implies that x isa A implies x isa B for all x. But the converse is not true: Take A=Int and B=Union{Int, Tuple{1}}; you will be hard pressed to instantiate an x with typeof(x) === Tuple{1}.

An analogy for mathematicians would be: Typing does not talk about what things are true; it talks about what things are provable by a specific bunch of very julia-specific logic / axioms. There is no nice law of excluded middle.

Saying A is a subtype of B is not analogous to “{x: x isa A}” is a subset of “{x: x isa B}”; it is analogous to saying that the julia type system rules prove that this is a subset. There is a wide conceptional and practical gulf between them! Not all that is true can be proven, cf goedel.

That is what I alluded to with “extensional / set-theoretic” vs “intensional / type-theoretic” viewpoint.

The entire type-theoretic terminology is pretty annoying for set-theoretically schooled people (i.e. it seems needlessly obscure). But that’s to some extent a me-problem, not a type-theory problem.

2 Likes
11

But it is intuitive in a sense. Specificity is, as @foobar_lv2 notes, not part of the extensional view of types. It’s merely a convenience for dispatch when an actual argument list is in the intersection of method signatures which aren’t related as subtypes. In the example I gave, which is just a rewrite of your dispatch mystery, there is some sense. If the argument is in the intersection, like ([1], [1]), the A type has more restrictive bounds on its type variables than B, whose type variable is only bounded by Any. It’s not unreasonable to interpret this as A being more specific than B, conditional on the actual type being in the intersection.