What is a unionall type?

Tem_Pl · December 4, 2016, 10:36am

Tamas_Papp · December 4, 2016, 3:13pm

See

github.com/JuliaLang/julia

type system design iteration

opened 03:16AM - 11 Nov 14 UTC

closed 05:06PM - 16 Jan 17 UTC

JeffBezanson

types and dispatch

@jakebolewski, @jiahao and I have been thinking through some type system improve…ments and things are starting to materialize. I believe this will consist of: - Use `DataType` to implement tuple types, which will allow for more efficient tuples, and make tuple types less of a special case in various places. This might also open the door for user-defined covariant types in the future. (DONE) - Add `UnionAll` types around all uses of TypeVars. Each `UnionAll` will bind one TypeVar, and we will nest them to allow for triangular dispatch. So far we've experimented with just sticking TypeVars wherever, and it has not really worked. We don't have a great syntax for this yet, but for now will probably use `@UnionAll T<:Int Array{T}`. These are mostly equivalent to existential types. - Unspecialized parametric types will actually be UnionAll types. For example `Complex` will be bound to `@UnionAll T<:Real _Complex{T}` where `_Complex` is an internal type constructor. - Technically, `(Int,String)` could be a subtype of `@UnionAll T (T,T)` if `T` were `Union(Int,String)`, or `Any`. However dispatch doesn't work this way because it's not very useful. We effectively have a rule that if a method parameter `T` only appears in covariant position, it ranges over only concrete types. We should apply this rule explicitly by marking TypeVars as appropriate. So far this is the best way I can think of to model this behavior, but suggestions are sought. - TypeVars should only be compared by identity, and are not types themselves. We will not have syntax for introducing lone TypeVars; `@UnionAll` should suffice. This is being prototyped in `examples/juliatypes.jl`. I hope this will fix most of the following issues: method lookup and sorting issues: #8959 #8915 #7221 #8163 method ambiguity issues: #8652 #8045 #6383 #6190 #6187 #6048 #5460 #5384 #3025 #1631 #270 misc. type system: #8920 #8625 #6984 #6721 #3738 #2552 #8470 In particular, type intersection needs to be trustworthy enough that we can remove the ambiguity warning and generate a runtime error instead.

jameson · December 5, 2016, 2:01am

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 type system revision and new subtype algorithm by JeffBezanson · Pull Request #18457 · JuliaLang/julia · GitHub. 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).

andyferris · December 5, 2016, 3:31am

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.

jameson · December 5, 2016, 7:49am

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.

andyferris · December 5, 2016, 11:46am

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.

cstjean · June 21, 2017, 2:02am

How does one check for type-equality?

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

jameson · June 21, 2017, 2:51am

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.

cstjean · June 21, 2017, 3:21am

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.

jameson · June 21, 2017, 5:16am

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.

greg_plowman · June 21, 2017, 9:09am

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

StefanKarpinski · June 28, 2017, 5:33pm

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.