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

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[].

5 Likes