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 https://dl.acm.org/doi/10.1145/3276483) 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 https://dl.acm.org/doi/10.1145/3276483.

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 https://dl.acm.org/doi/10.1145/3276483, `<:`

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
```