# What is difference between Type{T} and T

**URL:** <https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325>\
**Category:** New to Julia\
**Tags:** type, parametric-types\
**Created:** [January 6, 2019, 3:42pm UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325 "2019-01-06T15:42:15Z")\
**Posts on this page:** 1\
**Showing post:** 53

<div class="post-metadata">

**Author:** ![path-doc](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/path-doc/32/19183_2.png) [@path-doc](https://discourse.julialang.org/u/path-doc)\
**Post date:** [March 14, 2021, 7:17am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/53 "2021-03-14T07:17:05Z")

</div>

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](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 [Julia subtyping: a rational reconstruction | Proceedings of the ACM on Programming Languages](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 [Julia subtyping: a rational reconstruction | Proceedings of the ACM on Programming Languages](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](https://docs.julialang.org/en/v1/manual/types/)):

> 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
julia> typeof(Any)
DataType

julia> DataType <: Any
true

```

---

_[View the full topic](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325)._