# 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:** 20\
**Page:** 2

<div class="post-metadata">

**Author:** ![goretkin](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/goretkin/32/167_2.png) [@goretkin](https://discourse.julialang.org/u/goretkin)\
**Post date:** [March 12, 2021, 1:23am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/21 "2021-03-12T01:23:42Z")

</div>

> [@path-doc](#):
>
> You will note that on [Types · The Julia Language](https://docs.julialang.org/en/v1/manual/types/), 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](https://github.com/JuliaLang/julia/blob/master/doc/src/manual/types.md)

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

---

<div class="post-metadata">

**Author:** ![liuyxpp](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/liuyxpp/32/9870_2.png) [@liuyxpp](https://discourse.julialang.org/u/liuyxpp)\
**Post date:** [March 12, 2021, 1:27am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/22 "2021-03-12T01:27:02Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![goretkin](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/goretkin/32/167_2.png) [@goretkin](https://discourse.julialang.org/u/goretkin)\
**Post date:** [March 12, 2021, 1:28am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/23 "2021-03-12T01:28:00Z")

</div>

> [@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
julia> sin
sin (generic function with 13 methods)

julia> typeof(sin)
typeof(sin)

julia> typeof(typeof(sin))
DataType

```

---

<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 12, 2021, 1:39am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/24 "2021-03-12T01:39:30Z")

</div>

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

---

<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 12, 2021, 2:11am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/25 "2021-03-12T02:11:47Z")

</div>

> [@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).

---

<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 12, 2021, 2:42am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/26 "2021-03-12T02:42:11Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![goretkin](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/goretkin/32/167_2.png) [@goretkin](https://discourse.julialang.org/u/goretkin)\
**Post date:** [March 12, 2021, 2:50am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/27 "2021-03-12T02:50:18Z")

</div>

> [@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
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
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`.

---

<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 12, 2021, 2:59am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/28 "2021-03-12T02:59:05Z")

</div>

> [@goretkin](#):
>
> ```julia
> 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
> 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.)

---

<div class="post-metadata">

**Author:** ![goretkin](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/goretkin/32/167_2.png) [@goretkin](https://discourse.julialang.org/u/goretkin)\
**Post date:** [March 12, 2021, 3:21am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/29 "2021-03-12T03:21:17Z")

</div>

> [@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.

---

<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 12, 2021, 3:48am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/30 "2021-03-12T03:48:41Z")

</div>

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
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
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
julia> x isa typeof(x)
true

```

---

<div class="post-metadata">

**Author:** ![goretkin](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/goretkin/32/167_2.png) [@goretkin](https://discourse.julialang.org/u/goretkin)\
**Post date:** [March 12, 2021, 4:34am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/31 "2021-03-12T04:34:28Z")

</div>

> [@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
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
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 `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.

---

<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 12, 2021, 4:36am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/32 "2021-03-12T04:36:32Z")

</div>

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
> julia> x isa typeof(x)
> true
> 
> ```

---

<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 12, 2021, 4:37am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/33 "2021-03-12T04:37:56Z")

</div>

> [@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?

---

<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 12, 2021, 4:49am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/34 "2021-03-12T04:49:23Z")

</div>

> [@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.

---

<div class="post-metadata">

**Author:** ![Tamas\_Papp](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tamas_papp/32/25949_2.png) [@Tamas\_Papp](https://discourse.julialang.org/u/Tamas_Papp)\
**Post date:** [March 12, 2021, 5:52am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/35 "2021-03-12T05:52:41Z")

</div>

> [@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...](https://dl.acm.org/doi/10.1145/3276483)**
>
> Programming languages that support multiple dispatch rely on an expressive notion
> of subtyping to specify method applicability. In these languages, type annotations
> on method declarations are used to select, out of a potentially large set of...

---

<div class="post-metadata">

**Author:** ![goretkin](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/goretkin/32/167_2.png) [@goretkin](https://discourse.julialang.org/u/goretkin)\
**Post date:** [March 12, 2021, 5:54am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/36 "2021-03-12T05:54:54Z")

</div>

> [@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.

---

<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 12, 2021, 7:58am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/37 "2021-03-12T07:58:33Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Sukera](https://avatars.discourse-cdn.com/v4/letter/s/ce7236/32.png) [@Sukera](https://discourse.julialang.org/u/Sukera)\
**Post date:** [March 12, 2021, 8:00am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/38 "2021-03-12T08:00:05Z")

</div>

For the most comprehensive talk about the type system:

[![](https://global.discourse-cdn.com/julialang/original/3X/4/9/492c9aff3d96076d5a907e1e76178ed47a4e7de8.jpeg "JuliaCon 2017 | The State of the Type System | Jeff Bezanson") ](https://www.youtube.com/watch?v=Z2LtJUe1q8c)

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

---

<div class="post-metadata">

**Author:** ![Sukera](https://avatars.discourse-cdn.com/v4/letter/s/ce7236/32.png) [@Sukera](https://discourse.julialang.org/u/Sukera)\
**Post date:** [March 12, 2021, 8:08am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/39 "2021-03-12T08:08:28Z")

</div>

> [@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](https://docs.julialang.org/en/v1/manual/types/#Operations-on-Types), the relevant implementation for these builtins can be found [here](https://github.com/JuliaLang/julia/blob/master/src/builtins.c). In particular, `isa` is implemented [here](https://github.com/JuliaLang/julia/blob/c9c1d3e56c958d8d6985261705731c733bed6bdd/src/subtype.c#L2020).

---

<div class="post-metadata">

**Author:** ![zdenek\_hurak](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/zdenek_hurak/32/53118_2.png) [@zdenek\_hurak](https://discourse.julialang.org/u/zdenek_hurak)\
**Post date:** [March 12, 2021, 8:32am UTC](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325/40 "2021-03-12T08:32:35Z")

</div>

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

[Previous page](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325.md?page=1)

[Next page](https://discourse.julialang.org/t/what-is-difference-between-type-t-and-t/19325.md?page=3)
