Counterexamples to the interpretation `<:` means "is a subtype of"

[path-doc]

Continuing the discussion from A precise definition of what it means to be an instance of an abstract type:

The following appears to contradict the claim <: means “is a subtype of” that appears in the manual (Types · The Julia Language).

julia> subtypes(Ptr)
Type[]

julia> Ptr{Float64} <: Ptr
true

I think the manual is in need of correction because it also states:

And of course, all specific pointer types are subtypes of the umbrella Ptr type:

Note that, unless we the function supertypes also disagrees with <: here since

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

julia> supertypes(Ptr)
(Ptr, Ref{T} where T, Any)

Any suggestions on how to reconcile? Is this specific to parametric types, and if so, then is Type a parametric type?

julia> Type{Float64} <: Type
true

julia> supertypes(Type{Float64})
(Type{Float64}, Any)

I am leaning towards the following reconciliation: Ptr{Float64} is a parametric instance of Ptr, but not a type instance or a subtype. This would fit Types · The Julia Language :

types can take parameters, so that type declarations actually introduce a whole family of new types – one for each possible combination of parameter values.

Parametric instances are then “subnodes” of the parametric type.

But, since <: picks this up, Ptr{Float64} <: Ptr does not really mean “Ptr{Float64} is a subtype of Ptr”. Instead, it is simply ensuring that Ptr{Float64} inherits the properties of Ptr. Would it not make more sense to put both parametric instance and parametric type at the same level of <:, so that
Ptr <: Ptr{Float64} also holds? There is a weak precedent in

julia> Int <: Int64
true

julia> Int64 <: Int
true

[sostock]

@path-doc

Any suggestions on how to reconcile?

In my opinion, there is nothing to reconcile: <: is the subtyping relation and subtypes(T) and supertypes(T) simply don’t show you all objects for which S <: T or T <: S holds, because that’s not possible in general. How would they accomplish that? Both subtypes and supertypes would need to return arrays with an infinite number of elements in that case. For example, subtypes(Ptr) would have to return an array containing Ptr{Float64}, Ptr{String}, Ptr{Ptr{String}}, … really all Ptr{T} for every possible T. And supertypes(Float64) would have to return Union{Float64, String}, Union{Float64, Nothing}, … also infinitely many values. Therefore, they are not useful for determining actual subtyping relations (except in some cases), that’s what <: is for.

[FPGro]

@path-doc

There is a weak precedent in

julia> Int <: Int64
true

julia> Int64 <: Int
true

You may have gotten this wrong, Int is an alias to either Int64 or Int32 depending on your machine.

julia> Int === Int64
true

[path-doc]

Yes, that is why I say “weak precedent”. But the rest came straight from Julia.

[path-doc]

That would be true for supertypes. But also for subtypes? No, subtypes only shows the next level down I’m afraid. And my notion of parametric instance would bind all those infinite regressions into a single node. This would allow subtypes to accurately represent the children according to <:. For consistency reasons, I think that’s important: as it is, “subtypes” has two definitions:

1. according to subtypes
2. according to <:

[kristoffer.carlsson]

@path-doc

Yes, that is why I say “weak precedent”.

To be clear, Int and Int64 are exactly the same thing on 64-bit machines:

julia> Int
Int64

So I don’t see how there is any precedent at all. What you wrote was

julia> Int <: Int
true

julia> Int <: Int
true

[path-doc]

Thanks for the following info:

@kristoffer.carlsson

To be clear, Int and Int64 are exactly the same thing on 64-bit machines:

julia> Int
Int64

I was aware of the rest. So what about for other machines?

[kristoffer.carlsson]

On 32-bit machines, Int is simply an alias for Int32.

[DNF]

@path-doc

That would be true for supertypes . But also for subtypes ? No, subtypes only shows the next level down I’m afraid.

I’m pretty convinced with the argument that the issue (as far as there is one at all) is with the subtypes and supertypes functions, not with <:

[sostock]

@path-doc

Would it not make more sense to put both parametric instance and parametric type at the same level of <: , so that
Ptr <: Ptr{Float64} also holds?

This would mean that every method f(x::Ptr{Float64}) would also allow any Ptr as an argument. How would that work?

[path-doc]

Of course, yes, that helps.

[path-doc]

On the present question, I think @DNF is right, it is a question of making the output of subtypes/supertypes more accurate.

Can I please turn your attention to

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

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…

Do you agree that Ptr{Float64} is not an instance of Ptr? Rather, it is a subtype. In which case, the manual needs updating.

Do you agree with that definition?

[simeonschaub]

@path-doc

On the present question, I think @DNF is right, it is a question of making the output of subtypes/supertypes more accurate.

As others have already pointed out, this is generally impossible, because types can have an infinite number of sub- as well as supertypes.

I wouldn’t be too focused on sub-/supertype. They are really just for explorative interactive usage, e.g. if you want to find examples of an AbstractArray or if you want to get an idea of the type hirarchy of a specific type. These functions aren’t actually used by Julia internally, so they aren’t actually very important for understanding how Julia works and don’t really have a rigorous meaning like <: does.

[path-doc]

@simeonschaub

As others have already pointed out, this is generally impossible, because types can have an infinite number of sub- as well as supertypes.

I disagree, I think it can be effectively represented, but obviously not as an infinite regression.

(The like is for the last bit. )

[simeonschaub]

Then how would you represent subtype(Any) or supertype(Union{})? You can have an infinite number of tuple types alone and of course you can arbitrarily nest types.

[pfitzseb]

Also, supertypes doesn’t give you all supertypes of a given type; it gives you all types reachable by recursively applying supertype. Each type can only have one supertype, and UnionAlls are not reachable by supertype, afaict.

[path-doc]

Okay, I would parametrize it as a set in subtypes. An alias that specifies a set. Done. Very much like Int represents Integers for the infinitely many types of machine that may ever come into contact with Julia.

[path-doc]

Thanks, that’s a good point. Do you know the grounds on which supertype “chooses” parents?

[simeonschaub]

You mean introducing for example an object for representing the set of all types, let’s call it Any? You probably also need a way to represent Vector{T} where T can be any type, let’s call that Vector{T} where T (or Vector for short). Ok, now one other thing that would be useful would be having a way to represent the union of possibly infinite sets, for example a type that is either any subtype of Vector or any of SubVector. We can just call that Union{Vector, SubVector}. It would also be nice to be able to group vector-like objects in a single type, so let’s introduce something called AbstractVector – we might want to call that an abstract type – to group all of these under.

Congrats! You basically just implemented the basic constituents of Julia’s type system. There is of course a lot more to it than that, but you get the gist. The type system is exactly for representing these types of sets.

[path-doc]

@simeonschaub

You mean introducing for example an object for representing the set of all types, let’s call it Any ?

No, I meant for the subset of subtypes that is Ptr, it would be desirable to represent the fact that there is something in there like Ptr{T}. I don’t think what I am saying is that strange. I mean I have to do stuff like that on a daily basis in my field.

All I’m saying is that, if you say something is a subtype, then it should be what it says on the tin. In my view, the rest slightly sloppy at best and could be very misleading at worst. If you are saying it’s not worth the effort, I’ll take your word for it.