What is difference between Type{T} and T

[goretkin]

@path-doc

You will note that on Types · The Julia Language, there are certain more abstract types where isa is used instead of <: . I expect that <: does not account for relationships higher-up the type hierarchy.

Note that this page of the manual has been changed since this published version. You can see the latest (unformatted) version here: https://github.com/JuliaLang/julia/blob/master/doc/src/manual/types.md

In particular, the discussion around Type{...} has been updated.

[liuyxpp]

Agree! We may even find an answer that is better than the documentation and hopefully a PR for doc.

[goretkin]

@Henrique_Becker

I believe we cannot have typeof(Int64) as Type{Int64} because then typeof(typeof(Int64)) would be Type{Type{Int64}} and so on, instead of the cycle at DataType but I am not sure what would break by doing this.

Yes, it would be a different system without that cycle. I can’t articulate what would break, but it seems at least awkward for a dynamic language with multiple dispatch, because you would like some way to dispatch on any type, even if it’s a higher-order type.

Just to illustrate, as you mentioned, that there are types like typeof(...), but not higher:

julia> sin
sin (generic function with 13 methods)

julia> typeof(sin)
typeof(sin)

julia> typeof(typeof(sin))
DataType

[path-doc]

Yes, sorry, that’s why I changed my post.

I think that, in my initial read, I was distracted by the prescriptive tone of your comments

@Henrique_Becker

So does not make sense to me to use isa to establish any ordering/tree, you should be using <: for it.

If <: is indeed a subrelation of isa, and I am interested in type hierarchies, then I hope you will agree that there is no reason why I should not be using isa.

[path-doc]

@Henrique_Becker

I believe we cannot have typeof(Int64) as Type{Int64} because then typeof(typeof(Int64)) would be Type{Type{Int64}} and so on, instead of the cycle at DataType but I am not sure what would break by doing this.

My turn to be prescriptive: the “and so on” bit is exactly what you should have in any complete description of a type space. This is what higher order reasoning entails.

Please can you (and @Henrique_Becker) clarify what is meant by “a cycle at DataType”? DataType is a node on the graph, no?

I think DataType is acting as a kind of “fixed point” to avoid unbounded hierarchies (no cycles here).

[path-doc]

Thanks for pointing this out, this is useful information to have.

I have just checked, and I can see that isa is still used in some cases instead of <: . So I don’t really see the relevance to my statement. Please feel free to enlighten me.

[goretkin]

@path-doc

Please can you (and @Henrique_Becker) clarify what is meant by "a cycle at DataType "? DataType is a node on the graph, no?

I think DataType is acting as a kind of “fixed point” to avoid unbounded hierarchies (no cycles here).

Yeah, it sounds like you understand what I meant with “cycle”. I am talking about a cycle because if in your graph there is an edge S → T iff T == typeof(S), then there is a self-loop at S = T = DataType.

I am not sure that I understand your confusion about <: and isa.

julia> Int isa Integer
false

julia> Int <: Integer
true

julia> 3 isa Integer
true

julia> 3 <: Integer
ERROR: TypeError: in <:, expected Type, got a value of type Int64

Where it gets tricky is with the special Type type, which seems like it lets you express the <: relation using isa:

julia> Int <: Integer
true

julia> Int isa Type{<:Integer}
true

I think that S <: T === S isa Type{<:T} for all types S and T.

[path-doc]

@goretkin

julia> Int isa Integer
false

julia> Int <: Integer
true

julia> 3 isa Integer
true

julia> 3 <: Integer
ERROR: TypeError: in <:, expected Type, got a value of type Int64

Well done, that proves that <: is not a subrelation of isa.

@goretkin

I am talking about a cycle because if in your graph there is an edge S → T iff T == typeof(S) , then there is a self-loop at S = T = DataType .

Self-loops are just saying that the binary relation is “reflexive” (like \leq instead of <). That’s okay, I mean partial orders are reflexive.

@goretkin

Where it gets tricky is with the special Type type, which seems like it lets you express the <: relation using isa :

julia> Int <: Integer
true

julia> Int isa Type{<:Integer}
true

I think that S <: T === S isa Type{<:T} for all types S and T .

Very nice, I will think about this and get back to you. (I think I saw === defined in the link you sent.)

[goretkin]

@path-doc

Self-loops are just saying that the binary relation is “reflexive” (like ≤\leq instead of << ). That’s okay, I mean partial orders are reflexive.

Note that it’s not the case that all the nodes have that self-loop, rather DataType is unique in that way. So it’s not that the relation R(a, b) = (a == typeof(b)) is reflexive. It is most certainly not.

@path-doc

(I think I saw === defined in the link you sent.)

Sorry if that was confusing. I could have just written == in this case.

[path-doc]

Am I right in thinking that Type{<:T} is equivalent to the set of objects that are either at level T or lower according to <: ?
For instance

julia> DataType isa Type{Any}
false

julia> DataType isa Type{<:Any}
true

Assuming you are right, then you have shown that, the restriction of isa to the image of Type{<: } is isomorphic to <: . In other words, you have succeeded in “embedding” <: in isa. This is nice. What it does not provide is a characterisation of isa.

@goretkin

Note that it’s not the case that all the nodes have that self-loop, rather DataType is unique in that way. So it’s not that the relation R(a, b) = (a == typeof(b)) is reflexive. It is most certainly not.

Great, so this establishes that <: is not a partial order. Further clarification on what you mean by “unique” would be useful:

julia> DataType <: DataType
true

julia> Any <: Any
true

julia> Type <: Type
true

julia> Int <: Int
true

Is isa is characterised by typeof? if so, then we get reflexivity in the sense that, for every object x

julia> x isa typeof(x)
true

[goretkin]

@path-doc

Is isa reflexive?

“Relations” are a set theory “thing”, but I think I don’t know what set we’re discussing.

For R(a, b) = (b == typeof(a)), we can consider the set of all possible Julia objects (values).

julia> R(a, b) = (b == typeof(a))
R (generic function with 1 method)

julia> R(1, Int64)
true

julia> R(1, Integer)
false

julia> R(Any, Any)
false

julia> R(1, 1)
false

For R_isa(a, b) = (a isa b), you can’t:

julia> R_isa(1, Int64)
true

julia> R_isa(1, Integer)
true

julia> R_isa(Any, Any)
true

julia> R_isa(1, 1)
ERROR: TypeError: in isa, expected Type, got a value of type Int64

So that’s one thing to be clear about. It seems you’re asking set-theoretic questions, but set theory is famously not type theory, and it can be awkward to describe things that have types using set theory.

If you limit the sets to be only Julia objects that satisfy object isa DataType, or do something else to make isa be a Relation (e.g. if isa throws an error, return “false”), the answer is still, “no, isa is not reflexive”.

If I could take a step back, is there a different question you’re ultimately interested in answering? What is motivating you to ask these questions about relations?

And taking a step forward, I think you’ll find interesting structure if you consider the set of every julia object o such that o isa DataType and:

<: is a Relation. It is reflexive. It is probably supposed to be a partial order, but because the subtyping algorithm is 1. not simple, 2. not completely formalized, I am not confident that it is. I think the intent is that it be a partial order, in any case.

Also intended I believe is that the set of all DataTypes is a bounded lattice.

• Any and Union{} as the top and bottom.
• Union{S, T} and typeintersect(S, T) are “join” and “meet”.
• There is some additional structure due to abstract types. typejoin(S, T) is maybe also “meet” ? I’m not sure.

[path-doc]

I made an edit to clarify:

@path-doc

Is isa is characterised by typeof ? if so, then we get reflexivity in the sense that, for every object x

julia> x isa typeof(x)
true

[path-doc]

@goretkin

Also intended I believe is that the set of all DataType s is a bounded lattice.

• Any and Union{} as the top and bottom.
• Union{S, T} and typeintersect(S, T) are “join” and “meet”.
• There is some additional structure due to abstract types. typejoin(S, T) is maybe also “meet” ? I’m not sure.

But surely you agree that a bounded lattice is a partial order?

[path-doc]

@goretkin

So that’s one thing to be clear about. It seems you’re asking set-theoretic questions, but set theory is famously not type theory, and it can be awkward to describe things that have types using set theory.

I beg to differ, orders are relevant to type theory. And type theory is still, for all present purposes, still set theory. You would be amazed at how far one can get studying type spaces using sets, amazed. I am happy to provide references.

@goretkin

If I could take a step back, is there a different question you’re ultimately interested in answering? What is motivating you to ask these questions about relations?

My purpose is to understand the structure of the type hierarchy. This is what binary relations and functions do: allow you to understand structure. That is my only goal.

Anyway, I think the discourse has come to its natural conclusion with that post.

@path-doc

Assuming you are right, then you have shown that, the restriction of isa to the image of Type{<: } is isomorphic to <: . In other words, you have succeeded in “embedding” <: in isa . This is nice. What it does not provide is a characterisation of isa .

This still stands.

[Tamas_Papp]

@goretkin

the subtyping algorithm is 1. not simple, 2. not completely formalized, I am not confident that it is.

There is a nice paper “Julia subtyping: a rational reconstruction” about it, eg

Julia subtyping: a rational reconstruction | Proceedings of the ACM on...

[goretkin]

@path-doc

But surely you agree that a bounded lattice is a partial order?

Yup. I just mean that the implementation of those computational procedures might not actually perfectly exhibit the necessary properties, either due to bugs or for good practical reasons that I’m not familiar with.

[path-doc]

Thanks for this paper. It’s great to get some clarity, like breathing pure oxygen in fact. Concrete types and the definition of typeof in appendix A should address most of my concerns (assuming I am right in thinking that isa is the binary relation / graph form of typeof).

[Sukera]

For the most comprehensive talk about the type system:

JuliaCon 2017 | The State of the Type System | Jeff Bezanson

The syntax may not all be still valid, but the semantics basically haven’t changed.

[Sukera]

@path-doc

@path-doc

Assuming you are right, then you have shown that, the restriction of isa to the image of Type{<: } is isomorphic to <: . In other words, you have succeeded in “embedding” <: in isa . This is nice. What it does not provide is a characterisation of isa .

This still stands.

The difference comes down to values and types. A type is a set of values. <: is the subtyping relation, equivalent to ⊆ from set theory. isa gives values a meaning here - X isa Y is equivalent to asking typeof(X) <: Y (or, equivalently, is X in the set described by Y).

This should cover all values except for instances of DataType (e.g. Int, what you’d refer to as “type”), because of the mentioned loops above. Some more information can be found here, the relevant implementation for these builtins can be found here. In particular, isa is implemented here.

[zdenek_hurak]

I think that the sentence “In Julia types are data as well” is crucial.