How to interpret "Type{T} where T" in Julia's type system

New to Julia
, ,
12

Three confusing things are happening here:

  1. In Julia, types are values and values are types. We can’t draw clear distinctions between them. All types are values that are instances of DataType (well, almost Union{} strikes again!). But that means we couldn’t dispatch on a type because they are all DataTypes. So…
  2. Type is a unique, special-cased type that allows for sharpening type fields. It is extremely important to dispatch and such, but it does cause a violation of the type system’s rules which–I believe–leads to the friction you’re experiencing. Specifically, while each type is an instance of the concrete type DataType, it is ALSO an instance of the concrete type Type{T} (for some T). This is normally impossible (an instance can only be of one concrete type). Edit: see my comment below, this is not correct.
  3. Any is the top of that type system. By definition, all types are subtypes of Any. But Any is also an instance of DataType because types are just values. Not too weird, but it does yield funny things like:
julia> typeof(Any) <: Any
true

Your taxonomy of types doesn’t work because it presupposes that there are different kinds of types. There are not. Julia has a type system which describes the super- and sub-type relationships between all types, without drawing distinctions between those types.

The “issue” that

Isn’t an issue for the soundness of the system. Walking through it:

  1. Int isa Type{Int} – as we’ve addressed, this is the odd case.
  2. Type{Int} <: DataType – This is true because in a deep way Type{T} where T === DataType, so this is like saying Type{Int} <: Type which is true.
  3. DataType <: Type – All types, including DataType, are Types. Specifically, DataType isa Type{DataType}.
  4. Type <: Any this is axiomatic to the Julia type system.

I also don’t understand where your claim that:

comes from in the docs? Can you clarify the contradiction you’re seeing? Based on my reading of your code example above that claim, I don’t see an issue.

  • DataType is the type of all types. So DataType (being a type) is an instance of DataType.
  • Also, T <: T is true for all T where T is a type. So DataType <: DataType must be true.
  • DataType is an unparametrized type that has instances (all the other types), so it behaves like any concrete type.

Edit: Thinking about this more – I’m actually wondering if it’s more like DataType is the real special case because it is basically Type{T} where T in a trenchcoat pretending to be concrete even though it’s a UnionAll? I don’t know. Someone who knows more Type Theory will have to weigh in there :sweat_smile:

2 Likes