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

[kristoffer.carlsson]

@path-doc

(Btw, someone else somewhere was saying that Ptr is definitely abstract.) So according to you, parametric supertypes are neither concrete, nor abstract.

Did you watch the video that has been linked to you multiple times? It explains things quite clearly.

[giordano]

@path-doc

So according to you, parametric supertypes are neither concrete, nor abstract.

It’s a UnionAll Also, you can have parametric abstract types (e.g. AbstractArray{T,N}), so UnionAll is orthogonal to being abstract or concrete.

@path-doc

Though their subtypes are all concrete?

Not necessarily: Array{Float64} <: Array, but it isn’t concrete, it’s another UnionAll: you need to specify all parameters in order to get a concrete type.

[path-doc]

Thanks, please explain meaning of “orthogonal”. Are you saying it is independent (in the logical sense) of being abstract or concrete?

[giordano]

Yes

[path-doc]

To be honest I come from a fairly pure school of mathematics, so I don’t see why I should look to a video for a definition. But given your recommendation, I will. Yes, I have been into the manual, but I didn’t see anything about how the type space is partitioned. A nice diagram would do it.

[kristoffer.carlsson]

@path-doc

To be honest I come from a fairly pure school of mathematics, so I don’t see why I should look to a video for a definition

It seems you want to learn about the type system of Julia. The video is about the Julia type system from the creator of Julia. How can you not want to watch it??

[path-doc]

I am looking for formal definitions. Can you point to a formal definition of how types are partitioned?

[simeonschaub]

Here you go: https://benchung.github.io/papers/jlsub.pdf

[path-doc]

Thanks, yes, that is a very useful reference. I have been reading that for a few days now.

[giordano]

In case it isn’t clear enough, there hasn’t been a rigorous formal description of the type system before its implementation. Some researchers, like those in the paper linked above, have studied it afterwards. If you’re looking for an original complete formalisation of the type system you won’t simply find it anywhere, it doesn’t exist

[path-doc]

I appreciate that. But then can you please add some more flesh/structure to your previous statements. Can you prove that Ptr is neither Concrete, nor Abstract? Or would you point me to a video or the manual?

(Sorry, must have been tired last night.)
Correct version.
Let’s agree that abstract types are defined as precisely those that cannot be instantiated. That is, they only exist as nodes on the graph of types (this is literally from the manual). Moreover, let’s work with Array instead of Ptr.

You see, I would say that one way to tell that Array is abstract is that it can’t be instantiated in the sense that, unlike concrete types, there will never be an instance of an object x such that typeof(x) = Array. Since the parametric type Array can’t be instantiated in this sense, it only exists as a node on the graph and it is formally abstract.

Now concrete and abstract are complementary properties, thus Array is not concrete by virtue of the fact that it is abstract.

Next let’s prove that `Array{Float64} is a concrete type:

julia> x = [1.0]
1-element Array{Float64,1}:
 1.0

julia> typeof(x) == Array{Float64,1}
true

This is how I like to operate. I don’t trust videos or manuals. I barely even trust my own definition. Though I have to say it has held its own in this conversation.

So, assuming Ptr and Array similar in this respect, I deduce that Ptr is abstract (contrary to yesterday’s conclusions). You are completely right about the parametric instances of Ptr and Array: they are indeed concrete.

[giordano]

@path-doc

Can you prove that Ptr is neither Concrete, nor Abstract? Or would you point me to a video or the manual?

Ptr is a shortcut for Ptr{T} where {T} and it’s the set of all Ptr{T} over all T. It isn’t abstract in the sense that you can’t define a new type X such that X <: Ptr{T}. It isn’t concrete in the sense that you need to concretely specify T in order to have a concrete type that can actually be instantiated. Again, Ptr isn’t a type, it’s a set of types.

[path-doc]

The above like applies to everything except your last sentence.

@giordano

you should think of types as the set of values they can take, and <: is the subset relationship.

Because then every type is a set.

I think am looking for defining properties of objects that are neither concrete, nor abstract.

I am now sure that parametric supertypes lie in the complement of both concrete and abstract. In contrast, other parametric (sub)types such as Ptr{Float64} are concrete because they can have instances eg pointers themselves.

Thanks @giordano, you’re very helpful.

[giordano]

@path-doc

Because then every type is a set.

That’s correct: a type is the set of all values it can hold. A UnionAll is a set of types, so the union of multiple sets.

[path-doc]

But then it doesn’t help me: it’s a property of everything. I am looking to organise my mental map of the type space. (I mean numbers like 1, 2, … can also be viewed sets, this is what we do when we conduct well-ordered sets.)

Thanks again, and bye for now. It’s past midnight where I live.

[path-doc]

Definition : Object x is an instance of the abstract type y if, and only if,

1. the concrete type t_x of x and the value v_y of y satisfy t_x<:v_y, or
2. y is a singleton type and x is its instance (which can be verified using isa)
3. …
   What is difference between Type{T} and T - #58 by path-doc

[Tamas_Papp]

@path-doc

I am looking to organise my mental map of the type space. (I mean numbers like 1, 2, … can also be viewed sets, this is what we do when we conduct well-ordered sets.)

With respect, I think that approaching the whole of Julia’s type system with a very formal/mathematical mindset is unlikely to be helpful in using Julia.

The basic intuitive building blocks are (ignore Type and types as values for now):

1. values have a type, which you can query with typeof,
2. these types are organized into a tree, with <:,
3. types have parameters.

Now the complications: types themselves are first-class objects, so you can consider them values, with typeof(SomeType) == DataType. This is not super-helpful for dispatch, so Type{T} was introduced as a selector — the updated manual makes this more clear. But seeing a Type outside a method signature is code smell, and integrating Type and DataType into your mental map of Julia types is just a recipe for a headache.

[Jeff_Emanuel]

@Tamas_Papp

But seeing a Type outside a method signature is code smell

What about instantiating a parametric type, such as Array{Float64,1}? Is that also a code smell? I ask because I’ve seen many discussions of performance here mentioning avoiding containers that might infer the element type as an abstract type, particularly Any.

[Tamas_Papp]

@Jeff_Emanuel

What about instantiating a parametric type, such as Array{Float64,1}? Is that also a code smell?

Nope, that may be fine, especially if you do type calculations, or need the type repeatedly.

But I would avoid the term “instantiate”: in idiomatic code, that will be something the compiler just gets rid of. It is no more “instantiated” than 1 is.

[Jeff_Emanuel]

Maybe construct is the right word and I’m misapplying vocabulary from OOP languages.
Say I want to create an instance of a Dict and not have it infer Anys. I have been writing, for example, d = Dict{String,Float64}(). Would that be proper?

And I apologize for the digression from the original topic.