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:
- for every x = t_x \times v_x and y = t_y \times v_y in X, let x \mathbin{Q} y if, and only if, for some sequence of compositions (\text{typeof} \circ \cdots \circ \text{typeof})(v_x) = v_y. Note that \text{typeof} never cycles as per the Appendix of Julia subtyping: a rational reconstruction | Proceedings of the ACM on Programming Languages.
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