About the type constraint of `where`

This post was originally asked at 参数化方法的疑问 - 语言特性及语义 - Julia中文社区

Based on the doc at Methods · The Julia Language :

julia> function myappend(v::Vector{T}, x::T) where {T}
           return [v..., x]
       end
myappend (generic function with 1 method)

The type parameter T in this example ensures that the added element x is a subtype of the existing eltype of the vector v
The where keyword introduces a list of those constraints after the method signature definition.

But what exactly are those constraints?

At first thought, I expect the second T should be the subtype of the first T. But based on my experiment with the following definition:

julia> function myappend(x::T,v::Vector{T}) where {T}
          return [v..., x]
  end

julia> myappend(true, Real[1, 2.0])
3-element Vector{Float64}:
 1.0
 2.0
 1.0

It seems that we do not have such constraint in the order.
So now I’m also feeling confused :smiling_face_with_tear:

1 Like

So myappend(true,Real[1, 2.0]) is equal to myappend(1,Real[1,2.0])

which is constrain by function myappend(x::T,v::Vector{T}) where {T} with T being equal to Real.

oh! The order does not matter. As long as T can be equal to a Type.

1 Like

Thats because Bool is a subtype of Real so the constraint is fulfilled.
Also, you’re constructing a new vector and the type promotion between bool and float yiels flots, that’s why you got a float vector back.

julia> supertype(Bool)
Integer

julia> supertype(Integer)
Real

julia> true isa Real
true

If you put in a Float64 vector in the first place, the code fails.

julia> myappend(true, Float64[1, 2.0])
ERROR: MethodError: no method matching myappend(::Bool, ::Vector{Float64})
The function `myappend` exists, but no method is defined for this combination of argument types.

Closest candidates are:
  myappend(::T, ::Vector{T}) where T
   @ Main REPL[4]:1

Stacktrace:
 [1] top-level scope
   @ REPL[5]:1
 [2] top-level scope
   @ none:1
2 Likes

OK, that’s it! So basically here Julia will try to promote the type T of both arguments and see if it can find a common type (either concrete or abstract), right?

No its not really promoting, its checking the signature with actual runtime types and sees if that is valid.

Based on the second argument, it is clear that T must be Real. So, in this case, it needs to check whether your other argument is Real, which makes it a valid signature. However, there is no “searching” for a suitable type in the type hierarchy. For example

function foo(x::T, b::T) where {T}
    return T
end

errors for foo(1, true) because one argument requires T to be Bool and one argument requires T to be Int64, which is invalid.

I think one level of confusion here is that values never can have abstract types. However, you can have a container of abstract types Vector{AbstractType}, which can hold different objects as long as each of them isa AbstractType.

1 Like

Indeed, the following code:

function foo(x::T, b::T) where {T}
    return T
end

requires two variables x and b to have the exact same type T, or it will fail. However, the code

function myappend(v::Vector{T}, x::T) where {T}
      return [v..., x]
end

does not follow this rule. What are the reasons behind this?

1 Like

From https://benchung.github.io/papers/jlsub.pdf:

Being able to dispatch on whether two values have the same type is useful in practice, and the Julia subtype algorithm is extended with the so-called diagonal rule [The Julia Language 2018]. A variable is said to be in covariant position if only Tuple, Union, and UnionAll type constructors occur between an occurrence of the variable and the where construct that introduces it. The diagonal rule states that if a variable occurs more than once in covariant position, and never in invariant position, then it is restricted to ranging over only concrete types. In the type Tuple{T, T} where T <: Number the
variable T is diagonal: this precludes it getting assigned the type Union{Int, Float} and matching the value (3,3.0). Observe that in the type Tuple{Ref{T}, T, T} where T the variable T occurs twice in covariant position, but also occurs in invariant position inside Ref{T}; the variable T is not considered diagonal because it is unambiguously determined by the subtyping algorithm.

(note from myself: the last sentence explains that (Ref{Real}(5), 2.0, 2.0) isa Tuple{Ref{T}, T, T} where T is considered true in Julia subtyping rules.

1 Like

You’re mixing up the types in dispatch and the default element type promotion of array instantiation, which occur separately:

julia> function myappend(x::T, v::Vector{T}) where {T} # dispatch
         @info T, typeof(v), typeof(x)
         [v..., x] # array instantiation, element type promotion
       end
myappend (generic function with 1 method)

julia> myappend(true, Real[1, 2.0])
[ Info: (Real, Vector{Real}, Bool)
3-element Vector{Float64}:
 1.0
 2.0
 1.0

The function call was dispatched to the most fitting (and only) method. The static parameter T was inferred to be Real, as you provided v isa Vector{Real} and true isa Bool <: Real.

When you instantiated the result vector, you splat the elements of v and x, which are 1, 2.0, true. By default, array instantiation tries to promote numbers to one concrete type; in this case Float64, so 1 becomes 1.0, 2.0 stays, true becomes 1.0. Note that the promoted type is NOT a supertype of all the original types; Float64 is not a supertype of Int64 or Bool.

Again, these are two independent events, and method dispatch doesn’t promote types. The automatic promotion in the array instantiation wasn’t necessary either, you could have designated the static parameter as the element type of the array. The elements are unchanged:

julia> function ourappend(x::T, v::Vector{T}) where {T} # dispatch
         @info T, typeof(v), typeof(x)
         T[v..., x] # array instantiation, no promotion
       end
ourappend (generic function with 1 method)

julia> ourappend(true, Real[1, 2.0])
[ Info: (Real, Vector{Real}, Bool)
3-element Vector{Real}:
    1
    2.0
 true
3 Likes

The signature is a Tuple. In the first case the signature is Tuple{T,T} where T so that

julia> (1, 1) isa Tuple{T,T} where T
true

julia> (1, 1.0) isa Tuple{T,T} where T
false

julia> (1, [1.0]) isa Tuple{T,Vector{T}} where T
false

julia> (1, Real[1.0]) isa Tuple{T,Vector{T}} where T
true

In the last example, T is Real, and since the Tuple arguments are covariant it succeeds becase 1 isa Real.

In the third example, the second argument is a Vector{Float64}, so T must be Float64, and 1 is not a Float64.

The second example might seem surprising, one could match it with T === Real, but there is a rule, the diagonal rule, which says that if T occurs in more than one covariant position (i.e. in Tuple or Union), it must be a concrete type. And 1 and 1.0 is not the same concrete type. In the last example, T only occurs once in a covariant position (since Vector{T} is invariant).

3 Likes