# 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