type system revision and new subtype algorithm

[JeffBezanson]

This implements the plan in #8974. It is now working well enough to build a system image and get a REPL, albeit with inference disabled. I have some demos.

In the internals there are "only" three changes:

• Types are explicitly quantified by wrapping in UnionAll types, which have two fields: a TypeVar and a type body:

julia> Array
Array{T,N} where N where T

• Union types now have two fields, pointing to two types to union together (instead of an svec of types). This is just a representation change.
• There is a new algorithm for computing the subtype relation. It gives drastically more meaningful results, and will replace the code for subtype and intersection in jltypes.c with a significant net code deletion. Working examples:

julia> Tuple{Union{Int,String}} <: Union{Tuple{Int},Tuple{String}}
true

julia> NTuple <: Tuple, Tuple <: NTuple
(true,false)

The second one is issue #18450.

UnionAll types nest arbitrarily, and the signatures of methods with static parameters are UnionAll types, so we now have "triangular" dispatch:

julia> f{T<:Real, A<:AbstractArray{T}}(x::T, y::Vector{A}) = 0
f (generic function with 1 method)

julia> f(1.0f0, [rand(4,4)])
ERROR: MethodError: no method matching f(::Float32, 
 in eval(::Module, ::Any) at ./boot.jl:235SYSTEM: show(lasterr) caused an error

julia> f(1.0f0, [rand(Float32, 4,4)])
0

(Clearly showing the method error isn't working, but that should just be a matter of updating the showing and reflection code in Base.)

The next steps are to get inference working and then fully replace intersection and morespecific with implementations based on the new algorithm.

Edit: Fixes #19159 #18892 #18450 #18348 #17943 #16922 #13165 #12596 #11803 #8915 #8625 #6721 #2552

[vtjnash]

❤️
(can now get rid of this function, those comments, and rip out useenv entirely :)

[TotalVerb]

Theoretically, any tuple is NTuple{N, Any} for some value of N, so why shouldn't Tuple <: NTuple?

Nevertheless, this is incredible. 👍

[StefanKarpinski]

I'm a bit confused by Tuple{Union{Int,String}} <: Union{Tuple{Int},Tuple{String}} being true. Aren't instances of the LHS any tuples of Ints and Strings while instances of the RHS are tuples of Ints or tuples of Strings but not mixes of both? Shouldn't the inclusion be the other way around?

[johnmyleswhite]

I thought Tuple{Union{Int,String}} means either Tuple{Int} or Tuple{String} since there's exactly one element.

[StefanKarpinski]

Ah, yes. I was forgetting how the new Tuple type syntax works. Thanks, @johnmyleswhite.

[StefanKarpinski]

(I was thinking of Tuple as a hypothetical TTuple type that's like NTuple but with N and T in reverse order.)

[tbreloff]

so we now have "triangular" dispatch

Oh snap! Flashback to my giddy excitement during your JuliaCon 2015 talk :)

[JeffBezanson]

@TotalVerb Good point. !(Tuple <: NTuple) is caused by the "diagonal rule". For example a method f{T}(x::T...) only matches arguments that are all of the same concrete type, so it is not the same as f(x::Any...). The type system models this by saying that certain type vars only range over concrete types.

From there, we have two choices:

1. Disallow NTuple{N, Any}. Since the second parameter can only range over concrete types, substituting Any is not valid.
2. Allow it, meaning the property U{T} <: U does not hold.

We currently pick (2). While U{T} <: U intuitively seems like it should be true, in practice I don't believe we actually need this property for anything.

[TotalVerb]

Ah. So the current rule for function dispatch, that typevars in covariant position only range over concrete types, will be applied to type calculations too? It is certainly nice that this will be made more consistent than it is presently:

julia> test{T}(::Vararg{T,2}) = T
test (generic function with 1 method)

julia> test(1,1.0)
ERROR: MethodError: no method matching test(::Int64, ::Float64)
Closest candidates are:
  test{T}(::T...) at REPL[128]:1

julia> typeof(test).name.mt.defs.sig
Tuple{#test,Vararg{T,2}}

julia> isa((test,1,1.0), ans)
true

!(U{T} <: U) is certainly unintuitive, but I also don't think it's a huge loss. This is already the case with Union, and as far as I can tell will only be the case with things typealiased to Tuple (as no other type is covariant).

[JeffBezanson]

will be applied to type calculations too?

Yes. That certain typevars range over concrete types is now just a structural property of types, to be followed by all type operations.

[timholy]

flip argument order?

[JeffBezanson]

The underscore means you're not allowed to complain about it :)

[timholy]

OK 😄

[tkelman]

There's some performance we need to claw back, looks like this added about 10 minutes to the test time on appveyor. Probably comparable on Travis.