Unassigned type parameters in `UnionAll` of `Tuple` do not refer to concrete types in edge cases

General Usage
, , ,
1

Consider a simple example where I define a type alias for (non-empty) Tuple:

julia> const MyTuple1{T, N} = Tuple{T, Vararg{T, N}}
Tuple{T, Vararg{T, N}} where {T, N}

Even when the type parameter T is not assigned, the UnionAll-type MyTuple1 refers to all the instances of MyTuple1{T, N} where T and N are both concrete type parameters (meaning they are either concrete types or literal value like 1). This can be verified with the following example:

julia> t1 = Tuple{Int, Float64}
Tuple{Int64, Float64}

julia> t1 <: MyTuple1{Real}
true

julia> MyTuple1{Real} == Tuple{Real, Vararg{Real}}
true

julia> t1 <: MyTuple1
false

When T in MyTuple1 was unassigned, it included all possible concrete types but not abstract types like Real. Hence, even though t1 is a subtype of MyTuple1{Real}, it’s not a subtype of MyTuple1.

Such an implicit constraint on type parameters still holds when one type parameter is used as an upper bound for another type parameter:

julia> const MyTuple2{U, T<:U, N} = Tuple{T, Vararg{T, N}}
Tuple{T, Vararg{T, N}} where {U, T<:U, N}

julia> t1 <: MyTuple2
false

julia> t1 <: MyTuple2{Real}
false

julia> t1 <: MyTuple2{Real, Real}
true

Even when the upper-bound parameter U is set to Real, if T is unassigned, it does not include Real, unless I manually set it to be Real.

However, there are edge cases that break this implicit constraint on type parameters.

For example, when the type parameter is used as a lower bound, the bounded type parameter seems to be allowed to include abstract types when unassigned:

julia> const MyTuple3{U, T>:U, N} = Tuple{T, Vararg{T, N}}
Tuple{T, Vararg{T, N}} where {U, T>:U, N}

julia> t1 <: MyTuple3
true

So, my question is: Is this behavior expected?

Additionally, what’s more strange is the following paradoxical behaviors:

julia> t1 <: MyTuple3{Real}
true

julia> t1 <: MyTuple3{Float64}
false

julia> t1 <: MyTuple3{Float64, Real}
true

It appears that by setting U to be a concrete type Float64, T fell back to referring to all possible concrete types. I don’t know if this will be classified as a bug, but it’s definitely a bizarre behavior of the type system (on Julia 1.11.3).

Okay, what about having type parameters defined for both an upper and a lower bound? Here is the result:

julia> const MyTuple4{U, L<:U, L<:T<:U, N} = Tuple{L, Vararg{T, N}}
Tuple{L, Vararg{T, N}} where {U, L<:U, L<:T<:U, N}

julia> t1 <: MyTuple4
true

julia> t1 <: MyTuple4{Real}
true

julia> t1 <: MyTuple4{Real, Real}
true

julia> t1 <: MyTuple4{Real, Float64}
false

julia> t1 <: MyTuple4{Real, Real}
true

It seems that the “fall-back effect” of a concrete lower-bound parameter still persists, whereas when both U and L are unassigned, they do include abstract-type instances.

2 Likes
2

Regarding the constraint that restricts a type parameter of an UnionAll to concrete types, it’s called the diagonal rule. The open-access paper Julia Subtyping: A Rational Reconstruction (with DOI 10.1145/3276483) describes it like so:

This rule requires that if a type variable appears more than once in covariant position, it can be instantiated only with a concrete type

In more detail later in the paper:

A variable is said to be in covariant position if only Tuple, Union, and UnionAll type constructors occur between an occurrence of the variable and the where construct that introduces it. The diagonal rule states that if a variable occurs more than once in covariant position, and never in invariant position, then it is restricted to ranging over only concrete types.

The diagonal rule is also discussed in the Julia documentation, though only in the devdocs, for some reason: Diagonal types.

Regarding the unexpected behavior you point out: before publishing the paper, the authors of the paper made a suggestion to the Julia authors to relax the diagonal rule regarding lower bounds for pragmatic reasons:

This is also discussed in the paper itself, at the bottom of the paper, under Issues reported to Julia developers:

Whenever the programmer specifies explicitly a lower bound for a type-variable, as in Tuple{T,T}where T>:t, it is not always easy to decide if T should be considered diagonal or not. This depends on whether the lower bound, t, is concrete, but in general deciding concreteness is hard and Julia implementation approximates it with an heuristic. We proposed that the variables should be considered diagonal only if their concreteness is obvious. The proposal was approved, implemented and merged into the master branch.

2 Likes
3

Thank you for providing relevant materials! They are very informative!

I understand it’s more pragmatic for T to be considered non-diagonal (i.e., including abstract types in Tuple) when an explicit lower bound parameter is used. I don’t understand why T should fall back to being diagonal when the lower bound is a concrete type:

julia> const MyTuple5{T, S} = Tuple{T, T, T} where {S, T>:S}
Tuple{T, T, T} where {S, T>:S}

julia> (Tuple{A, A, Number} where A>:Number) <: MyTuple5
true

julia> (Tuple{A, A, Number} where A>:Number) <: MyTuple5{Float64}
false

To me, just because S is set to be Float64, it does not mean I would want T also to be concrete. Because if that’s the case, I would have just used NTuple{3, T} instead of MyTuple5 in the first place. Isn’t it assumed that a type that can be a supertype of a concrete S (and S is not set to be Union{}) should be inferred as an abstract type? If there isn’t some implementation obstacle, I don’t see why we can’t lift off the diagonal-type rule for T even when S is assigned a concrete type. (I’d like to learn more if there is any!)

Moreover, the current convention for switching on/off the diagonal-type rule for T seems inconsistent in the following case:

julia> (Tuple{A, A, Number} where A>:Number) <: Tuple{T, T, T} where {T>:Float64}
false

julia> (Tuple{A, A, Number} where A>:Number) <: Tuple{T, T, T} where {S>:Float64, T>:S}
true

In the first line, the diagonal-type rule is turned on when T is lower-bounded by a concrete type Float64. However, in the second line, when T is bounded by S, which should be diagonal (i.e., only allowed to refer to any concrete types) as it is bounded by Float64, granted T the permission to refer to abstract types…

I suppose the cause behind such a consequence could be that S where {S>:Float64} is deemed an abstract type, so the diagonal-type rule is then turned off for T when it’s bounded by S. But if the diagonal-type rule is so easily turned off (rather than persisting across all type parameters iteratively as long as the initial bound enforces the diagonal-type rule), then why do we need to enforce it for a type parameter bounded by a literal concrete type in the first place?

2 Likes
4

TBT to this lower bound of a Tuple parameter messing with me:

julia> Tuple{Int} <: (Tuple{T} where T>:Real) # huh?
true

julia> Tuple{Any} <: (Tuple{T} where T>:Real) # obviously
true

julia> Tuple{Int} <: Tuple{Any} # obviously...oh right, covariance
true
5

I think it may be way too late for making that change, as explained here PSA: Julia is not at that stage of development anymore.

If you really want to make this change, you could make a PR. Assuming it passes the Julia test suite, it could be further evaluated with PkgEval, to see which registered packages’ test suites does it break. Hypothetically it could get accepted as a minor change if it’s not too breaking, however I think you’d have to present a stronger motivation than given here.

It might be interesting to see what would such a PR break in the ecosystem :joy:

1 Like