Subtyping is not reflexive and not transitive with triangular rule

[julbinb]

In julia 0.6.0 subtyping is not reflexive for some examples.

julia> (Tuple{T, T} where Int<:T<:Int) <: (Tuple{T, T} where Int<:T<:Int)
false

julia> (Tuple{T, T} where T>:Int) <: (Tuple{T, T} where T>:Int)
false

It seems to me that there is a problem with lower bounds in triangular dispatched cases, because these examples work fine:

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

julia> (Tuple{T, T} where T<:Int) <: (Tuple{T, T} where T<:Int)
true

Also, transitivity is broken:

julia> T1 = Tuple{Number, Number, Ref{Number}}
Tuple{Number,Number,Ref{Number}}

julia> T2 = Tuple{T, T, Ref{T}} where T
Tuple{T,T,Ref{T}} where T

julia> T3 = Tuple{S, S, Ref{Q} where Q} where S
Tuple{S,S,Ref{Q} where Q} where S

julia> T1 <: T2
true

julia> T2 <: T3
true

julia> T1 <: T3
false

Although, to my understanding, T1 <: T2 == true and T1 <: T3 == false are correct, but T2 <: T3 == true is not. So it's not really transitivity, but rather some problem with T2 on the left.

Finally, this looks weird:

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

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

julia> Vector{Tuple{T, T} where Number<:T<:Number} <: Vector{Tuple{Number, Number}}
false

I don't see why vectors should not be in subtype relation.

Here is the version info:

Julia Version 0.6.0
Commit 903644385b (2017-06-19 13:05 UTC)
Platform Info:
  OS: Linux (x86_64-linux-gnu)
  CPU: Intel(R) Core(TM) i5-4200U CPU @ 1.60GHz
  WORD_SIZE: 64
  BLAS: libopenblas (USE64BITINT DYNAMIC_ARCH NO_AFFINITY Haswell)
  LAPACK: libopenblas64_
  LIBM: libopenlibm
  LLVM: libLLVM-3.9.1 (ORCJIT, haswell)

@JeffBezanson

[martinholters]

julia> Vector{Tuple{T, T} where Number<:T<:Number} <: Vector{Tuple{Number, Number}}
true

on master, so at least that has been fixed.

[JeffBezanson]

Thanks for these examples. In fact there was a TODO in the code asking for them. The diagonal rule has been tricky to get right.

[julbinb]

@JeffBezanson Thanks for the reply and the fix!

Related to this topic: should this example be true or false?

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

I would expect true, as there is only Tuple{Int,Int} on the left (for there is only one concrete type >: Int).

[martinholters]

I had a radical idea the other day: Make Tuples invariant in subtyping. Something like Tuple{Number,Any} would need to become Tuple{<:Number, <:Any}; Tuple{T,T} where T would automatically only match "diagonally" (but T would no longer have to be a leaf type). Up to here, I think this could simplify subtyping by removing lots of special cases. But Vararg would be tricky: Tuple{Vararg{Any}} would implicitly introduce an unknown number of TypeVars (being equivalent to Tuple{T1, T2, ...} where {T1, T2, ...}, which might add complications that could outweigh any benefits.

I guess such a radical change is off the table for 1.0 anyways, but has it been seriously considered in the past? If so, what were the conclusions?

[julbinb]

@JeffBezanson This doesn't seem right:

julia> Ref{Tuple{T, T} where T} <: Ref{Tuple{S, S}} where S
true

As there doesn't exist single S such that Tuple{T,T} where T == Tuple{S,S}.

But this is fine as is:

julia> Ref{Tuple{T} where T} <: Ref{Tuple{S}} where S
true

In this case we can chose S == Any and

julia> (Tuple{T} where T) == Tuple{Any}
true

[vtjnash]

If I remember correctly, the first should be OK, since Ref{Tuple{T, T} where T} should type-equal Ref{Tuple{Any, Any}} (currently seems like subtyping disagrees though).

[julbinb]

But Tuple{T,T} where T is a diagonal type, so T cannot be instantiated with Any.

[andyferris]

I too have wondered as @martinholters about exploring invariant tuples (for v2.0 I suppose).