A precise definition of what it means to be an instance of an abstract type

New to Julia
1

This question builds on What is difference between Type{T} and T - #16 by Henrique_Becker

Are there any objections to the definition below?

Based on the following two quotes from Types · The Julia Language

One particularly distinctive feature of Julia’s type system is that concrete types may not subtype each other: all concrete types are final and may only have abstract types as their supertypes.

When the type is abstract, it suffices for the value to be implemented by a concrete type that is a subtype of the abstract type.

Definition: Object x is an instance of the abstract type y if, and only if, the concrete type t_x of x and the value v_y of y satisfy t_x <: v_y.

Note that, according to this definition, Type is an instance of itself because

julia> typeof(Type)
UnionAll

julia> UnionAll <: Type
true

Moreover, this definition works with examples like Type{Float64}. It is an instance of Type because typeof(Type{Float64}) = DataType and DataType <: Type both hold.
But UnionAll is not an instance of itself

julia> typeof(UnionAll)
DataType

julia> DataType <: UnionAll
false

Indeed, via the same argument, no type in the chain (Int64, Signed, Integer, Real, Number) is an instance of itself.

Whilst I am comfortable with the above, the Ptr provides a potential counterexample because, according to the manual it has “instances” such as Ptr{Int64} and Ptr{Float64}. But

julia> typeof(Ptr{Float64})
DataType

julia> DataType <: Ptr
false

and

julia> isa(Ptr{Float64},Ptr)
false

Personally, I like definition at the top of this post as I can imagine applying it in the field. There are two ways to rescue it:

  1. say that Ptr is not an abstract type. Is this reasonable? If so, then is it concrete, or can parametric types be neither abstract, nor concrete?
  2. say that Ptr{Int64} is not an instance of Ptr. This would fit the observation that Ptr has no subtypes, but not the observation that Ptr{Int64} <: Ptr holds. (I am putting this latter contradiction in a separate topic.)
2

I don’t understand this part of the definition:

What is “the value” of an abstract type?

3

For instance, the value of Int64 is simply Int64, but the concrete type of Int64 is typeof(Int64) = DataType.

4

But why do you need v_y then? Simply use y in its place.

5

I’m not sure what you mean by “value vy of y” in your definition. If it’s saying that y is an abstract type that implements vy in the way that Int64 is a concrete type that implements 1, then that’s impossible because by definition, only concrete types implement. It looks fine if that detail is omitted: in more familiar terms, x isa y if and only if typeof(x) <: y.

Couple things:

  • isconcretetype(aType) can be used to distinguish a concrete type and an abstract type. Ptr is definitely abstract.
  • Ptr{Float64} is a subtype, not an instance, of Ptr.
1 Like
6

Well, it depends on what you’re trying to do. When you write an object as a pair you can then consider the concrete type tag of y as its second dimension. Objects and values are then isomorphic.

7

Well, if you are right, then the manual is wrong as it explicitly says that Ptr{Float64} is an instance of Ptr. But, personally, I agree with you on this point.

But regarding

consider

julia> supertypes(Ptr{Float64})
(Ptr{Float64}, Ref{Float64}, Any)

julia> subtypes(Ptr)
Type[]

As you can see, Ptr is not in there. Yes, I know it is according to <:, but as I point out in another discourse, it is not at all clear that <: means “is a subtype” in the case of Ptr.

8

Ptr (like all parametric types where some of the parameters aren’t fully specified) isn’t a single type, it’s a UnionAll, an infinite-many collection of concrete types. Ptr{Float64} is a concrete realisation of Ptr.

This doesn’t make sense: X isa Y is the relation “X is an instance of type Y”. Perhaps you wanted either of

julia> Ptr{Float64} <: Ptr
true

julia> Ptr{Float64}() isa Ptr
true

?

5 Likes
9

Great, then, since typeof returns the concrete type of an object, why do we have

julia> typeof(Ptr{Float64})
DataType

Well the manual states that Ptr{Float64} is an instance of Ptr. See the first line of
https://docs.julialang.org/en/v1/manual/types/#UnionAll-Types

10

Ptr{Float64} is a data type, why do you think it’s wrong?

Would “realisation” instead of “instance” be clearer for you? You can only have instances of concrete types

2 Likes
11

That first bit isn’t that odd. Ptr{Float64}() is an instance of the concrete type Ptr{Float64}, and Ptr{Float64} is an instance of the concrete type DataType. Types are objects/instances, too!

In that thread you linked, I think the takeaway is that <: means exactly “is a subtype of”, and that the subtypes and supertypes methods just cannot be comprehensive.

That line in the manual is odd. Right before that line, it states that Ptr{Float64} is a subtype of Ptr in the <: sense.

1 Like
12

Okay, so you are saying that realisation \neq instance, right?

Can you please give me a formal definition of realisation? I have given you one of instance. I like my definition. But my definition does not extend to abstract parametric types precisely because

julia> typeof(Ptr{Float64})
DataType

julia> typeof(Ptr{Float64}) <: Ptr
false

And everyone here seems to be convinced that Ptr{Float64} is a subtype of Ptr.

13

I’m saying that Ptr is a family, a set of concrete types. Ptr{Float64} is a concrete type of this family/set. Call it “realisation” or whatever you want, I don’t know whether there is a formal name for it. “Instance” here is probably used in a loose way.

3 Likes
14

I think we should just call it a concrete subtype, just to stick with formal terms.

1 Like
15

There is this nice talk by Jeff about the type system:

It’s from 2017 and some details may have changed since then, but I think the most interesting takeaway message is that you should think of types as the set of values they can take, and <: is the subset relationship.

6 Likes
16

If your definition puts any importance on the relation typeof(Something{Parameter}) <: Something, I think it’s best you discard it. Maybe it seemed to make sense at first because of Type, UnionAll, and DataType, but those are really more of an exception.

Say you have an object x then recursively go through the concrete types by repeatedly running x = typeof(x), eventually you start to cycle through DataType because the type system had to begin somewhere to make instances. Note that this is not about the type hierarchy; Any was decided to be the union of all types and thus the ultimate supertype, but even Any is an instance of DataType.

1 Like
17

That is the concrete type tree. It is the foundation on which the abstract graph of types is built. Abstract types form the hierarchy, but instances live on the concrete tree. That is the essence of my definition.

18

Well not if Something{Parameter} is not an abstract type. My definition only applies to abstract types. So is Ptr an abstract or concrete supertype of those concrete types `Ptr{x}?

19

Again, it’s none of them: it’s a collection, a family, a set of concrete types

4 Likes
20

Thanks, so my definition remains intact. (Btw, someone else somewhere was saying that Ptr is definitely abstract.) So according to you, parametric supertypes are neither concrete, nor abstract. Though their subtypes are all concrete? I will try to digest.