Why isn't `Vector{<:Float64}` reduced to `Vector{Float64}`?

I’m not sure if I misremembered, but I thought when applying <: to a type parameter that represents a concrete type, <: would automatically be removed.

However, it seems that in Julia 1.10 and 1.11, that’s not the case, and Vector{<:Float64} and Vector{Float64} are not equivalent to each other.

julia> t1 = Vector{<:Float64}
Vector{<:Float64} (alias for Array{<:Float64, 1})

julia> t2 = Vector{Float64}
Vector{Float64} (alias for Array{Float64, 1})

julia> t2 <: t1
true

julia> t1 <: t2
false

Is there a reason for t1 and t2 not to be considered identical?

1 Like

This is in the Julia FAQ. There are many discussions that try to help explain this. See e.g.

I guess you are asking specifically about Vector{<:Float64}. Realize that Vector{<:T} for any type T is a set of types: Vector types for any subtype of T. Now, I guess your point is that, since Float64 is concrete, it has exactly one subtype Float64, so Vector{<:Float64} is a set containing only one element, Vector{Float64}. Still, in mathematics we generally don’t equate a set of a single element with that element: \{x\} \ne x. As noted by @nsajko below, the bottom type Union{} is a subtype of Float64, so Vector{Union{}} <: Vector{<:Float64}.

3 Likes

I am aware that Vector{T1} is not a subtype of Vector{T2} even if T1 <: T2… I am talking about the the specific case where T2 is a concrete type so it has no subtypes except itself.

In that case, one would assume Vector{<:T2} (a.k.a. Vector{T} where {T<:T2}) falls back to Vector{T2}.

Yes, I edited my post already to address that point. As I said, you are asking Julia to equate a set containing only one element with that element. They are certainly related, but it would not be normal in mathematics to equate the two. As noted by @nsajko below, the bottom type Union{} is a subtype of Float64, so Vector{Union{}} <: Vector{<:Float64}.

(That being said, there are other places in Julia that do blur this distinction. e.g. Union{Float64} == Float64 == Union{<:Float64}: the Union operation acts sort of like set union, but it seems to equate concrete types T with sets \{ T \}. Not doing this would be pretty inconvenient, though — instead of Union{Float32, Float64}, I guess you’d need to write something like Union{<:Float32, <:Float64}, which would make some pedantic sense but would annoy everyone in practice.)

5 Likes

Counterexample:

julia> Union{} <: Float64
true

Indeed, then we have:

julia> Vector{Union{}} <: Vector{<:Float64}
true

Don’t forget about the bottom type!

7 Likes

They aren’t the same thing because Vector{Union{}} is also a subtype of Vector{<:Float64}.

1 Like

This is very interesting. I guess it makes sense to define a “bottom type” with respect to Any as the “top type” for the entire type system. On the other hand, it seems that Union{} is not intended to be revealed to the user:

julia> subtypes(Float64)
Type[]

Anyway, thank you all for the comments that helped me deepen my understanding of Julia’s type system.

2 Likes

Its doc string is here: Union{}.

But definitely take a look at the subtype operator’s (<:) doc string, too. The in-development version of the doc string, specifically: <:

1 Like

If I understand correctly, Vector{<:Float64} and Vector{Float64} cannot differ in terms of the values they can contain (since there are no values of type Union{}).

Couldn’t the compiler just replace Vector{<:Float64} with Vector{Float64} ?

Also related question: Is there any difference in how Vector{<:Float64} and Vector{Float64} are stored in memory?

Vector{<:Float64} is an abstract type, so it doesn’t have any instances and hence no memory layout. It has two subtypes: Vector{Float64} and Vector{Union{}}, both of which can be instantiated, although the latter only has a single possible value, namely the empty vector Union{}[].

So in practical terms, I suppose that’s the most important distinction: Union{}[] isa Vector{<:Float64} but !(Union{}[] isa Vector{Float64}).

Made a PR to expand the doc string:

Also:

1 Like

Counterexample:

julia> Vector{Union{}}(undef, 2)
2-element Vector{Union{}}:
 #undef
 #undef

julia> Vector{Union{}}(undef, 1)
1-element Vector{Union{}}:
 #undef

So it can’t have elements (throws on access to any index), but, confusingly, it can have a nonzero length.

5 Likes

I think it would potentially be interesting for us to have a rule that a type is not instantiable if it contains a field with an uninhabited type, but enforcing that rule consistently would be very tricky.

Wouldn’t that be quite breaking? AFAIK some parts of the ecosystem, due to @tkf as far as I remember, but still very relevant, use a pattern of starting from an empty collection of Union{} element type, then adding elements one-by-one, progressively widening the element type.

1 Like

An empty Array{Union} doesn’t have uninhabitable fields. It’s only ones of size>0 that do. That probably does make this hard to implement though…

1 Like

Once upon a time I, too, suggested these should be unconstructible, but it was shot down pretty hard:

Interesting, thanks for the correction!

1 Like