Specs clarification: `type[A | B]` is equivalent/the same as `type[A] | type[B]`

[carljm (Carl Meyer)]

@Liz

The only issue I have with the latter is type[object] vs type[Any]. The two should be identical in terms of what they accept given covariance

If we redefined type[X] to mean “all type objects that are subclasses of X and also have a constructor signature which is a subtype of X’s constructor signature” (which is “the latter” idea), then type[] would by necessity no longer be covariant. If X <: Y, type[X] <: type[Y] might hold in some cases, or it might not; it would depend on the constructor signatures of X and Y. So there is no special problematic case with object.

@mikeshardmind

I think this is where as a matter of pragmatism, the “default” implementations probably need to be seen as defaults that only apply when no definition exists rather than part of LSP

I don’t agree that there should be or needs to be any special-casing around the object constructor. Even if we ignore the object constructor, non-LSP constructor overrides are way too useful and widespread (and sound, essentially everywhere except for in type[]) to consider outlawing them in general. As I mentioned above, the constructor is not even part of the instance type (barring calling __init__ or __new__ explicitly on an instance, which is extremely unusual and should just be a type error in a type checker aiming for soundness), so instance subtyping does not need LSP on constructors to be sound. Requiring LSP on constructor signatures would be letting the “tail” of type[] wag the “dog” of instance subtyping.

We don’t need LSP on constructors, or any special-casing of object, in order to pursue a sound definition of constructible type-object types as the intersection of a subclass type and a callable type.

@Liz

As for analyzing the original equivalence discussion, my analysis of it is that if we are fine with relegating this to a new construct or waiting on 2 type system features that dont exist yet (intersections + copying callable signatures/ return types from static types) then type[A | B] is identical to type[A] | type[B] in the types which it describes both for assignment and for usage, if we aren’t, these aren’t identical, but ironically would be again if LSP was enforced on constructors, except in the special case of type[object] and whatever necessary exceptions needed to be implemented because of default construction.

Ok, let me spell this out a bit more explicitly. Let’s hypothesize (just for the sake of clearer spelling here) that ConstructibleType[X] means type[X] & CallableTypeOfConstructor[X]. ConstructibleType[X | Y] would therefore be type[X | Y] & CallableTypeOfConstructor[X | Y]. We’ve already agreed that if type[] just means “subclass” then distributing it over a union is fine, and it seems equally reasonable to say that the callable type of the constructor of a union is the union of the callable types of each constructor, so that expands to (type[X] | type[Y]) & (CallableTypeOfConstructor[X] | CallableTypeOfConstructor[Y]). The lack of equivalence arises because a type object that is a subclass of X but whose constructor is a subtype of the constructor of Y would satisfy this, but would not satisfy either ConstructibleType[X] or ConstructibleType[Y].

I think this analysis is correct, but I also think specifying that type[X | Y] is equivalent to type[X] | type[Y] is correct given the already-existing clear definition of type[] in the spec, and it matches the existing interpretation of type checkers. And as a general principle, I think that we shouldn’t avoid clarifying today’s spec because of changes we might want to make to the spec tomorrow. Redefining the meaning of type[] will have to contend with the real-world backward-compatibility concerns either way; changing a sentence in the spec is an inconsequential barrier in comparison (there are several other sentences about type[] already in the spec that would also need to be changed for this redefinition to occur).

So I don’t see this as a barrier to the proposed spec change.

@InSync

Since no other relevant concerns have been raised

I think the concern about unsoundness of type[] and how we might possibly want to tighten it in the future is a relevant concern, but (as mentioned above) I also think it shouldn’t block the clarification.