What is a unionall type?


#1

What is a unionall type?


#2

See


#3

UnionAll isn’t actually part of the system right now (the closest approximation is the TypeConstructor object that you can create via a typealias), which is why the system makes type inference and dispatch mistakes in some cases. A UnionAll type will allow the type system to make concrete statements about the meaning of a TypeVar inside a parameterized DataType. The pull request to add this documents it https://github.com/JuliaLang/julia/pull/18457/files#diff-644af0d842466925732f9d7271836363R76. I’ll try to unpack this description some:

Any DataType is a concrete type. Unless it is abstract, then it couldn’t have any subtypes, and we can make an instance of this. In order to represent a set of parameterized types, a UnionAll must be added to indicate that it represents a set of types. The UnionAll is a logic expression that means the type represents a set of related DataTypes. For example, when we write Array, this type is describing the union of all array types that are parameterized by its two type parameters (T and N). Those parameters are TypeVar's, which means that they are essentially placeholders variables which can be filled in with an actual value to construct a subtype. The UnionAll bound documents how these variables may be matched and filled in when they appear multiple times. This UnionAll will let the type system distinguish between two cases:
Array{Complex{T}, 1} where T vs. Array{Complex{T} where T, 1}
(The where T is the proposed syntax for constructing a UnionAll.)
In the former case, this type describes the set of all arrays that contain a complex number parameterized by T. In the latter case, this expression describes the single array type that contain any type of complex number. The latter case is a subtype of the former.

I hope this helps! I’m excited to see this addition to the system, since it will allow users to write down more precise type parameterizations, and so the type system will be correct (making type-inference more reliable).


#4

This is very interesting, thank you.

At the moment (v0.5) we could also dispatch on a subtype of Array{T,1} where T <: Complex, and the concrete vector type which can hold any complex number would be Array{Complex{Any},1}.

Am I guessing the type you wrote, Array{Complex{T} where T, 1) is more flexible, in that we might want Array{Complex{T},1} where T<:Union{Float64,Float32} for example? At the moment I could write Array{T,1} where T <: Union{Complex{Float64},Complex{Float32}} but I guess the new syntax is much more succinct and to the point, and additionally it automatically fills in the missing abstract type, so it effectively allows T <: Union{Complex{Float64}, Complex{Float32}, Complex{Union{Float64, Float32}}}?

EDIT: I think I overcomplicated the above… but I am beginning to appreciate the subtleties

Any DataType is a concrete type

So, is there a convenient way of constructing and maintaining a binding to an abstract type? E.g. AbstractFloat(1.0) just returns Float64, not an AbstractFloat box. The system seems to do its best to not let you use such a box - and while I do understand the box is used internally, this isn’t exactly user controlled.

EDIT: ANY being the only way I know of, whereas ANY{T} where T might be a better model of an abstract box at the Julia language level.


#5

the concrete vector type which can hold any complex number would be Array{Complex{Any},1}.

Semantic precision becomes necessary here. That Array can only hold instances of the Complex{Any} type. Whereas Array{Complex, 1} can hold instances of any subtype of Complex. Note that Complex is type equal to Complex{T} where T (meaning they are the same type). So it is the same expression as it is today, but the nesting semantics today are ambiguous, which can lead to erroneous type computations during inference and dispatch.

So, is there a convenient way of constructing and maintaining a binding to an abstract type

No, leaftypes are not permitted to have subtypes (which does answer your question, just in reverse).

ANY being the only way I know of, whereas ANY{T} where T might be a better model of an abstract box at the Julia language level.

I’m not sure what this is supposed to mean. There is a TypeVar in the system named ANY, which is type equal to Any, but which dispatch can detect as a user hint to avoid compiling a method specialization on that argument. A TypeVar cannot be parameterized by another TypeVar, so that specification isn’t particularly meaningful.


#6

Right - I got myself in a muddle in my last post. It seems clear that the new system should be easier to comprehend.

With regard to ANY, I think I was really looking for more control over how things dispatch. For instance if ANY = T where T<:Any then I might consider ANYFLOAT = T where T<:AbstractFloat. So it would be a method that dispatches only on AbstractFloat (because that is the only case the generic method makes sense, and maybe there are other methods) but we don’t want a specialised compilation (compiler overhead being estimated as worse than run time penalty).

Where this is coming from is our previous discussion on improving the performance of Union. Specifically, if we update the internal layout (“box”) for a Union type, then we will be able to use that layout in ccall. Is it useful or desirable to let users create a generic Julia function that can also take advantage of this new kind of box, only specialised for the union rather than each concrete type, in the same way that ANY lets us use the existing box?

Otherwise, to achieve this, users would have to use a wrapper type (an immutable Ref type of container) or call cfunction and ccall. I was wondering if we can fit all of this into the new where syntax or modify ANY to something like typealias ANY{T where T} T such that ANY{Union{A,B}} uses the new box, or something.


#8

How does one check for type-equality?

julia> (Complex{T} where T) == Complex
false

#9
julia> Complex == Complex{T} where {T <: Real}
true

Yeah, Complex is one of those special types that has extra constraints (which I didn’t represent), so it perhaps was not the best choice for the example.


#10

Shouldn’t Complex and Complex{T} where T be equal though?

julia> f(x::Complex) = 1
f (generic function with 1 method)

julia> f(x::Complex{T} where T) = 2
f (generic function with 2 methods)

I don’t think there’s any way of calling the second method.


#11

Julia doesn’t care about that. There’s lots of way to make un-constructable types. A lint program might be created to find and warn about these cases, but it doesn’t matter to the language.


#12

Also note the shorthand syntax Type{<:T}:

Julia-0.6.0> Complex == Complex{<:Real} == Complex{T} where T<:Real
true

Julia-0.6.0> Array == Array{<:Any,<:Any} == Array{T,N} where T where N
true

Julia-0.6.0> Array{Int} == Array{Int,<:Any} == Array{Int,N} where N
true

#13

There’s an open issue somewhere about teaching the system to know that Complex{T} where T actually has an implicitly constrained T because of the definition of Complex, but it’s a future feature and just hasn’t been done yet.