Extraneous ambiguity warning: (MyType{T},T) vs (T,MyType{T})

[toivoh]

The code

abstract MyType{T}

f{T}(::MyType{T}, ::T) = 1
f{S}(::S, ::MyType{S}) = 2

produces the ambiguity warning

Warning: New definition f(S,MyType{S}) is ambiguous with f(MyType{T},T).
         Make sure f(MyType{T},MyType{S}) is defined first.

This seems like
S has been instantiated to MyType{T} in the intersection, and
T has been instantiated to MyType{S}.
But that would mean that T == MyType{MyType{T}}. No type could fulfill this, right?
(8 out of the 19 ambiguity warnings here seem to be of this kind.)

The similar case

g{T}(::MyType{T}, ::T) = 1
g{S}(::S,         ::S) = 2

does not produce an ambiguity warning, though it would have been ambiguous if there were a type T such that T == MyType{T}.

[jiahao]

But that would mean that T == MyType{MyType{T}}. No type could fulfill this, right?

How about T == None?

Consider the closely related type

type NyType{T}
    x::T
end

which exhibits the analogous ambiguity warning.

What does NyType{None} really mean? If types are sets of all valid values, and the field x has no valid values of type None it can bind to, then there is no valid value with type NyType{None}. But this is the same as None, the type corresponding to the set of no valid values. In other words, NyType{None}==None should be true (although it currently isn't), and hence T == NyType{NyType{T}} should have the solution T==None.

(Not entirely sure how to make the analogous reasoning for MyType since there is no field to bind.)

[JeffBezanson]

No, the field x could be uninitialized, so you can have an instance of NyType{None}. Granted, if all constructors of a type throw errors then yes you can't have instances. However the rules of the type system do not depend on the behaviors of constructors.

[jiahao]

So is #undef a valid value? If it is, then x::None can be bound to a valid value #undef. But doesn't that contradict the definition of None as bottom type, that it can have no valid values?

[JeffBezanson]

No, undef is not a valid value, but a value with an undefined field is a valid value.

[jiahao]

Ok, so then parametric types are not universally quantified: it is not true that there exists a value x::None that produces a value y::NyType{None}, so NyType{None} is not the type defined by the image of the set of valid values of None when mapped through its constructor NyType{None}(x::None).

[jiahao]

Perhaps values with undefined fields simply have to be special-cased, so that NyType{T} is the union of NyType{T}(x::T=#undef) (which cannot be constructed in the usual way) and the set of all values which is the image of x::T --> NyType{T}(x::T = x).

[JeffBezanson]

I don't believe so, because a type does not have to be defined by the possibility of constructing it from other values. It can't matter if, for example, none of a type's constructors terminate.

[jiahao]

The specific issue I'm trying to grasp concerns specifically the relationship between parametric types and existentially quantified types; the latter, IIUC, are defined by construction as the image of a type when composed with a function type. I don't see the relevance of computability of a type constructor to this statement.

[JeffBezanson]

The point is that the type system can say a certain type is "inhabited" even if it is not actually possible to construct an instance. I don't think the function type x::T --> MyType{T} is especially important in deciding whether a type satisfies the equation T == MyType{MyType{T}}.

What is so bad about:

julia> type MyType{T}
       x::T
       MyType()=new()
       end

julia> MyType{None}()
MyType{None}(#undef)

?

[jiahao]

All I'm trying to do is to figure out how to express the behavior of Julia's parametric types in terms of "type theory types". Naively I thought

NyType{T} :== ∀ x ∈ T : x  ⟶ NyType{T}(x)

but to cover the case you just described it would at the very least have to be

NyType{T} ::= ∀ x ∈ T : x  ⟶ NyType{T}(x) | NyType{T}(#undef)

If the former were correct then NyType{NyType{T}} == T has the solution T = None, but not in the latter case.

I think I've reached the limit of what I can explain in writing.

[StefanKarpinski]

The issue with that formulation seems to be the use of the NyType{T}(x) construction syntax and the idea that there must be a unique empty type – in the sense that any type that is uninstantiable is None. Since we compare types somewhat formally (since whether a type is instantiable or not is undecidable), MyType{MyType{T}} can never be the same as None even if both contain no instances.

[JeffBezanson]

Yes, I really don't think this theory can be based on construction from
fields, because these are abstract data types. A constructor can accept any
arguments, and initialize fields any way it likes.

Tuples (product types) are a different case, because they are, by
definition, made of their elements. So arguably (Int,None) should be None,
the same way that Union(Int,None) is Int.

[jiahao]

It sounds like the argument for NyType{None} != None is based on the possibility of having valid compiler values with bit patterns like

+------+ :: NyType
|      |       +--------+
| [&x]-------> | #undef | :: None
|      |       +--------+
+------+

where &x is a memory address and #undef is an arbitrary bit pattern. Therefore the only reasonable type these values can have is NyType{None}. In contrast, by definition every valid compiler value can be assigned a type other than None (the bottom type), and so there is no valid value of type None.

It's interesting because the conventional view in type theory is to view an abstract type as either an existentially quantified or a universally quantified type, together with its interface of all allowed operations on them (Mitchell and Plotkin, 1988). In contrast, MyType{T} and NyType{T} are both examples of abstract types that are unquantifiable, so it is abstract in a sense that is demonstrably different from the sense intended by most type theories.

If tuple types are product types, then they are by definition record types with the trivial labels 1,2,..., which are quantifiable (which I believe is the formal way of saying "made of their elements"), and so it should be true that any tuple type containing a None should just be None.

[jiahao]

This can't be the full explanation though. My hypothetical argument above doesn't explain why MyType{None} != None. Also, if you can have a valid value of type NyType{None}, then surely you can have a value that looks like

+------+ :: (None,)
|      |       +--------+
| [&x]-------> | #undef | :: None
|      |       +--------+
+------+

whose only reasonable interpretation is a value of type (None,)?

[elextr]

@jiahao as I read @JeffBezanson MyType{None} != None because MyType{None} is a type object and it exists (so its not None) even if its not possible to create instances of that type.

[StefanKarpinski]

Without assuming the Axiom of Choice, it is quite possible that a tuple type where none of the components is None is still None. Of course, it would have to be an uncountable tuple.

[JeffBezanson]

@jiahao The issue is that "tagged struct" kinds of types are not defined by
their fields. You can add and remove fields from these types without
affecting any of their type relationships. There is no reason MyType{T}
must have a field of type T.
I think covariance has something to do with the emptiness of (None,). This
is a subtle difference between tuples and tag types like Tuple2{T,S}.

[JeffBezanson]

To clarify, it's not just covariance, but that there is no indirection
between a tuple type and the types of its elements.

[tkelman]

Oh, that's why this is recent. The test is new. It's been failing intermittently on AppVeyor and OSX Travis.