[FR] provide a predicate to check whether a type intersection subtypes some type?

Internals & Design
,
1

Just found out that typeintersect isn’t commutative, i.e., typeintersect(A, B) == typeintersect(B, A) isn’t guaranteed for general A and B: suboptimal typeintersections for degenerate TypeVars · Issue #53069 · JuliaLang/julia · GitHub

Often when typeintersect is used, it’s used to check whether the intersection of two types subtypes a third type. The naive implementation is:

typeintersect(A, B) <: C

The following is, however, more accurate, given that the left and right intersection may err in different directions:

(typeintersect(A, B) <: C) || (typeintersect(B, A) <: C)

Should Julia provide this functionality? I think so, because the latter code is nonobvious, and I think people tend to inadvertently use the less accurate version. I guess this could alternatively go into a package, but I don’t think many people would find and use that package.

EDIT: the premise of this post was that one may want to check whether the intersection of two types subtypes a third type. After more examination, it seems that this (necessarily only approximate in general) construct is rarely used. And when it is used, the third type is usually the bottom type, in which case just typeintersect(A, B) <: Union{} seems to be as good as the two-sided version.

4 Likes
2

I don’t really understand what typeintersect is for. Types aren’t sets so I don’t expect all properties to carry over from set theory (for example we can’t subtype Int with a type for only even instances), but the docs just reads weird to me. It does subtly imply non-commutativity by saying the intersection “usually will be the smallest such type or one close to it.” But isn’t the maximum intersection desired? Wouldn’t the smallest type just be Union{}? And what is the point of a type intersection that isn’t a subtype of both inputs, taking your first example:

julia> both_intersections(A, B) = typeintersect(A, B), typeintersect(B, A)
both_intersections (generic function with 1 method)

julia> s, t = both_intersections(Tuple{T, T} where T, Tuple{X, X, Vararg{Any}} where Int<:X<:Real)
(Tuple{T, T} where T<:Real, Tuple{X, X} where Int64<:X<:Real)

julia> [s t] .<: [Tuple{T, T} where T, Tuple{X, X, Vararg{Any}} where Int<:X<:Real]
2×2 BitMatrix:
 1  1
 0  1

julia> s <: Tuple{X, X, Vararg{Any}} where Int<:X<:Real
false

julia> (1.0, 2.0) isa s
true

julia> (1.0, 2.0) isa Tuple{X, X, Vararg{Any}} where Int<:X<:Real
false
3

it has to be the smallest type that the true intersection is a subtype of.

2 Likes
4

Okay the docstring is more coherent now. I might as well paste and clarify my misunderstanding here, it’s so short:

Compute a type that contains the intersection of T and S. Usually this will be the smallest such type or one close to it.

So there is a strict meaning for a type intersection being a largest subtype of both types, mirroring intersections of sets, but typeintersect only computes a supertype of a type intersection. I was confused because “smallest such” supertype is trivially an intersection so I thought it meant “smallest such” subtype of both inputs. That is, I assume the smallest such supertype is synonymous with intersection, maybe this isn’t true for types like it is with sets.

Going by that assumption, a supertype unequal to and thus larger than an intersection will fail to subtype both input types (s in previous comment’s example), while a supertype equal to an intersection would subtype both inputs (t). Taking typeintersect at its word, we can check typeintersect both ways and hope one of them reached an intersection. I’ve been careful not to say “the intersection” because I recall different (!==) types can be equal (==).

2 Likes
5

I would think that the places where typeintersect is non commutative are likely cases in which both orders are inexact. I would be interested if there are counter-examples to this though.

2 Likes
6

Like this:

#= Assumes typeintersect always returns a supertype of a strict
intersection, which is a largest type that subtypes both inputs.
Does not return an under- or over-estimated type. =#
function trystricttypeintersect(@nospecialize(A), @nospecialize(B))
  if begin AnB = typeintersect(A, B)
           AnB <: A && AnB <: B  end
    return AnB
  elseif begin BnA = typeintersect(B, A)
               BnA <: A && BnA <: B  end
    return BnA
  else # issue #36951 has examples that don't reach strict intersection
    return nothing
  end
end

My question is, how did they verify that typeintersect always computes a supertype of a strict intersection if there wasn’t a way to directly compute a strict intersection?

7

Your hypothesis is that (typeintersect(A, B) <: C) || (typeintersect(B, A) <: C) will never be more accurate than typeintersect(A, B) <: C, right? Here are some examples where the former does turn out to be more accurate:

julia> function test_property(a, b, c)
         ab = typeintersect(a, b)::Type
         ba = typeintersect(b, a)::Type
         x = (ab <: c)::Bool
         y = (ba <: c)::Bool
         accuracy_improvement = (x != y)::Bool
         accuracy_improvement
       end
test_property (generic function with 1 method)

julia> test_property(t) = test_property(t...)
test_property (generic function with 2 methods)

julia> examples = NTuple{3, Type}[
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X, Vararg{X}} where X<:Real, Tuple{X, X, Vararg{X}} where X),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X, Vararg{X}} where X<:Real, Tuple{X, X, Vararg{X}} where X<:Real),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X, Tuple{Vararg{X}} where X>:Int),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X, Tuple{X, Vararg{X}} where X>:Int),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X, Tuple{X, X, Vararg{Any}} where X>:Int),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X, Tuple{X, X, Vararg{Real}} where X>:Int),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X, Tuple{X, X, Vararg{X}} where X>:Int),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X, Tuple{X, X} where X>:Int),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{Vararg{X}} where Int<:X<:Real),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{Vararg{X}} where X>:Int),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{X, Vararg{X}} where Int<:X<:Real),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{X, Vararg{X}} where X>:Int),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{X, X, Vararg{Any}} where Int<:X<:Real),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{X, X, Vararg{Any}} where X>:Int),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{X, X, Vararg{Real}} where Int<:X<:Real),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{X, X, Vararg{Real}} where X>:Int),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{X, X, Vararg{X}} where Int<:X<:Real),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{X, X, Vararg{X}} where X>:Int),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{X, X} where Int<:X<:Real),
         (Tuple{X, X, Vararg{Any}} where X>:Int, Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int),
         (Tuple{X, X, Vararg{Real}} where Int<:X<:Real, Tuple{Any, Vararg{X}} where X, Tuple{Any, Vararg{X}} where X),
         (Tuple{X, X} where X<:Real, Tuple{X, X, Vararg{X}} where X>:Int, Tuple{X, X} where X>:Int),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{Vararg{X}} where Int<:X<:Real),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{Vararg{X}} where X>:Int),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{X, Vararg{X}} where Int<:X<:Real),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{X, Vararg{X}} where X>:Int),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{X, X, Vararg{Any}} where Int<:X<:Real),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{X, X, Vararg{Any}} where X>:Int),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{X, X, Vararg{Real}} where Int<:X<:Real),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{X, X, Vararg{Real}} where X>:Int),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{X, X, Vararg{X}} where Int<:X<:Real),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{X, X, Vararg{X}} where X>:Int),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{X, X} where Int<:X<:Real),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int, Tuple{X, X} where X>:Int),
       ];

julia> println(test_property.(examples))
Bool[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]

More examples:
improved_accuracy_examples.jl (2.5 MB)

Breaking down the last example:

julia> const A = Tuple{X, X} where X<:Real
Tuple{X, X} where X<:Real

julia> const B = Tuple{X, X} where X>:Int
Tuple{X, X} where X>:Int64

julia> const AB = typeintersect(A, B)
Tuple{X, X} where X<:Real

julia> const BA = typeintersect(B, A)
Tuple{X, X} where Int64<:X<:Real

julia> AB <: B  # suboptimal
false

julia> BA <: B  #    optimal
true
8

That’s good to know, but the more interesting property is if you can find examples of

function test_property(a, b)
    ab = typeintersect(a, b)::Type
    ba = typeintersect(b, a)::Type
    accuracy_improvement = (ab !== ba && (ab <: ba  || ba <: ab)
    accuracy_improvement
end

since if one of the intersections isn’t a strict subtype of the other, picking which one to return can not be done in a principled way.

9

Some nice ones:

julia> function test_property(a, b)
           ab = typeintersect(a, b)::Type
           ba = typeintersect(b, a)::Type
           (ab != ba && (ab <: ba || ba <: ab))::Bool
       end
test_property (generic function with 1 method)

julia> test_property(t) = test_property(t...)
test_property (generic function with 2 methods)

julia> examples = NTuple{2, Type}[
         (Tuple{T, T} where T<:Integer, Tuple{X, X} where Int<:X<:Real),
         (Tuple{T, T} where T<:Integer, Tuple{X, X} where X>:Int),
         (Tuple{X, X} where X<:Real, Tuple{X, X} where X>:Int),
         (Tuple{Vararg{X}} where X, Tuple{Any, Vararg{X}} where X),
         (Tuple{Vararg{X}} where X, Tuple{X, X, Vararg{Any}} where X),
       ];

julia> println(test_property.(examples))
Bool[1, 1, 1, 1, 1]

More examples

I’m not sure what are these more interesting for, though? Should I add these to the issue on Github?

EDIT: changed ab !== ba to ab != ba

1 Like
10

The reason why these are (IMO) more interesting is that these are ones where we could use to improve type intersection (at the cost of running the intersection twice).

1 Like
11

Wait, this was slightly wrong. I forgot the difference between != and !== on types. This should be (ab !== ba && (ab <: ba || ba <: ab))::Bool.

1 Like