constraints on non-type as type parameters

[yuyichao]

When a type parameter is specified to be T <: Top, it actually accept non-type as parameters as well.

julia> type A{T<:Top}
       end

julia> A{1}
A{1}

julia> A{1.2}
A{1.2}

Although 1 and 1.2 are clearly not subtypes of Top

julia> 1 <: Top
ERROR: type: subtype: expected Type{T<:Top}, got Int64

julia> 1.2 <: Top
ERROR: type: subtype: expected Type{T<:Top}, got Float64

This is also the case for the builtin Type (some other types like Array doesn't even have this constraint specified)

julia> Type
Type{T<:Top}

julia> Type{1}
Type{1}

julia> Type{1.2}
Type{1.2}

No error is raised even if this parameter is used as a type of a field

julia> type A{T<:Top}
       a::T
       end

julia> A{1}
A{1}

julia> A{1}.names
(:a,)

julia> A{1}.types
(1,)

The same thing happens for T <: Any although this time it correctly reject Core.Unref

julia> type A{T <: Any}
       end

julia> A{1}
A{1}

julia> A{1.2}
A{1.2}

julia> A{Core.Undef}
ERROR: type: A: in T, expected T, got Type{Undef}

julia> Core.Undef <: Any
false

Specifying other types seems fine

julia> type C{T <: Integer}
       end

julia> C{1}
ERROR: type: C: in T, expected T<:Integer, got Int64

julia> C{Int}
C{Int64}

Another related issue is that Vararg doesn't specify any constraint on the parameter and therefore the following syntax is allowed.

julia> (1...)[1]
1...

julia> typeof((1...)[1])
DataType

[JeffBezanson]

This is not a high priority, since it doesn't prevent anybody from getting work done.

[yuyichao]

I agree, I couldn't really think of a situation that this can affect the correctness of valid code either. It's only a little bit confusing when I did sth wrong and the error pops up in unrelated place etc...

[vtjnash]

the Top and Undef types are gone now. its unclear to me if type A{T<:Any} end is supposed to mean something different from type A{T} end, which was the remaining odd case observed here.

[toivoh]

Well it would definitely seem reasonable that T would be constrained to be a type in the former case, but I don't know enough about the internals to day whether it would be reasonable to change it to work like that.

[yuyichao]

Yeah, I relized that Top and Undef are gone. However, this issue is about T <: Any (and also T <: Top before) accepting non-type as type parameters.

Conceptually type A{T<:Any} end means A{1} is not allowed.

[yuyichao]

I guess it requires a field in TypeVar to define whether non-type is allowed? Although I guess there's a number of other places that needs to be changes as well.

[yuyichao]

At some point I was also thinking that it might be nice to be able to write sth like

type A{T<:Top, N::Int}
...
end

So that the first parameter has to be a type and the second has to be a Int.

The (only) benefit would be less confusion and less manual checking if one want to be safe but I'm not sure how big a change it requires in the underlying system...

Edit: I am aware that T <: Top is a boolean expression while N::Int is an assertion so it's not that consistent but I guess the meaning should be pretty clear....

[toivoh]

This idea has come up before (a long time ago I believe), I also think that it would be a good addition (and don't know how hard it would be).

[mgkuhn]

As far as I can tell, the Julia documentation does at the moment not explicitly state, what values are permitted as type parameters. All the examples I found show only other types as type parameters. Are e.g. integer values also allowed as type parameters? Any immutable value that can be created at compiler time (e.g. a text string)?

A good practical application example of an integer parameter would be a parametric modular-arithmetic type, where the modulus is compiled into the code, rather than being encoded as a run-time parameter along with each value. Imagine an application that does a lot of modular arithmetic, but only ever with the three fixed modulus values 5, 7 and 17. It would be great to be able to implement that via a single parametric "type Mod{modulus::Int} v::Int; end", which the programmer can then instantiate as types Mod{5}, Mod{7} and Mod{17} and add with "+(x::Mod{N}, y::Mod{N}) = Mod{N}(mod(x.v+y.v, N))"?

At the moment, the latter results in "ERROR: UndefVarError: N not defined".

[mbauman]

Please ask questions about usage on our discourse message board.

For documentation, see the first section of the page you linked, the last bullet point. Integers as type parameters are fully supported and frequently used. That's how we encode the dimensionality in our arrays. In fact, your exact example is in the examples/ folder.

The thing you're running into is that Julia does not support isa (::) restrictions within type parameter lists. Only subtype (<:) expressions are currently supported. But this is unrelated to this issue. If you have further questions, please continue the discussion on the message board.

[grahamas]

@yuyichao Could another benefit of the N::Int syntax be expressions like:

const PlusTwoD{T,N::Int} = Array{T,N+2}

I'm not sure that deserves its own feature request separate from this, but it is a feature I would find useful for writing more readable code. One simple example would be for making space-time arrays, since there's always a single implicit time dimension but any number of space dimensions, and I want to have SpaceTime{SpaceDimensionality} correspond directly to a timeseries of Space{SpaceDimensionality}.

edit: Though then what would PlusTwoD{Int,3}.parameters return? Maybe this is a separate (if dependent) request?

[yuyichao]

The implementable subset of it is #18466

[philtomson]

What was the ultimate outcome here? Are non-type parameters still under consideration or not?

[mbauman]

Non-type parameters are fully supported and always will be. They simply must be isbits. See the fourth bullet point in the documentation for types.

This issue is about "abusing" the syntax T<:Any in type parameters — that currently means that they're completely unrestricted and also allow non-type values, but ideally it'd require a subtype relation like it does everywhere else.

[philtomson]

Ok, the way I ended up here was that I was trying to parametize a struct based on a UInt8 value, something like this:

julia> mutable struct NDimArray{N::UInt8}
    arry::Array{Int64, N}
end
ERROR: syntax: invalid variable expression in "where"

(I guess I was taking a bit too much inspiration from C++ non-type template params where you have to specify the type)

Just now I tried not specifying the type of N:

julia> mutable struct NDimArray{N}
          arry::Array{Int64, N}
       end

That seemed to work, though it doesn't convey the constraint that N should be a unsigned integer of some sort.

Also, can that non-type parameter 'N' be used in an inner constructor inside the struct definition?

EDIT: yes that seems to be possible:

julia> mutable struct NDimArray{N}
          arry::Array{Int64, N}

          NDimArray{N}(i::Integer) where {N} = new([N*i])
       end

but the 'where' seems a bit odd there.

[mbauman]

Right, we currently don't support :: constraints within type parameters, but you can use non-type parameters everywhere — including in inner constructors that can enforce your constraints at construction time. Further questions here would probably be better suited for the discourse mailing list.

[brenhinkeller]

This issue seems to have become a placeholder for the general idea of allowing additional constraints on non-types as type parameters, but FWIW it looks like the original complaints are all fixed now:

julia> struct A{T<:AbstractFloat} end

julia> A{Float64}
A{Float64}

julia> A{1}
ERROR: TypeError: in A, in T, expected T<:AbstractFloat, got a value of type Int64
Stacktrace:
 [1] top-level scope
   @ REPL[50]:1

julia> A{1.2}
ERROR: TypeError: in A, in T, expected T<:AbstractFloat, got a value of type Float64
Stacktrace:
 [1] top-level scope
   @ REPL[51]:1

julia> (1...)[1]
1

[vtjnash]

Fair enough that we don't really need this issue to know about the general idea of wanting to express constraints on values used in type parameters

[nsajko]

This was closed by mistake, the issue of <:Any not requiring subtyping, as pointed out in the OP and comments above, remains.

Also, the title is misleadingly ambiguous, perhaps it should be changed to something like "<:Any constraint doesn't require subtyping, having no effect". Otherwise people will keep thinking this issue is about "wanting to express constraints on values used in type parameters".

[nsajko]

Furthermore, the same is true of UnionAll constraints like in this type definition:

struct S{T <: (AnyType where {AnyType})} end

Sadly this behaves as if there's no constraint, while the expected behavior would be to require that T be a type.

So it seems there's currently no workaround.

[vtjnash]

We do not parse variable names, so AnyType<:Any is not different from Any, even with the change to the name, and is still representative of the supertype of all values of any kind

[vtjnash]

This issue was about fixing the root of the type system, so that it is Any, and not some other object. Your solution to this issue cannot be to reintroduce the problem that was fixed in order to close it.

[StefanKarpinski]

How about changing an explicit T <: Any to require a type rather than allowing values as type parameters and then also implement n :: Int to constrain the type of a value parameter? I get that we haven't implemented that yet because it's work, but surely we want to have those features at some point, as well as checking that type parameters actually respect bounds when we construct types.

[vtjnash]

That would likely be spelled T :: Type once that is implemented, so there is not a need for a large, breaking change to the meaning of Any back to Top

[nsajko]

a large, breaking change to the meaning of Any back to Top

You completely misunderstood the proposal, the intent behind is precisely to avoid large breaking changes by adding another abstract type.

[frankwswang]

I think whatever the final solution is, it's better to reopen this issue so that it won't be forgotten after a few weeks and sit in the corner, not fixed until another person rediscover the problem. I can already see some potential features/existing packages that can be affected by the outcome.

[StefanKarpinski]

We're not adding some pseudo type whose "subtypes" are values. We can just fix this. If a parametric type is declared as P{x} then x can be anything—type or value; if it's declared as P{x<:Any} then x can only be a type, not a value. Internally we may need a way to indicate the difference but we certainly do not need a new pseudo type. This is slightly technically breaking because we currently allow a value in the latter case, but that's just bad and any code that relies on it should be fixed. Independently l we can add support for the P{x::T} which requires x to be and instance of T.

[StefanKarpinski]

Interestingly, P{x<:Any} and P{x::Type} would mean the same thing, but that's fine.

[vtjnash]

That is contradictory. If Any does not describe all values, then it is not the supertype of all values anymore, and thus there must exist a new element (it used to be called Top) that is the supertype of all values. But you have gained much confusion and breakage then with no gain.

[frankwswang]

That is contradictory. If Any does not describe all values, then it is not the supertype of all values anymore, and thus there must exist a new element (it used to be called Top) that is the supertype of all values. But you have gained much confusion and breakage then with no gain.

Could you elaborate more on why there should be a type that's the supertype of all values as opposed to just all types (as a subset of all values)? Is such a relation (between this "top" type and any value instead of any type) actively required and very pervasive in the source code of Julia?

[vtjnash]

Since there must be a type that represents the maximal set of all type-query, thus the supertype is a type. But all types are values, thus it is a supertype of all values. Using non-type values as parameters is rather common in julia, whether to describe the length of a tuple, the size of an array, or the fields of a named tuple.

[frankwswang]

Since there must be a type that represents the maximal set of all type-query, thus the supertype is a type. But all types are values, thus it is a supertype of all values.

I think you made a logical mistake here. "All types are values" does not necessarily mean "all values are types". Thus, even if we need a type to be the supertype of all types (though every possible type query), it does not necessarily mean we need a type to be the supertype of all values.

Furthermore, having non-type values as parameters for composite types does not require having a supertype of all values either. Because those non-type values are always wrapped by the composite type as a container, hence are not directly exposed to the subtype evaluation (A <: B). This matches the argument that we only need a complete relation tree within all types, not all values.

[vtjnash]

I didn't make a logical mistake, but did forget to state the additional condition that some values are types. And if you don't have a type that is the supertype of all values, then I can take Union{other-thing-not-in-any, Any} to make a new type that is now the real supertype of all values (and of all types). This however means that this new type was the actual supertype of all types, not Any (since it is a type that contains Any, but is not Any). This followed from the proof-by-contradiction starting from the assumption that Any is not the supertype of all values, then showing that it is either not the supertype of all types, or there is no value that is not a subtype of it.

Tuple{1} <: Tuple{Any} <: Tuple is a legal query (it returns true), because 1 <: Any is directly evaluated and returns true. In fact, all parameters comparisons are defined as computing the subtype relation <: on them. The subtyping algorithms are described in https://dl.acm.org/doi/10.1145/3276483 or Jeff's thesis work.

[frankwswang]

Thanks for providing the reference! I'll have a read! Meanwhile, can you give an instance of Union{other-thing-not-in-any, Any}?

From what I just checked, every element inside the {} of Union has to be a Type. Therefore it is automatically a subtype of Any (even if Any is set to be only the supertype of all types). Hence, it seems that Union{T1, ..., T1} can not be a supertype of Any other than Any:

julia> Union{1, Any}
ERROR: TypeError: in Union, expected Type, got a value of type Int64
Stacktrace:
 [1] top-level scope
   @ REPL[1]:1

julia> Union{Any, Any}
Any

[frankwswang]

Tuple{1} <: Tuple{Any} <: Tuple is a legal query (it returns true), because 1 <: Any is directly evaluated and returns true.

Personally, I also disagree with allowing Tuple{1} since one cannot actually create an instance (value) of this type.

[vtjnash]

From what I just checked, every element

Union{some, Any} is often (but not always) isomorphic to lower bound constraints on a TypeVar, of the form T>:some. Though it does possibly raise a slight, valid concern that Union{T} where T will simplify directly to Any even though substituting T=1 would not have been valid originally. It seems like Union also should allow any valid type parameter as a argument, similar to <:.

It also leads to this slight oddity (though Core.Compiler tries to filter out uninhabited tuple types to avoid this from causing crashes)

julia> Core.Compiler.unswitchtupleunion(Union{Tuple{1},Tuple{Int}})
ERROR: TypeError: in Union, expected Type, got a value of type Int64

one cannot actually create an instance (value) of this type

This is not usually a concern of type systems. For example, in Rust, this is used to have a Never type, which cannot have instances, but is distinct from other uninhabited types or the bottom type.

[frankwswang]

It seems to me that maintaining your insistence on having Any being the supertype of all values introduces more breaking changes and complications that will reflect on the user-end syntax than simply requiring T to be a type in SomeCT{T<:Any} (different from SomeCT{T} as here T can also be a value instead of just a type):

• Adding methods of <: for isbits, Symbol, Module, or tuples of them, making it effectively the same as isa
• Allowing Union{NotT} where NotT is not a Type even though it's not implementable

Meanwhile, you still haven't provided a scenario (that can already be realized in the current version of Julia) of creating a type Union{other-thing-not-in-AnyOfType, AnyOfType} (i.e. the true Any) that's the supertype of AnyOfType, except maybe

julia> Tuple{1} <: Tuple{Any}
true

which no user would encounter unless they deliberately try to construct Tuple{1}.

This also brings up another interesting inconsistency:

julia> Val{1} <: Val{Any}
false

which is another direct contradiction to insisting on 1 <: Any.

[vtjnash]

This does not mysteriously break isa, because types are already values. The isa query is fine with this. No, the Val example just shows that type parameters are invariant and that Any is not a subtype of 1.

[frankwswang]

No, the Val example just shows that type parameters are invariant and that Any is not a subtype of 1.

I admit I made a mistake here. For two parametric types with the same type names, the type relation between the parameters does not infer the relation between the two parametric types unless the supertype parameter is a UnionAll Type. As for Tuple, it's a particular case as its parameters are indeed covariant.

However, this does not affect my overall argument. I understand that, at this point, my discussion with @vtjnash has become somewhat unproductive, and I don't intend to convince or continue bothering them. So I write down my latest (and hopefully definite) thoughts here for whoever still wants to or will jump into this annoying little corner of Julia's current type system.

I really don't know why you really should hold on to using <: to constrain the type parameters, which I believe is the fundamental reason why you have to settle on having a type (a.k.a Any) be not only the supertype for all types but also all type parameters... Can't we just use someT in struct A{V::someT} to constrain the non-type parameter V? In fact, the current measure V<:Any is pretty useless at providing information to the compiler, precisely because for a non-type parameter, its type-related information lies in its type (e.g., typeof(V)), instead of its relation to Any or whatever we would call a "top type".

[vtjnash]

Another example of what would be logically inconsistent is T where T would now be have to be a strict supertype of Any (instead of simplifying to Any). It would no longer be equal to Any, since it is also valid for that T to take as value any type-parameter. This can arise in expressions such as Val{T} where {T<:(S where S)}, which is a valid constraint to form. This again shows that Any must be the supertype of all values, or it contradicts the assumption that Any is the supertype of all types.

[frankwswang]

Another example of what would be logically inconsistent is T where T would now be have to be a strict supertype of Any (instead of simplifying to Any). It would no longer be equal to Any, since it is also valid for that T to take as value any type-parameter. This can arise in expressions such as Val{T} where {T<:(S where S)}, which is a valid constraint to form. This again shows that Any must be the supertype of all values, or it contradicts the assumption that Any is the supertype of all types.

I don't see this as something that cannot amend. Even though the T where T in a Val{T} where T can be a superset of Any once you restrict Any to be only the supertype of all types, its effect will not leak out of Val which is a set of all the instances of a parametric type named Val, which is strictly a subtype of All. To explain my argument, we can see a similar case:

julia> Vector{Any}
Vector{Any} (alias for Array{Any, 1})

julia> Vector{Any} <: AbstractVector
true

julia> AbstractVector <: Any
true

where even though Any is a supertype of AbstractVector , but it doesn't jeopardize the fact that AbstractVector is still a supertype of Vector{Any}.

As for Val{T} where {T<:(S where S)}, If we make the behavior of <: consistent with its current methods (meaning its arguments have to be types), then T<:(S where S) would not be allowed because the upper bound here can only be Any, not the local UnionAll of T that can include non-type parameters but only resides in the {} of a parametric type.

The one side effect I can think of now is for the type query of Tuple since its parameters are covariant. However, as I said before, I don't think Tuple{V} where V is not a type should be legal in the first place.

[knuesel]

Maybe I'm reading it wrong, but the Julia subtyping paper seems to give some support to the argument against 1 <: Any. The paper refers to parameters such as 1 as "plain-bit values". In the grammar (start of section 3) they are distinguished from types: values that can be either types or plain-bit are written $a$ while values that are always types are written $t$.

Here are some quotes from the paper that are relevant to this discussion:

The abstract type Any is the type of all values and is the default when type annotations are omitted.
[...]
The variable v ranges over plain-bit values: in addition to types, plain-bit values can be used to instantiate all parametric types.
[...]
We abbreviate with Bot the empty union type Union{}, the subtype of all types. In the where construct, omitted lower bounds (resp. upper bounds) for type variables default to Bot (resp. Any); the notation t where T is thus a shorthand for t where Bot <:T <: Any.
[...]
The rule ANY states that Any is the super-type of all types.
[...]
Plain-bit values behave as singleton types; as such, the rule REFL is the only one that applies on plain-bit values.

Some observations:

• The paper describes Any as "type of all values" and "supertype of all types" but doesn't use the phrase "supertype of all values" that many find confusing (because "supertype" is a concept that doesn't logically apply to values that aren't types).

• In figure 2 the article defines the TOP rule (t <: Any) only for types (not plain-bit values), and the text states that the REFL rule (a <: a) is the only rule that applies to plain-bit parameters.

• The grammar (start of section 3) seems to allow where constructs for types but not for plain-bit values (it uses $t$ symbols here, rather than $a$ symbols). And in figure 2 where constructs are also never used with $a$ values).

• In the UnionAll paragraph on page 5 the article does mention the possibility of leaving a plain-bit parameter unspecified, but where clauses (such as where N) are never used to represent such a parameter. For example the article says that Rational can be written more accurately as Rational{T} where Union{} <:T <: Any, but the only relevant examples with arrays are the following:

  • Tuple{T, Array{S}} where S <: AbstractArray{T} where T <: Real refers to 2-tuples whose first element is some Real, and whose second element is an Array of any kind of array whose element type contains the type of the first tuple element.

  • partial instantiation is supported, and, for instance, Array{Int} denotes arrays of integers of arbitrary dimension.

[uniment]

That was quite a debate. I hope we can agree that 1 <: Any throwing an error makes sense, and Foo{1} <: Foo{<:Any} evaluating to true is nonsense—an artifact of an implementation detail instead of a design objective.

I'd like to throw out some possibilities to test the ergonomics of what could be:

Foo{T} where T         # T can be any type or any isbits value
Foo{:}                 # synonym for `Foo{T} where T`
Foo{T} where T<:Any    # T must be a type
Foo{<:Any}             # synonym for `Foo{T} where T<:Any`

degenerate cases:

T where T              # synonym for `Any`
T where T<:Any         # synonym for `Any`
Tuple{1} <: Tuple{Any} # throw TypeError? or return false?

Introducing type assertion :: allows for this:

Foo{n} where n::Int    # n must be a value of type `Int`
Foo{::Int}             # synonym for `Foo{n} where n::Int`

but also allows these redundancies:

Foo{::Type}            # synonym for `Foo{<:Any}`
Foo{::Type{Int}}       # synonym for `Foo{Int}`
Foo{::Type{<:Number}}  # synonym for `Foo{<:Number}`

It's attractive, but I'm not sure how to feel since <: returns a Boolean while :: does not; I could also argue for isa here.

[uniment]

Why was this closed?

[frankwswang]

Will this issue be reconsidered/reopened anytime soon in the future?