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

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

@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> Rational{Int} <: Rational
true

julia> supertype(Rational{Int})
Real