# A Question on the Type System: Concrete Types, Super-Types and Type Intersections

**URL:** <https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869>\
**Category:** Internals & Design\
**Tags:** jump, type\
**Created:** [July 29, 2020, 11:34am UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869 "2020-07-29T11:34:00Z")\
**Posts on this page:** 12\
**Page:** 1

<div class="post-metadata">

**Author:** ![barankarakus](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/barankarakus/32/15938_2.png) [@barankarakus](https://discourse.julialang.org/u/barankarakus)\
**Post date:** [July 29, 2020, 11:34am UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/1 "2020-07-29T11:34:00Z")

</div>

Hi,

I have a quick question on the type system of Julia.

My mental model of a type is simply a set of values. We can say a value v is an instance of a type T if v is in the set T. We can also say a type T is a super-type of a type S if T contains the set S.

But Julia also enforces that every value v is an instance of a concrete type C.

Now, my question is this:

If v is an instance of T, must T be a super-type of C?

In other words, if C is a concrete type and (T intersection C) is non-empty, must T be a super-type of T (edit: I mean ‘must T be a super-type of C’)? This is clearly false for C an abstract type: A counterexample is C = Union{TypeA, TypeB} and T = TypeA.

If this is not true, then is it at least true that two different concrete types must have empty intersection? This seems to me like it should be true: If not, there would be ambiguity as to what type the typeof function should return when passed values in this intersection.

A third question: Is there a complete, rigorous description of the type system somewhere? I’m looking for something that’s as axiomatic as possible. For example, two axioms of the type system appear to be: 1. Every value is an instance of a concrete type, 2. Concrete types cannot sub-type one another. But these axioms leave open the possibility that two concrete types have non-empty intersection - this is what I’m trying to clarify in my second question, above.

Thanks!

---

<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:** [July 29, 2020, 11:55am UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/2 "2020-07-29T11:55:58Z")

</div>

> [@barankarakus](#):
>
> If v is an instance of T, must T be a super-type of C?

Effectively, are you asking if a \in T, a \in C implies C \subseteq T? It doesn’t.

> [@barankarakus](#):
>
> must T be a super-type of T?

No, in Julia types are not their own supertypes.

> [@barankarakus](#):
>
> two different concrete types must have empty intersection?

Yes, this is correct.

> [@barankarakus](#):
>
> Is there a complete, rigorous description of the type system somewhere? I’m looking for something that’s as axiomatic as possible. For example, two axioms of the type system appear to be: 1. Every value is an instance of a concrete type, 2. Concrete types cannot sub-type one another. But these axioms leave open the possibility that two concrete types have non-empty intersection - this is what I’m trying to clarify in my second question, above.

Not that I am aware of (but the code may of course qualify as a rigorous description, just not in the language of math).

Generally an axiomatic approach is not needed, it would be a lot of notation for little insight as the type system is pretty intuitive conceptually. But if you insist on creating one, keep _parametric types_ in mind, they complicate the picture a bit as technically Julia does not consider the `UnionAll` a supertype, eg

```julia
julia> Rational{Int} <: Rational
true

julia> supertype(Rational{Int})
Real

```

---

<div class="post-metadata">

**Author:** ![johnmyleswhite](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/johnmyleswhite/32/31_2.png) [@johnmyleswhite](https://discourse.julialang.org/u/johnmyleswhite)\
**Post date:** [July 29, 2020, 12:10pm UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/3 "2020-07-29T12:10:14Z")

</div>

> [@Tamas\_Papp](#):
>
> No, in Julia types are not their own supertypes.

I think this isn’t strictly true: `supertype(Any) === Any`.

---

<div class="post-metadata">

**Author:** ![johnmyleswhite](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/johnmyleswhite/32/31_2.png) [@johnmyleswhite](https://discourse.julialang.org/u/johnmyleswhite)\
**Post date:** [July 29, 2020, 12:10pm UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/4 "2020-07-29T12:10:31Z")

</div>

If you want a PL approach to the type system, I recommend [http://janvitek.org/pubs/oopsla18a.pdf](http://janvitek.org/pubs/oopsla18a.pdf)

---

<div class="post-metadata">

**Author:** ![barankarakus](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/barankarakus/32/15938_2.png) [@barankarakus](https://discourse.julialang.org/u/barankarakus)\
**Post date:** [July 29, 2020, 3:15pm UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/5 "2020-07-29T15:15:12Z")

</div>

> [@Tamas\_Papp](#):
>
> > [@barankarakus](#):
> >
> > If v is an instance of T, must T be a super-type of C?
> 
> Effectively, are you asking if a \in T, a \in C implies C \subseteq T? It doesn’t.

Would you be able to provide a counterexample?

> [@Tamas\_Papp](#):
>
> > [@barankarakus](#):
> >
> > must T be a super-type of T?
> 
> No, in Julia types are not their own supertypes.

Apologies, I meant to ask “if C is a concrete type and (T intersection C) is non-empty, must T be a super-type of C?”.

---

<div class="post-metadata">

**Author:** ![barankarakus](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/barankarakus/32/15938_2.png) [@barankarakus](https://discourse.julialang.org/u/barankarakus)\
**Post date:** [July 29, 2020, 3:15pm UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/6 "2020-07-29T15:15:48Z")

</div>

Fab, thanks!

---

<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:** [July 29, 2020, 3:26pm UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/7 "2020-07-29T15:26:20Z")

</div>

> [@barankarakus](#):
>
> > [@Tamas\_Papp](#):
> >
> > Effectively, are you asking if a \in T, a \in C implies C \subseteq T? It doesn’t.
> 
> Would you be able to provide a counterexample?

a = 1, C = \{ 1, 2 \}, T = \{1, 3\}.

---

<div class="post-metadata">

**Author:** ![barankarakus](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/barankarakus/32/15938_2.png) [@barankarakus](https://discourse.julialang.org/u/barankarakus)\
**Post date:** [July 29, 2020, 3:27pm UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/8 "2020-07-29T15:27:41Z")

</div>

But is it possible to define a concrete type C whose values are ONLY 1 and 2, and another type T whose values are ONLY 1 and 3?

---

<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:** [July 29, 2020, 3:32pm UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/9 "2020-07-29T15:32:50Z")

</div>

Sorry, I don’t understand your question; `typeof(1) === Int`.

Generally, each value has one type, ie `typeof` is a function.

---

<div class="post-metadata">

**Author:** ![barankarakus](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/barankarakus/32/15938_2.png) [@barankarakus](https://discourse.julialang.org/u/barankarakus)\
**Post date:** [July 29, 2020, 3:35pm UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/10 "2020-07-29T15:35:36Z")

</div>

Apologies, I’ll state it more clearly:

If C is a concrete type, and T is another type (concrete/abstract/whatever), and the intersection of T and C is non-empty, must we necessarily have that T is a super-type of C?

Of course, it is easy to come up with sets T and C such that this is not true. But types cannot be arbitrary sets of values.

---

<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:** [July 29, 2020, 3:43pm UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/11 "2020-07-29T15:43:59Z")

</div>

> [@barankarakus](#):
>
> If C is a concrete type, and T is another type (concrete/abstract/whatever), and the intersection of T and C is non-empty, must we necessarily have that T is a super-type of C?

I think yes, in the sense that `isconcretetype(C) && x isa C && x isa T` implies `C <: T`.

---

<div class="post-metadata">

**Author:** ![barankarakus](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/barankarakus/32/15938_2.png) [@barankarakus](https://discourse.julialang.org/u/barankarakus)\
**Post date:** [July 29, 2020, 3:47pm UTC](https://discourse.julialang.org/t/a-question-on-the-type-system-concrete-types-super-types-and-type-intersections/43869/12 "2020-07-29T15:47:01Z")

</div>

Ah okay, brilliant! Thanks.

The reason I was wondering whether or not this is true is that it would be nice to say that a value’s concrete type is the node on the type graph such that every type for which that value is an instance is a super-type of this node (i.e. ‘a parent of’ this node).