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

[barankarakus]

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!

[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

[johnmyleswhite]

@Tamas_Papp

No, in Julia types are not their own supertypes.

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

[johnmyleswhite]

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

[barankarakus]

@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?”.

[barankarakus]

Fab, thanks!

[Tamas_Papp]

@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\}.

[barankarakus]

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?

[Tamas_Papp]

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

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

[barankarakus]

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.

[Tamas_Papp]

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

[barankarakus]

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