Julia: Subtyping bug: `Type{T} where DataType<:T<:DataType` and `Type{DataType}` behave differently

[abolotina]

The following looks for me like a bug in Julia 1.2.0. It says false on this judgment:

julia> (Type{T} where DataType<:T<:DataType) <: DataType
false

However, this holds:

julia> Type{DataType} <: DataType
true

Also,

julia> (Type{T} where DataType<:T<:DataType) <: Type{DataType}
true

julia> Type{DataType} <: Type{T} where DataType<:T<:DataType
true

I think this behavior is incorrect, for the equal types behave differently.

Version info:

Julia Version 1.2.0
Commit c6da87ff4b (2019-08-20 00:03 UTC)
Platform Info:
  OS: Linux (x86_64-pc-linux-gnu)
  CPU: Intel(R) Core(TM) i3-7100U CPU @ 2.40GHz
  WORD_SIZE: 64
  LIBM: libopenlibm
  LLVM: libLLVM-6.0.1 (ORCJIT, skylake)

[julbinb]

I agree that equal types should behave consistently. I'd say that Type{DataType} <: DataType should not hold. At least, it is so for normal types:

julia> Type{Int} <: Int
false

[vtjnash]

julia> Type{Int} <: DataType
true

[julbinb]

Oh, indeed. Is there a motivation why Type{t} <: DataType should hold? It seems logical that typeof(Type{t}) is DataType, but I wonder why it is also true for subtyping.

Also, DataType <: Type...

[abolotina]

I'm not a Julia expert, but it seems to me that Type{DataType} and DataType are the same thing:

julia> isa(Type{DataType}, DataType)
true

julia> isa(DataType, Type{DataType})
true

This is why I vote that Type{DataType} <: DataType should return true.

[julbinb]

Hm, this is curious. I expected isa(x, t) to mean typeof(x) <: t, but for isa(DataType, Type{DataType}) this does not hold.

[ulysses4ever]

it seems to me that Type{DataType} and DataType are the same thing:

I don't think you can rely on isa here. Only <: can prove "the same thing" for types.

The two expressions you check have subtle meanings:

isa(Type{DataType}, DataType)

is true because every type (or rather "type object") in Julia (including Type{t}) is an instance of DataType -- that's the definition of DataType. On the other hand,

isa(DataType, Type{DataType})

is true because it's just the definition of Type{t} -- it's a type whose single instance is t, if t is a type.

[abolotina]

Your explanation is interesting. I found that in the Julia 1.2.0 documentation:

In other words, isa(A,Type{B}) is true if and only if A and B are the same object and that object is a type.

I thought that "the same object and that object is a type" means "the same type." But now I'm not sure that this statement is correct.

[ulysses4ever]

@Maryann13 I believe that's (equivalent to) what I said. The thing is Julia has a banch of facilities to reason about types (e.g. <:) and a bunch of them to reason about terms/objects (e.g. isa). Depending on what you use, things like Int can have different meanings: in the context of <:, Int is a type, but in the context of isa, Int is an object representing the type Int on the term level. On the term level, object Int has type Type{Int}, but it has nothing to do with the properties of type Int (e.g. Int being a subtype of something, etc.).

Although, this is a nice description of term-level behavior of Type{T}, no one really understands how Type{T} should behave on the type level (e.g. w.r.t. <:) — including @JeffBezanson, I believe -- from what I remember from conversations with him during our work. I think that's the ultimate reason of the Type-related bugs like this one.

@Maryann13 To become more comfortable with term-level objects like Int, you might want to try building vectors of such objects and inspect their types or play with them otherwise, e.g. [Int, Bool], Type{Int}[Int, Int], Type[Int, Bool], etc.