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

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

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
``````

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

2 Likes

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

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

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?

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
``````

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.

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

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

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