I am glad that you find the paper helpful.
However, I don’t think that a formal understanding of the edge cases of Julia’s type system is necessary for being productive in Julia. A lot of concepts are very intuitive, and having to think about complex type graphs in Julia code may be a code smell in itself.
That should be the talk Introduction to Julia Internals. I’d recommend to watch it at least three times, screenshot at ~5:50.
For clarification, the right box of each double-box is the value and the left box is its corresponding type.
This diagram and talk are very helpful, thanks. I now have an answer to my original short question.
DataType is indeed the top of the type tree according to typeof (not isa or <:). It’s nice to see my intuition was correct even though I didn’t have the vocabulary to express this earlier.
Moreover, DataType is unique in the sense that it’s the only type that’s equal to its value. That’s the fixed-point property.
That’s great, thanks!
While technically true, it’s not really useful to think of it that way - type computations are done in regards to <:, which has Any as its top type and Union{} as its bottom type. typeof is also not a relation, contrary to <:, as it’s 1-ary and not binary.
It’s more accurate to say that each value has some type defined by typeof, which can be related to one another via <:.
It’s not my way of thinking, its a fact: DataType is the top according to typeof, not according to <: of course.
typeof does not establish a relation though. There is no (partial) order defined by applying it - you need <: to establish that. In some sense, the graphic above is misleading in that regard since it suggests that there is.
I think what you’re thinking about is recursively applying typeof, in which case, yes, that chain is what you end up with, but again, that is orthogonal to subtyping and Type{T} vs T.
Yes, you or I may not have written one down, but typeof will be associated with a binary relation, lets call it R. According to R, DataType is top.
Yes, it is distinct from or independent of <:.
Very cool. I love getting to the bottom of things.
Right, that’s what I meant. In graph parlance, that relation can only ever be applied <=2 times before arriving at the DataType loop, so it’s not really a useful relation when trying to work with it. You just loose a lot of information in each application of typeof. You can picture it like (type on the left, value on the right again)
and as it works now, it will never get to a third fourth sublevel here. It’s a very shallow, very wide tree (that could be considered an implementation detail to allow types to be used as values).
I guess I technically could put Int|1 under DataType|Integer as well, but that’s exactly the point where <: comes into play, so that’s why I didnt. You’d also lose the representation of “going up one level is one application of typeof”.
Thanks it’s structure of that left-hand-side that I wanted to understand. I mean, for obvious reason, there is a lot more out there about <: because that’s the relation we need when passing bits of data around. But one interpretation of Jeff Bezanson in the 2014 video is that much of the power of Julia lies in understanding both sides of the type coin: the “tag” on the left and the “bits” on the right (or type and value as you put it).
Around 4:26 
We go nuts with it.
@goretkin Sincere apologies for confusion here. I’m afraid I didn’t have the product structure \text{tags} \times \text{bits} in mind when we were discussing this. I now see that (Where tags and bits are the terminology of Jeff Bezanson in the 2014 video.)R and <: are independently defined on \text{tags} and \text{bits} respectively.
I do not know if this was already cited. But on another recent thread the issue #29368 redesign typeof(::Type) was mentioned, and right on the original post:
A related issue is that types like
DataTypeandType{Int}have an overly-complex subtype and specificity relationship: one is not a subtype of the other, but their intersection is non-empty, and we’re not able to accurately represent that intersection. For various reasons (including backwards compatibility) subtyping currently gets this wrong on purpose, makingType{Int} <: DataTypetrue.
For future reference and the sake of completeness, I wish to clear up the answer to the second “longer” question that I asked. To more precise, I will clarify the sense in which concrete types form a tree. In particular, I’ll now complete the description of the partial ordering R on the set of objects that is induced by the function typeof and show that R describes an inverted tree with \text{DataType} \times \text{DataType} at the top.
The Concrete Type Tree
It is not a completely naive construction. The most basic problem is that (as per appendix A of Julia subtyping: a rational reconstruction | Proceedings of the ACM on Programming Languages) the domain of typeof is not only the set of type tags it also accepts values. Thus (contrary to what I suggested in a previous post) we cannot define R on type tags alone.
The graph of typeof and the set of objects X.
In what follows, I take as given that the left-hand side of every object is a “concrete type tag”, henceforth a member of the set \text{ctypes}. The right-hand side of every object is the value of the object and a member of the set \text{values}. Note that every t \in \text{ctypes} satisfies t = v for some v \in \text{values}. Every object x is an element of the Cartesian product X = \text{ctypes} \times \text{values}. (Note that X is simply a transposition of the functional graph of \text{typeof}.)
Objects x = t_x \times v_x such that v_x \in \text{values} - \text{ctypes} are, by definition “leaves” of the graph since v_x does not belong to the image of \text{typeof}. Let L denote the set of such objects. For every object x = t_x \times v_x such that v_x \in \text{ctypes}, there exists an object y = t_y \times v_y \in X such that \text{typeof}(v_y) = v_x. Let \neg L denote the latter set of objects (chosen because such objects are never leaves). Then L \cup (\neg L) is equal to X.
The definition of R.
We will take R to be a binary relation on X with asymmetric part P and symmetric part I. R is then the disjoint union of P and I and, as a binary relation, it is a subset of the product of X\times X.
Definition of I. Take I to be the main diagonal of X \times X, so that it is by definition reflexive. Then R is also anti-symmetric because x \mathbin{I} y implies x = y.
Definition of P. Let the binary relation Q be defined by:
Now let P = Q - \{y \times y\} where y is the object \text{DataType}\times \text{DataType}. Because of the \text{DataType} is the unique fixed point of \text{typeof}, P is indeed asymmetric.
It remains to be shown that R is transitive. Suppose not. Then there exist x , y , z \in X such that x \mathbin{R} y \mathbin{R} z and \neg (x \mathbin{R} z). Then \neg (x \mathbin{R} z) and symmetry of I implies x \neq z. Moreover x \mathbin{R} y and \neg(x \mathbin{R} z) together imply that y \neq z. Similarly, y \mathbin{R} z and \neg (x \mathbin{R} z) together imply that x \neq y. Thus, x, y and z are pairwise distinct.
Then, together, anti-symmetry of R and x \mathbin{R} y \mathbin{R} z imply that both x \mathbin{P} y and y \mathbin{P} z. This is equivalent to \text{typeof} (v_x) = v_y and \text{typeof}(v_y) = v_z. But then (\text{typeof} \circ \text{typeof}) (v_x) = v_z, so that x \mathbin{P} z. This contradicts the assumption that \neg ( x \mathbin{R} z).
Thus R is indeed a partial order. The fact that R is an inverted tree follows from anti-symmetry of R and the fact that P is formed via repeated composition of \text{typeof}.
Note 1. The unique fixed point of the (monotone increasing in the partial order R) map v \mapsto \text{typeof}(v) = t is \text{DataType}.
Note 2. Via the example at the bottom of page 17 of Julia subtyping: a rational reconstruction | Proceedings of the ACM on Programming Languages, <: is intransitive. Though this is a bug, this implies that the tree (X,R) is in fact the only type tree we have in Julia! (Though I’m not sure how sub/super types deals with the intransitivities of <:.)
Note 3. Any relation that we might induce from isa is, via my preceding post, intransitive and hence not a partial order.
Note 4. The above construction shows that we could also have simply worked with values. This is because the construction of R relies on \text{typeof}: \text{values} \rightarrow \text{values}. In other words, we can define another relation R' on \text{values} that is order isomorphic to R. This supports the statement “values are objects in Julia”. (Though I would probably formalise that statement as “values are isomorphic to objects in Julia”.) So contrary to previous comments, we do not need the product structure to construct R. However, I think it is useful to leave the product structure in as it allows us to make the connection with <:. To demonstrate, consider the following quote from the manual (Types · The Julia Language):
When the type is abstract, it suffices for the value to be implemented by a concrete type that is a subtype of the abstract type.
In the present formalisation, I believe this translates as: for arbitrary object x = t_x \times v_x and abstract type y = t_y \times v_y, if t_x < v_y, then x is an instance of y. I assume that this can be strengthened to the
Definition: Object x is an instance of the abstract type y if, and only if, the concrete type t_x of x and the value v_y of y satisfy t_x <: v_y.
Thus, for example, Any is an instance of itself since
julia> typeof(Any)
DataType
julia> DataType <: Any
true
Are there any objections to the following?
Definition: Object x is an instance of the abstract type y if, and only if, the concrete type t_x of x and the value v_y of y satisfy t_x <: v_y.
For instance, Type is an instance of itself because
julia> typeof(Type)
UnionAll
julia> UnionAll <: Type
true
But UnionAll is not an instance of itself
julia> typeof(UnionAll)
DataType
julia> DataType <: UnionAll
false
Indeed, via the same argument, no type in the chain (Int64, Signed, Integer, Real, Number) is an instance of itself.
Whilst I am comfortable with the above, the Ptr doesn’t seem to fit the bill: according to the manual it has “instances” such as Ptr{Int64} and Ptr{Float64}, but
julia> typeof(Ptr{Float64})
DataType
julia> DataType <: Ptr
false
But a closer look at Ptr also shows that <: is not recoverable from subtypes:
julia> subtypes(Ptr)
Type[]
julia> Ptr{Float64} <: Ptr
true
But this section of the manual is factually incorrect because it also states:
And of course, all specific pointer types are subtypes of the umbrella
Ptrtype:
The function supertypes also disagrees with <: here since
julia> supertypes(Ptr{Float64})
(Ptr{Float64}, Ref{Float64}, Any)
julia> supertypes(Ptr)
(Ptr, Ref{T} where T, Any)
Personally, I would settle for the definition at the top of this post: it is clear as daylight.
I don’t understand what that means.
For example, x = \text{int64} \times 1 is just a mathematical formalisation of 1::Int64. Then v_x= 1 and t_x = \text{Int64}. (I only put the type tag on the left because that’s how it appears in the image below.)
For types, which, as the manual says, are also values, v_x is just the name of x. For example, the value of Any is Any, but the concrete type tag of Any is Datatype. So, in this formalisation, if y is the object Any, then y = \text{DataType} \times \text{Any}, so that v_y = \text{Any} and t_y = \text{DataType}.
I think the definition is logically sound. But, I am confused about the definition of abstract types. On the one hand the manual (and other sources) say that abstract types cannot be instantiated. On the other, the manual also says of singleton types:
For each type, T, the “singleton type” Type{T} is an abstract type whose only instance is the object T.
According to my definition, T is not an instance of Type{T} since
julia> typeof(Int64)
DataType
julia> DataType <: Type{Int64}
false
For real clarity, I would like to change the definition to say indirect instance instead of instance. But then it seems weird to say that Type is an indirect instance of itself, which it is since:
julia> typeof(Type)
UnionAll
julia> UnionAll <: Type
true
I’m now looking for is a precise definition of abstract type in the context of Julia. Is it simply one that has been created via a line like the following?
julia> abstract type Foo end
Or can “abstract” be a derived property? So, we can deduce that y is abstract because it cannot be instantiated?
I would also need a precise definition of instantiation. Is it the following object-oriented programming definition?
an instance is a concrete occurrence of any object, existing usually during the runtime of a computer program.
I think an appropriate definition of abstract is one that is complementary to concrete. For then a type y is concrete if, and only if, there exists an object x such that its concrete type \text{typeof}(x) is equal to y. For example,
julia> x = [1.0]
1-element Array{Float64,1}:
1.0
julia> y = Array{Float64,1}
Array{Float64,1}
julia> typeof(x) == y
true
Then, since there is no x such that \text{typeof}(x) = \text{Array}, Array is an abstract parametric type. Ptr is the same.
So then, in line with the manual, Abstract types (such as singleton types and abstract parametric types) may have instances but not “instantiations”. This almost rescues my definition because instances of abstract types are allowed even though instantiations are not!
But, in the end, I think the singleton types example means that I have to weaken the definition slightly
We arrive at:
Definition : Object x is an instance of the abstract type y if, and only if,
isa)