Playing around with Union{}, Type{Union{}}, Type{Core.TypeofBottom}, etc

Consider this weird Julia session:

$ julia
               _
   _       _ _(_)_     |  Documentation: https://docs.julialang.org
  (_)     | (_) (_)    |
   _ _   _| |_  __ _   |  Type "?" for help, "]?" for Pkg help.
  | | | | | | |/ _` |  |
  | | |_| | | | (_| |  |  Version 1.5.3 (2020-11-09)
 _/ |\__'_|_|_|\__'_|  |
|__/                   |

julia> function f1()
               local t = Union{}
               for _ in Base.OneTo(10)
                       println(t)
                       t = Type{t}
               end
               return nothing
       end
f1 (generic function with 1 method)

julia> function f2()
               local t = Union{}
               for _ in Base.OneTo(10)
                       println(t)
                       t = typeof(t)
               end
               return nothing
       end
f2 (generic function with 1 method)

julia> f1()
Union{}
Type{Union{}}
Type{Core.TypeofBottom}
Type{Type{Core.TypeofBottom}}
Type{Type{Type{Core.TypeofBottom}}}
Type{Type{Type{Type{Core.TypeofBottom}}}}
Type{Type{Type{Type{Type{Core.TypeofBottom}}}}}
Type{Type{Type{Type{Type{Type{Core.TypeofBottom}}}}}}
Type{Type{Type{Type{Type{Type{Type{Core.TypeofBottom}}}}}}}
Type{Type{Type{Type{Type{Type{Type{Type{Core.TypeofBottom}}}}}}}}

julia> f2()
Union{}
Core.TypeofBottom
DataType
DataType
DataType
DataType
DataType
DataType
DataType
DataType

I’ve got some questions:

  1. Why does the second iteration of f1() use Type{Union{}}, but subsequent iterations instead use Core.TypeofBottom?

  2. Why does f2() not use Type?

  3. What’s up with DataType, isn’t that for named types? To be specific, the documentation says “DataType represents explicitly declared types that have names, explicitly declared supertypes, and, optionally, parameters.”

  4. Are there any legitimate uses for such constructs (Type{Type{ ... Type{X} ... }}) :smile:

You’ve just hit the subtle differences between the semantic and the structural interpretation of a Julia type! Semantically, Type{Union{}} and Core.TypeofBottom represent the exact same thing, i.e. the type of the bottom type. Structurally, however, Type{Union{}} is represented as a parametrized Type while Core.TypeofBottom is a separate stand-alone entity.

julia> Type{Union{}} == Core.TypeofBottom
true

julia> Type{Union{}} === Core.TypeofBottom
false

Take it one step further and Julia will semantically normalize Type{Union{}} into Core.TypeofBottom, hence the Type{Core.TypeofBottom} in the third iteration.

For the second case, the built-in typeof function returns the structural type of the value. The value Union{}, for example, is structurally represented by Core.TypeofBottom, which in turn is a DataType. This confluence between structure and semantics is so complicated that the subtyping algorithm even has a dedicated section to deal with Type{...}, and we still have surprising behaviors sometimes. Consequently, I’d say it’s highly recommended we stay away from any kind of deeply nested Type{...}.

For a fun thought experiment, Type{DataType} and DataType is the Julia’s equivalent of the classic chicken and egg problem. DataType is obviously a Type{DataType}, but Type{DataType} is also a DataType. If you can point out the catch right away, then you have answered all of your questions :grin:.

3 Likes