What type union (`Union`) is equivalent to an iterated union (`UnionAll`) with a concrete type bound?

Internals & Design
, , ,
1

As far as I know and have read, the only subtypes of a concrete type that isn’t DataType are itself and the bottom type Union{}. However, that doesn’t seem to be the case as type parameters:

julia> let T = Vector, P = Int
         @assert !(T <: Tuple) && isconcretetype(P) && P !== DataType
         (Union{T{Union{}}, T{P}} == T{<:P},
          Union{T{Union{}}, T{P}} <: T{<:P},
          T{<:P} <: Union{T{Union{}}, T{P}})
       end
(false, true, false)

What other T{...} type could possibly subtype T{<:P}?

1 Like
2

Relevant discussion:

Summary: <: will return false if it was not able to prove subsetting. So, while the analogy between sets and types is useful, it often breaks down.

The main thing that subtyping has to follow for correctness is being a partial order (there are some open issues with transitivity counterexamples!), see the doc string:

(I’d move this topic from Internals to General.)

1 Like
3

I suppose if dispatching over type parameters or concrete types of instances is the point, then subtyping <: doesn’t have to perfectly align with type union subsetting, it just needs to “preserve transitivity.” But then does that mean == (ccalls :jl_types_equal) or two-way <: just doesn’t really compute type union equality to begin with?

I did know that type unions aren’t sets in some ways, but this still surprised me (and you too) given the straightforward description of parametric types and subtyping. Wonder if there’s a simple thing that could be added to the documentation that clears up the exact distinction.

1 Like
4

<: is the single source of truth on subtyping. It is always correct, by definition, as long as it’s a partial order. Actually it also must be a lattice, regarding top (Any) and bottom (Union{}) types.

5

What I said was kinda off, maybe it’s better to make a clear divide: consider that any Julia type is a supertype to members of a unique, exhaustive set of concrete Julia types, Type{...}, Union{}, or whatever else that’s roughly a “leaf” type. I’m gathering that

  • <: of types implies subsetting of such sets but not vice versa, which is sufficient for type-based method dispatch in practice.
  • == of types imply equality of such sets but not vice versa. I don’t know if jl_types_equal is implemented as a two-way <: check the same way set equality is equivalent to two-way subsetting.
1 Like
6

I’m pretty sure that, yes, jl_types_equal is just an optimization and should behave the same as checking for subtyping in both directions.