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

Typing
21

No, I meant C.__call__ (not an instance of C), which without a metaclass is the same as type.__call__

The full chain that determines the appropriate signature involves metaclass call, metaclass prepare, metaclass new, class new, and class init

22

I don’t think C.__call__ is typically used to refer to its metaclass’s __call__. It might help to write type(C).__call__ explicitly.

>>> class M(type):
...     def __call__(self, *args, **kwargs):
...         return super().__call__(*args, **kwargs)
...
>>> class C(metaclass = M):
...     def __call__(self, *args, **kwargs):
...         ...
...
>>> class D:
...     pass
...
>>> C.__call__  # Its own __call__
<function C.__call__ at 0x0000000000000000>
>>> D.__call__  # type.__call__
<method-wrapper '__call__' of type object at 0x0000000000000000>
1 Like
23

right, I only checked something that looked more like D and wasn’t thinking out all the outcomes when discussing this with @Liz

The practical signature ... and return type of C(...) when the type C is called, whether resulting in an instance of C or not is probably a good phrasing.

This composes several function signatures in both the type and any metaclass of the type, and we don’t have a concise term for that.

24

I guess this one of those cases where the actual interpreter behavior doesn’t match what it looks from just looking at the objects created.

I’m “okay” with this definition, it matches the intent we were discussing.

There’s still a question of if this is something that breaks existing use. I’m not convinced by @carljm 's example with statictypes. This seems to be the most common way people use type[], so I can’t make a good argument that we should have ConstructableType or something separate that accurately describes this where type doesnt. the type system should probably just work how people expect it to.

25

This has a point of unsoundness, the definition of Y itself is unsound. If this was the whole program, and we specifically analyze it, we can say the unsoundness is never triggered, but python isn’t a compiled language, and the type system has function boundaries.

26

It’s a matter of opinion where precisely you choose to place the unsoundness. If you assume that type[] must exist and be both covariant and constructible, then sure, any subclass that doesn’t preserve LSP in its constructor is unsound. But that’s not a very useful definition, since object.__init__ takes no arguments, which would make all Python classes that accept any constructor arguments at all unsound. So this approach is equivalent to saying “we just won’t have soundness,” since outlawing constructor arguments is not going to happen. (And “we just won’t have soundness” is of course the status quo for actual type-checkers in this area.)

It’s just as reasonable (and IMO more useful) to say that the unsoundness lies in having type[] be both covariant and constructible, rather than inherently in the subclass. Subclasses that don’t preserve LSP in the constructor are perfectly sound in terms of the instance type (the constructor isn’t even part of the instance type!), the unsoundness only appears when we introduce a covariant and constructible type[] type.

I think a conceptually clear approach that allows us to soundly express everything we might want to express has been mentioned above already: to say that type[] just refers to subclassing (as the spec currently defines it), which would mean it is covariant but not constructible (at least not in a safe/sound mode), and then make constructible types from an intersection of type[] and Callable[]. IMO this outcome is generally worth aiming for. The open question, as you mentioned, is whether we keep type[] defined as-is (though without constructibility, which is not specified but is implemented, unsoundly, by all type checkers) and add a new syntax sugar for that constructible-type intersection, or we redefine type[] to mean that constructible-type intersection. I agree that the latter probably agrees better with much current usage of type[]. Both are breaking changes in practice for some current code. The former is more expressive, in that it still gives you a way to spell the always-covariant-but-not-constructible “C and all subclasses of C” type[].

6 Likes
27

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, but that when a type is defined the default may be applied and that any definition has to conform to what the interpreter needs (not the default implementation). But we don’t have a way to describe this in the type system currently. Similar issues exist with __hash__ and __eq__

1 Like
28

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 (though how they can be used would differ)[1], but because of the way object is implemented and typed, without further special casing here, these would not remain equivalent in accepting all type objects.

I have to wonder if it’s possible to do this temporarily, with a note that the rule may change if the tools to express the needed intersection are added to the language. or if that is the intent, that it’s better to put a new special construct into the language that type checkers understand to mean this because it’s not expressible by users yet.

Normally, I lean towards more expressiveness, but when the most common use I see for type[] is unsound, I’m led to believe that the type system isn’t being pragmatic here and that people aren’t getting what they likely expect from type checking here.

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.

  1. tangent/prodding you to actually start the discussion when you have the time @mikeshardmind possibly another compelling reason for you to open a discussion about AnyOpaque I think you’re now at at least 5 places in the type system where people may benefit from this. ↩︎

29

Update: The wording concerns have been addressed in the PR. Since no other relevant concerns have been raised, I have filed a proposal for the typing council.

30

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.

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.

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.

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.

3 Likes
31

This change has been approved by the TC, and the typing spec has been updated accordingly.

Thanks to @InSync and everyone else who contributed to the discussion.

5 Likes