type system design iteration

[JeffBezanson]

@jakebolewski, @jiahao and I have been thinking through some type system improvements 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.

[Jutho]

+100
and another +100 for the 0.4 milestone.
0.4 will be so great

[timholy]

This will be one heck of an improvement. I'm not sure I fully appreciate your intentions with ForAll, but I'm already eagerly anticipating it.

[StefanKarpinski]

Currently the scoping of the variable in typevars is both vague and limited. By explicitly wrapping them in a universal quantifier – i.e. ForAll – you can address both: the scope becomes explicit and one can therefore do much more sophisticated things.

[toivoh]

This sounds great, but can you elaborate on the part

It turns out that we effectively have a rule that if a method parameter T only appears in covariant position, it is made invariant instead.

When does it apply? Which positions are considered covariant and which invariant? (Are there any contravariant positions?) Is that different in any way from making type parameters always invariant?

[jiahao]

@toivoh the idea was to describe how diagonal dispatch currently works.

Consider:

f{T}(x::T, y::T) = x + y#matches a concrete type like T = Float64 but not an abstract type like T = Real
f{T}(A::Matrix{T}, b::T) = A .+ b #matches both T = Float64 and T = Real in 0.4-dev but only T = Float64 in 0.3

The first method has input signature T. (T, T) but unlike ordinary tuples, only allows for (Float64, Float64), not (Real, Real) even though the former is a subtype of the latter. Therefore tuples in this context do not behave covariantly, but invariantly.

f(3.0, 4.0) #arguments of type (Float64, Float64)
f(3, 4.0) #arguments of type (Int, Float64) <: (Real, Real) but does not match

The second has signature T. (Matrix{T}, T) and is matched invariantly in 0.3, but covariantly in 0.4.

f(zeros(Real, 3, 3), 4.0) #arguments of type (Matrix{Real}, Float64) <: (Matrix{Real}, Real)

The general rules appear to be:

• v0.3: match tuples of input arguments invariantly, always
• v0.4: match tuples of input arguments covariantly, unless the type parameter only appears in a fully covariant context (like (T, T, T, T...)), in which case, match the tuple invariantly.

The v0.4 rule is admittedly strange when written out like that.

[JeffBezanson]

I don't think it's the whole tuple that's matched invariantly, just the typevar. For example f{T}(x::Real, y::T, z::T) still allows any Real as the first argument.

[toivoh]

The new covariant behavior of ::T in e.g. f{T}(A::Matrix{T}, b::T) was news to me, very much appreciated! (I do follow most issues though, has this been discussed anywhere?) As I understand it, before this, type parameters were always considered invariant.

I agree that it's useful to be able to match e.g. f{T}(x::T, y::T) invariantly (or equivalently, force T to be concrete there), but I'm not sure that it's not useful to be able to match it covariantly.

I understand the rule from the point of view that when trying to match a signature against an actual argument tuple, each type parameter can always be bound to a type derived from one of the argument types, and then we check if the other constraints are fulfilled. I also see that this rule would minimize breakage while letting ::T be covariant in cases like f{T}(A::Matrix{T}, b::T).

Still, I'm not quite comfortable with the special casing. It's easier that you unwittingly change a case from covariant to invariant or vice versa, and if you haven't read the manual very carefully, you might not even be aware of the distinction. Could we consider having :: be always covariant even on type parameters, and have another way to get the invariant behavior, like e.g. on of

f{T}(x:::T, y:::T) = x + y
f{T}(x::=T, y::=T) = x + y

This would make it immediately clear to the reader that something different is going on.
The ::: form would be in some kind of analogy with ===, which is stricter than ==.
Or maybe the type parameter T itself could be marked as invariant in some way.

[StefanKarpinski]

I have to admit that I'm not entirely comfortable with the special casing either, although I realize we've been doing something similar for a rather long time. Not sure how else to handle it, although I would mention that if you can dispatch on type paremeters being concrete, then covariance would be a good choice.

[jiahao]

@JeffBezanson @jakebolewski and I have had a followup discussion and we feel that ForAlls is not the right use of ∀ in the sense of universally bounded quantifiers in type theory. Perhaps UnionAll is a better name.

[toivoh]

Thinking about this some more, I realize that it is mostly an issue of consistency rather than functionality. Looking at the prototypical case where a type parameter appears only in covariant position,

f{T}(x::T, y::T) = T

the covariant behavior can be achieved anyway with one of

f{S,T}(x::S, y::T) = Union(S,T)
f{S,T}(x::S, y::T) = typejoin(S,T)

depending on how you want the matching of T to behave. That alone might be reason enough to forbid a type parameter to act covariantly everywhere it is used. It would require to specify a special case behavior, and it feels better require the user to choose explicitly instead. So if we should do this for consistency, I would probably vote to make f{T}(x::T, y::T) an error and require that the user specify that T behave invariantly or use one of the patterns based on f{S,T} above.

We would of course still permit type parameters appearing only once covariantly such as in f{T}(x::T) = T, where both the covariant and invariant behavior would be to set T to the type of x.

When it comes to functionality, the only thing it seems that we stand to lose with the rule is the possibility to let e.g. T work in an invariant manner in f{T}(::Array{T}, ::T). Not sure how big that loss that is.

[toivoh]

One possibility for marking a type parameter as concrete might be to allow something like

f{T::Concrete}(x::T, y::T) = T

I have no idea how much havoc it would wreak in the type system to have all concrete types and no others be instances of Concrete.

It appears that allowing :: relations on type parameters would widen the domain of dispatch even further, allowing to dispatch on the types of type parameters and not just on the types of arguments (meta-dispatch?) I can't say if this is a really bad idea or maybe even useful in other cases than T::Concrete. Of course, marking up a type parameter as concrete could be done with some new special syntax without opening up this Pandora's Box.

One thing to note is that f{T<:Concrete}(x::T, y::T) will not serve to mark T as concrete. I guess it has to be an axiom that if A <: T and B <: T then Union(A, B) <: T, so that would allow T = Union(typeof(x), typeof(y)) above. A union is not a concrete type (right?) in the sense that typeof(x) can never return a union type, so apparently concreteness can not be described by a subtyping relationship. But perhaps by an instance-of relationship.

[eschnett]

It's not just a question of whether T is covariant or invariant, it's also a question of how T is determined at the call site, i.e. how the pattern matching works. In the case of f{T}(::Matrix{T}, ::T}), T may be forced to be an abstract type by the first argument. In the case of f{T}(::T, ::T), there is nothing that would immediately force T to be abstract.

Instead of arguing via covariance or invariance, I would describe Julia's current type matching rule as "match the (implicitly concrete) argument types against the types in the function signature, and deduce type parameters from that". Nothing in type matching is currently looking for supertypes (or unions) of two types to make things match.

Having said this, which is obviously not news to you: @JeffBezanson, are you looking for a way to introduce such a behaviour (automatically looking for supertypes or unions)? If so, what about allowing type arithmetic in function signatures? Or maybe it would be better to extend type pattern descriptors?

What would be the advantage of deducing supertypes or unions? Would it be to prevent specialization of routines? If so, couldn't that be expressed differently, with metadata instead of through the type system, or by analyzing the function body to see whether specialization is beneficial?

[JeffBezanson]

The question is whether a tuple of actual argument types is a subtype of the method signature, so this does reduce to a question of covariance vs. invariance (the argument tuple is covariant).

There wouldn't be any advantage to deducing supertypes or unions; we don't want that. However theory requires them, because (Int,String) is indeed a subtype of forall T . (T,T) if you let T be Union(Int,String). So we need an explanation for why we don't do that. If we did this outside the type system, you wouldn't be able to write down a type for the method that lets you reason about how it can be called, which I think would be unfortunate.

[eschnett]

Thanks for the rationale.

I agree with @toivoh: It would then be necessary to express the notion "T is a concrete type" in the type system, since type matching starts from actual arguments, which are concrete types.