What I’m trying to get at here and not doing a great job of explaining is that the choice of invariance is actually more superficial than people think it is. That’s because the language actually has ways of expressing all the variances. The only way that invariance is privileged is that the syntax T{P}
is invariant with respect to P
rather than being covariant (or even contravariant). So let me try to clarify a bit. I’m going to write T{=:P}
for the type we normally write as T{P}
, i.e. the invariant parameterization of T
. There three distinct types associated with any parametric type:
- The covariant type,
T{<:P}
‚ which includesT{=:S}
for allS <: P
- The invariant type,
T{=:P}
, whereP
is fixed. - The contravariant type,
T{>:P}
, which includeT{=:S}
for allS >: P
.
The first and last are abstract whereas the middle is concrete. Languages may use different syntaxes for these concepts, may not have syntaxes for all of them, and may even use the same syntax for more than one of these concepts. They may even combined some of these concepts in their type system.
For example, most languages that are said to have “covariant parametric types” use the syntax T{P}
to mean both T{<:P}
and T{=:P}
in different contexts. They also combine these distinct concepts in their type systems: the type of a vector that can any element that is a subtype of Real
is Vector{Real}
in such a system; but in dispatch that type also applies to any vector with an element type that is a subtype of Real
. In such a language the syntax and the type Vector{Real}
represent both the concrete type Vector{=:Real}
when asking the type of things and the abstract type Vector{<:Real}
when doing dispatch. In effect, what it means to be a language with covariant parametric types is that a language conflates the distinct concepts T{<:P}
and T{:=P}
both syntactically and conceptually. Perhaps I’m missing something here and someone who is an expert in these kinds of languages will be able to correct me on this.
Julia distinguishes T{<:P}
from T{=:P}
both syntactically and conceptually, using the syntax T{P}
for the latter. The type Vector{Real}
is concrete and is the type of a vector whose element type is Real
. You can use this type in dispatch and write a method that only dispatches on vectors with that exact element type. The type Vector{<:Real}
, on the other hand, is abstract and not the type of any value. You can, however, use this type in dispatch (or as the type annotation of a field or as parameter of another type).
The decision to not allow subtyping concrete types is another case of languages traditionally failing to distinguish different concepts. When you subtype a concrete type in a language that allows it, this is really conflating two distinct concepts:
- The type that is concrete, complete and can be instantiated but not subtyped
- The type that is abstract, incomplete and can be subtyped but not instantiated
Many OOP languages treat these distinct concepts as a single thing. In such a language, you can declare a type as final
thereby precluding the second option. Otherwise you have, say, Vector{Float64}
and you can’t tell if the element type is the concrete, final Float64
type or the abstract, subtypable Float64
type.
If you want to both instantiate and subtype a type in Julia, you do have an option: you make two separate type — one abstract, A
and a concrete subtype of that, C <: A
. Then we can distinguish, for example, Vector{C}
which can only hold instances of the concrete type C
, from Vector{A}
which can hold instances of C
but also instances of any other subtype of A
. But most of the time this isn’t necessary, especially since new methods for C
can be defined externally.
In general the Julian approach is primarily about keeping distinct concepts distinct both syntactically and in the type system. One aspect of this is not conflating T{<:P}
and T{P}
. The other aspect is forcing the user to distinguish between a concrete type that can be instantiated and abstract types that can be specialized.