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.
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}.
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.)
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.
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}).
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.