Tuple constructor forgets types

General Usage
1

Hi type lovers,

just stumbled upon the following surprising behaviour

julia> typeof(Tuple{Type{Int}, Type{String}}((Int, String)))
Tuple{DataType, DataType}

This should be Tuple{Type{Int}, Type{String}} shouldn’t it?

For NamedTuple this actually works as expected:

julia> typeof(NamedTuple{(:A, :b), Tuple{Type{Int}, Type{String}}}((Int, String)))
NamedTuple{(:A, :b), Tuple{Type{Int64}, Type{String}}}
2

Think of Type as a selector for dispatch in methods, not something that is a first-class object.

I would say that Type outside a method signature is a code smell.

What’s the problem you are trying to solve?

2 Likes
3

Hi @Tamas_Papp thanks for the picture, I am not sure whether it applies to my case as well:

I am trying to not loose type information :wink: and if my Tuple is just of type Tuple{DataType, ...} then I was expecting that type-inference would be poorer. Hence my goal to construct Tuple{Type{Int}, ... instead

4

Can you give an example of an actual value that has that type, with some context on how you use it?

5

EDIT: sorry, I was confused, better ignore this comment, it is rather unrelated

You are totally right, there is no actual value which has this type.

I am constructing it myself as a signature type with support for bits values. I.e. I represent the calling

f(1, [1,2,3])

with the signature

Tuple{typeof(f), 1, Vector{Int}}

turns out this is a quite intuitive representation, which simplifies a previous setup of mine where I used an extra wrapper for bits types. This way the interpretation is more direct, as everything which is not a Type is automatically a bits value. So I can clearly distinguish both levels without the need of an extra Wrapper.

Artificial, yes, but still useful

6

I am still missing context, and suspect this may be an XY problem. In any case, using Type as a first-class construct will be working against the language as it currently is.

7

I think I actually went to far.
The bits thing is indeed rather unrelated to my question here. Sorry for the confusion. You can forget it again for this question.

There actually is a concrete value which should have the type Tuple{Type{Int}, Type{String}}, and that is Tuple{Type{Int}, Type{String}}((Int, String)).
This is my understanding of a type-constructor, to preserve its own type.

But you seem to suggest, that this not intended… however then for all/most other Type constructors I know of, it is actually the case that they preserve. Like NamedTuple does it.

Can you explain further why you think Tuple{Type{Int}, Type{String}}((Int, String)) works against the language?

8

Perhaps you missed the docs link above?

1 Like
9

I mean Tuple{X,Y}(x,y) is such that typeof(x) == X. In your case, typeof(Int64) == DataType as expected.

Noticeably, typeof(Int64) is not Type{Int64} despite Int64 isa Type{Int64} being true. Type{} is used in function arguments such that compiler will specialize on argument that are types, which other wise won’t be specialized.

I think most of your questions arise from the fact that you keep trying to find edge cases in Julia’s type system without seeing Julia’s type system serves the multi dispatch in technical computing’s context, not Coq-like type system as a proof system context.

4 Likes
10

Type{T} basically only exists to make dispatching on types possible - all types (Int, String etc) are basically instances of type DataType.

julia> typeof(Int)   
DataType             
                     
julia> typeof(String)
DataType

Since you can’t usually dispatch on values (that would require some form of dependent type system), this Type{T} was invented to make it possible anyway.

There’s some more information in this juliacon talk from a few years back (should be timestamped, but in case it isn’t, relevant section starts at 13:00):

2 Likes
11

Hi @Tamas_Papp I am not so much a fan of XY problems. It is like a hammer you can put on any technical question which has its right to be discussed on its own. Sure my question arose in a concrete context, but still the question is a valid question on its own.

I already have my workarounds in place, so this is not a helpdesk scenario. I am stating this question because I am interested in this particular question.

This is why I am interested in this question: I want to understand how I can work with type-inference, especially whether I can preserve type-information when working on Tuples of Types.

I am open to use another DataType other than Tuple, that would fit fine. If Julia actually typeinfers nevertheless despite the types seem to indicate that information is lost, that would be good to know too.

12

I am a bit surprised that these type-level questions seem to be slightly unwelcome here.

I am just a programmer like you and it happens that one of my interestes is to get some better Type-Inference into my code. Others may have other interests, but that does not imply that my interest is somehow invalid.

Sure the authors of Julia had some thoughts on it and will have the final say. But Julia is a thing in its own right and if it turns out that I can improve the type-inference for my code by changing the definition of the Tuple constructor, that sounds like a valid thing to discuss.

(for complementing the typeof arguments. Sure typeof does not give you the type. That is intentional to keep down the load on the JIT compiler. Nevertheless there is Core.Typeof(Int) == Type{Int} which gives you more type-information and is readily available)

13

I don’t think your questions are invalid or anything. It’s just you have to realize Julia’s type system is (not yet?) designed to be like a mathematical proof. It just looks like you’re doing something overly complicated to achieve technical goals, which is why Tamas asked if this could be a XY problem.

If you’re only interested in type operations for fun, just do dynamic typing. If you’re using typing like the most people are: for compiler’s information → performance, then we want to know what’s your actual use case to have tuples of types while have types recorded in tuple’s type too – this just looks counterproductive.

2 Likes
14

Thank you for clarifying. I am still not convinced that it is a good idea to follow this XY thinking, but here you are: That is what I want to achieve:

  • I would like to build a function isdef(func, ArgType1, ArgType2, ...) which can tell me whether a function func actually has an implementation for the given types. I am not interested whether someone has written a generic method f(args...) = g(args...). If you just would like to know whether someone wrote a method, that is already simple to do. I would like to go through all these wrappers and see whether behind the layers there is still a proper definition.
  • my first thought was to use some generated functions together with Core.Compiler.return_type which worked reasonably well in my experiments.
  • however back then I got massive push back from some out of the Julia community spending a lot of efforst convincing me that, as of back then and I guess still today, Core.Compiler.return_type is something you should not use in your code at all. And yes, it is used in almost every package which defines a map, so apparently Julia has a type-inference problem, we know that.
  • I was indeed convinced that I do not want to rely on an instable functionality like Core.Compiler.return_type. One part I understood the argument that it my change from julia version to julia version and by this break arbitrary code. And I actually got into a lot of troubles with it myself, as the type-inference is far away from being easily understood.
  • so I am here and try to implement my own type-inference system which is powerful enough and constraint enough to implement an isdef finally.
  • and yes, I think such a functionality would very well fit into the Julia language. Concretely I would like to use it to circumvent the need of writing Trait functions which only define whether a function is defined. Exactly this I think is abstractable and solvable in general.
  • … I stop here for now

writing all this background information, my doubts about the XY approach haven’t become smaller unfortunately. It still feels like all this information is just needed because the original question is not answerable directly. Actually I haven’t understood, why the original question is not directly answerable. Please, if someone could explain to me, why it is not answerable, that would be highly appreciated. If someone can answer the original question directly, that is also still highly appreciated.

Does this background information help finding an answer to my question?

15

I forgot the crucial summary:

for isdef to be a truly useful function, it should be able to do most of its work at Compile time. Otherwise people would still define their own traitsdefinitions for better performance.

16

see, this is what NOT to do in Julia because Julia doesn’t have typed function. Of course it’s fine if you want to play with it, but this is the kind of thing either built-in to the language or not.

1 Like
17

I disagree as of now. Maybe you can convince me: What is the reasoning why you shouldn’t do this?

At this point I feel like it is just an aversion against type-level things. If someone says let’s do some AD, or some genify, that is all welcome, but type-inference seems to be special. All these are meta programming tasks, I cannot see as of now why type-inference is special.

18

Addition:
You say that the reason is because Julia doesn’t have typed functions. However, this is not a problem for me as I am using intermediate-representation IR for parsing everything myself.

this is the kind of thing either built-in to the language or not

Please if you could provide a reference to documentation or github issue which says this clearly, it would really be helpful. For now it seems to be your opinion which is stated as a fact with no return.

19

Basically the problem is that in Julia, it is possible to write functions where figuring out the return type requires solving the halting problem. As such, any attempt to determine the return type at compile time will be hacky and potentially incorrect.

3 Likes
20

thanks. Yeah, I get the feeling.

It is however not a problem to me. Also not every function can be autodifferentiated. Still it is useful to be able to autodifferentiate all the other functions.
Same goes for type-inference. I will have to think about how to deal with such functions… Still my intuition says I can identify or mark them to throw an Error or similar. Should not be a problem.