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

New to Julia
, ,
1

I have some problems parsing the Julias type-system.. and I came up with a few questions.

  1. Docs - Types: “Type{T} is an abstract type whose only instance is the object T”

How can an abstract type have instances??

  1. As far as I can understand is Type{T} kind of a special thing that has the following defining property: " isa(A,Type{B}) is true iff A and B are the same object and that object is a type". Why has this special thing DataType, Union etc. as subtypes?
julia> subtypes(Type)
4-element Array{Any,1}:
 Core.TypeofBottom
 DataType
 Union
 UnionAll

  1. Are all types of some type that is listed above?

  2. Let D be an instance of DataType, thus isa(D, DataType) is true. By the definition of Type{T} is also isa(D,Type{D}) true. This leads me to the conclusion that either DataType <: Type{D} or Type{D} <: DataType must be true. And indeed for D=Int holds the second relation true. But why runnig supertype(Type{Int}) returns Any even though the documentation says “declared types ( DataType ) have unambiguous supertypes” (typeof(Type{Int}) is equal DataType)… Other thing is that isabstracttype(DataType) returns false but Type{Int} <: DataType is true. Is it possible to use non abstract types as supertypes?

I am very confused.. if someone knows any other sources that explain this matter I would be grateful. Thanks in advance.

3 Likes
2

You misunderstood: T can be any type (including an abstract type), while Type{T} is another type, for which the only instance is T. Types can be values, too.

Types (as values) also have a type.

Yes.

No, concrete types cannot have subtypes.

I think the docs are the best source. I would suggest that you think of Type{T} as something which helps you dispatch on types, eg as in

julia> struct Foo end

julia> f(::Foo) = "the value"
f (generic function with 1 method)

julia> f(::Type{Foo}) = "the type"
f (generic function with 2 methods)

julia> f(Foo())
"the value"

julia> f(Foo)
"the type"

and otherwise not worry about the types of types unless you are working on the internals of Julia.

9 Likes
3

Thank you for your answer.

Yes I do understand but Type{T} where T is an abstract type. (isabstracttype(Type{T} where T) is true)

Yes but I don’t get it why should they be a subtype of Type{T} where T if Type{T} where T is something which introduces some special behaviour on its own.

Sadly, it doesn’t seem to be consistent with the behaviour I described. isconcretetype(DataType) returns true

I just wanted to fully understand it but I think you are right, from the user perspective it shouldn’t be a big deal if I don’t have the whole picture. Thanks

4

Note that Type{T} where T is an UnionAll type, and as such it is of course not concrete. There is nothing specific to Type here. Cf

julia> isconcretetype(Vector{Int})
true

julia> isconcretetype(Vector{T} where T) # == Vector
false

I don’t see the inconsistency (in the language, I am still not sure what behavior you are describing).

1 Like
5

The behaviour is the following:
1.

julia> isconcretetype(DataType)
true

julia> Type{Int} <: DataType
true

So Type{Int} is a child of a concrete type.

and is still able to have instances ??

julia> isa(Int, Type{Int})
true

EDIT: maybe the meaning of an abstract type is just that it cannot be instantiated but may somehow have instances

julia> supertype(Type{Int})
Any

julia> Type{Int} <: DataType
true

Supertype returns Any although it is a subtype of DataType

6

Type{Int} <: DataType is true in the same way that 5<:Int. It’s not saying “is a subtype of”, it’s saying, “is an instance of”.

7

That is not the case. The following comes straight from REPL help.

<:(T1, T2)


  Subtype operator: returns true if and only if all
  values of type T1 are also of type T2.

  Examples
  ≡≡≡≡≡≡≡≡≡≡

  julia> Float64 <: AbstractFloat
  true

  julia> Vector{Int} <: AbstractArray
  true

  julia> Matrix{Float64} <: Matrix{AbstractFloat}
  false
8

Note that x isa A and A <: B means that x isa B, eg

julia> map(T -> 5 isa T, (Int, Real, Number))
(true, true, true)

The manual tells you what an abstract type is:

Abstract types cannot be instantiated, and serve only as nodes in the type graph, thereby describing sets of related concrete types: those concrete types which are their descendants.

Again, I would recommend that you read the manual and allow some time to digest it. Figuring out these things by trial and error may be a somewhat confusing approach. YMMV.

9

5<:Int is not true. It’s an error, since 5 is not a type. Type{Int} <: DataType is true because Type{Int} is a subtype of DataType.
I think Type is the only case in the language where an abstract type is a subtype of a concrete type. I also found it surprising and confusing when I first encountered it, though I suppose it doesn’t technically contradict anything the docs say.

That’s not true, although the docs seem to suggest that, and I think that’s the main confusing point here.
One example of a concrete type having a subtype is Type{Int} <: DataType, as @samuel noted. Other examples are Union{} <: Int and Tuple{Int,Float64} <: Tuple{Integer,Real}.

EDIT: I also share @samuel’s confusion about the fact that supertype(Type{Int}) !== DataType. Seems like a bug, as far as I understand, but maybe not, since the docs don’t seems to define what “the supertype” means (the docs also mention the terms “unambiguous supertype”, “immediate supertype”, and “direct supertype”, which persumably refer to the same thing supertype is supposed to return).

1 Like
10

I prefer to think of the type system the following way:

  1. A tree of abstract types, with concrete types as the leaf nodes. The root is Any. Relevant keywords are abstract type and struct.
  2. Each node in the above tree describes a UnionAll set when parametrized, invariance is the key concept here. The relevant keyword is where.
  3. Tuples, which are in contrast covariant.

Technically DataType and Type{T} are types, and thus <: can be used to compare them. But for most practical code, I don’t think it is advantageous to think of these types as being part of the type hierarchy. Similarly, Base.Bottom / Union{} is there to make a lattice, and is useful for some code manipulating types, but most users can safely ignore it when encountering the Julia type system for the first time. Keep in mind that its main purpose is organizing dispatch and efficient compilation.

2 Likes
11

Though it might be too late, but I still want to add my understanding to the type system of Julia.

It’s better understood as several levels of “type universes”.

Let’s say level-0 types are concrete values like 1, "a". And level-1 types are “usual” types like Int, Real, Number, Any.

Now there are two operations we could do to compare them:

  1. isa(A, B) asks if a type A in level n has type B in level n+1. So we do 1 isa Int.
  2. A <: B asks if type B includes type A where A, B are of the same level (this doesn’t work for level-0 obviously but that’s not very important).

Now types in level-1 should have types in level-2. This is where DataType, Type{Int}, etc. kicks in.

We have in particular

Int isa Type{Int} <: DataType <: Type <: Any

Note Int is a level-1 type and Type{Int}, DataType etc. are in level-2.
Note further that Any in the line above is a level-2 type while Any in Int <: Any is a level-1 type!!!

If you adopt such a mental model the type system somewhat make sense. However, I believe strongly that unfortunately Julia isn’t designed to be working as described above. This gives nonsensical on the results returned by isconcretetype and supertype on types with level > 1. In particular,

julia> DataType isa DataType <: DataType
true

julia> isconcretetype(DataType)
true

isconcretetype(DataType) really should be false according to the documentation.

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
13

I agree the compiler definitely doesn’t write according to my interpretation. But if you add special rules, DataType isn’t that universal to be the “type of all types”. Type of Vector is UnionAll.

I think for the best interest someone knowing those C files in the compiler should probably document all the additional rules.

14

Also to mention Type{T} for some T is not a concrete type despite having instance.

julia> isconcretetype(Type{Int})
false

julia> Int isa Type{Int}
true
1 Like
15

This is not special. Number is also not a concrete type, but 1 isa Number is true…

Perhaps the wording “has an instance” is confusing here? It is mentioned in the docs (same quote that @samuel mentioned originally, I’m just repeating it here for clarity) that

For each type T, Type{T} is an abstract parametric type whose only instance is the object T.

There seems to be an understanding that only concrete types can have instances. but this is just not true.

The same docs page also mentions for example

the :: operator is read as “is an instance of”. It can be used anywhere to assert that the value of the expression on the left is an instance of the type on the right. When the type on the right is concrete, the value on the left must have that type as its implementation

Of course any type can be on the right-hand side of ::, including abstract types. One example being Any, for which it is stated that

When no supertype is given, the default supertype is Any – a predefined abstract type that all objects are instances of and all types are subtypes of

So “having instances” is clearly possible for abstract types as well as abstract [EDIT: concrete] types.

As to the original question of @samuel , it does seem weird that both of these are true: [EDIT: The second one is not confusing here, just that both are true at the same time.]

Type{Int} <: DataType
Type{Int} isa DataType

The first one also seems confusing to me at first glance, but in the “set theory” picture that the REPL docstring of <: also gives

  Subtype operator: returns true if and only if all
  values of type T1 are also of type T2.

it makes sense. All values (instances) of Type{Int}, which is only Int, are also values (instances) of DataType since all concrete types are of type DataType (I presume that’s why its called DataType, since it directly refers to data and has to have some concrete memory layout, some numer of bytes required to represent the values etc. – but then again, also abstract types are of type DataType, e.g. Number if they are not unions or parametric).

But by this logic, also these have to be true:

  • DataType <: Type (every possible value of DataType is in fact a type, so it is also a possible value of Type
  • UnionAll <: Type (every value of UnionAll are essentially the parametric types, so again types)
  • Union <: Type (a union of any types is still a type, so if you write Union{Int, String} that itself is a type in the sense of “a type is a bag of all its possible values”)
  • I have no real clue what Core.TypeofBottom actually does…

I think the answer to the question 3 from the original post is yes:

  1. Are all types of some type that is listed above?

All concrete and “non-union or parametric” types are of type DataType, all parametric types are UnionAll and what’s left are Unions I guess.

Question number 4 is also confusing me, but I guess to get all the desired relations between Any, DataType, etc. it is necessary that Type{Int} <: DataType is true, but still DataType is considered a concrete type, since it has values that have a concrete memory layout etc.
This really does sound like a contradiction, but I think it comes down to the “fuzzyness” that @mrufsvold mentioned

In Julia, types are values and values are types. We can’t draw clear distinctions between them

16

@sevi , partially my bad. I mischaracterized the situation in my 2nd point, And said that there is (paraphrasing myself) “some concrete type Type{T} so types have more than one concrete type”. Which is not true. I didn’t realize that all Type values are abstract!

This actually settles any expections though because, with some simplification, we can say that these “type of type” types are defined as:

abstract type Type{T} <: Any end
struct DataType <: Type
    T
end

The weird thing that remains, is the special casing for <: which is something like:

:(<:)(::Type{T}, ::Type{Type{T2}) = T <: T2

I think this is the only case where <: is defined in a custom way (instead of being derived from the definition of a type).

17

I think my remaining confusion boils down to this:

  • Int (as a value) has typeof(Int) === DataType
  • Type{Int} has as its one (and only) possible value Int, so of course Int isa Type{Int} is true
  • From this we know that Type{Int} <: DataType should hold (it does)

This is only consistent if you don’t impose that concrete types cannot have subtypes. But (unlike the statement about “having instances”) this is kind of stated in the docs:

One particularly distinctive feature of Julia’s type system is that concrete types may not subtype each other: all concrete types are final and may only have abstract types as their supertypes.

DataType is a concrete type (all its values have typeof(x) === DataType as per definition of isconcretetype). However, Type types like Type{Int} are somehow formally subtypes of DataType, otherwise they don’t work as intended – so they are definitely a special thing. But when we start splitting hairs here we realize that Type{Int} <: DataType does not contradict the above restriction for “concrete types”, because even though DataType is concrete, Type{Int} is not concrete (consistent with isconcretetype)!

That this distinction is normally not relevant and that these Type types are somewhat special is also reflected in @samuel 's earlier observation that all of these three statements are true:

Type{Int} <: DataType

supertype(Type{Int}) === Any

DataType <: Any

So Type{Int} has as its direct supertype Any, but it also has as a supertype DataType, which also has Any as supertype (like every other type of course).

Type{T} types just don’t fit into the usual “type tree” structure many people have in mind. That might be the reason why it’s called “type graph” in the docs instead of “type tree” (?)

Just to clarify: I don’t think that’s a problem and for me the Type types are just special things that are just needed for making dispatch a lot more powerful. As was mentioned earlier, for the vast majority the assumption that all the types are arranged in a tree, and that isconcretetype means that the thing has no subtypes, are working just fine to produce working and correct code :person_shrugging:

More rambling

Also I didn’t really appreciate this earlier, but I find it kind of neat that there is this “duality” (if that’s a good word for it) between types and values. Every type is a value and every value has a type. So in the end you need two “tops” of the type graph: One is the supertype of every type (in the sense that asking for the supertype repeadedly always ends up at Any) and one is the type of every value (in the sense that typeof applied repeatedly at some point ends up at DataType).

julia> typeof(Any)
DataType

julia> supertype(supertype(DataType))
Any

It would be cool if supertype(DataType) were Any directly, but I guess then we lose the convenient Type types again…

2 Likes
18

Make a PR to improve the Manual? The intent of the quoted paragraph is to say that it’s not possible to define a new type with a concrete strict supertype (with struct, mutable struct or abstract type).

Another exception to this “rule” is how Union{} subtypes all types, including all concrete types.

1 Like
19

Pretty sure supertype is just a helper for reflection, debugging and similar. It’s not important for the type system. <: is the single source of truth.

20

FWIW I have a diagram in the readme (at the very bottom) of one of my packages, TypeDomainNaturalNumbers.jl, visualizing the subtyping relation for the exported types. It’s a directed acyclic graph, because many of the exported types are Unions.