Not sure if I should post under Offtopic but anyway…
In Bezanson’s PhD thesis in 2015, he mentions that
Set-theoretic types are a natural basis for such a system. A set-theoretic type is a symbolic expression that denotes a set of values. In our case, these correspond to the sets of values methods are intended to apply to, or the sets of values supported by compiler-generated method specializations.
This is clearly reflected in the design of union types in Julia. We however notice that UnionAll types involve impredicative existential quantification (see e.g. Decidable Subtyping of Existential Types for Julia). Typically impredicative types quantifying over all types are not interpretable set theoretically.
So does Julia’s type system have a set theoretic interpretation?