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!