Pulse check on Intersections draft work

Typing
21

I can see three potential use-cases for always-raising methods:

  1. raise NotImplementedError. I’ve used this several times myself, when implementing or designing classes with multiple methods, and I think the developer should be able to tell the type checker “I know what I’m doing, don’t distract me” until the code is production-ready.

  2. Always-raising method in a base class that’s annotated to produce a value, because subclasses are allowed to implement it in order to provide custom behaviour (for example supporting additional, external types).

    Silly example (obviously not the best interface but I think this idea is common in the wild, especially since you cannot implement methods on external types without 'black magic') 
    class Serializer:
    @final
    def serialize(self, x: object, /) -> str:
        ... # logic that handles builtins, collections etc. by calling `self._serialize_scalar`

    def _serialize_scalar(self, x: object, /) -> str:
        raise TypeError(f"I don't know how to serialize object of type {type(x)}")

class DecimalSerializer(Serializer):
    @override
    def _serialize_scalar(self, x: object) -> str:
        if isinstance(x, decimal.Decimal):
            return str(x)
        return super().serialize_scalar(x)

  3. Some exception types (for example, StopIteration, but a library might define their own) are intended to be handled in a specific way, maybe because they carry control-flow information. It makes sense for __next__ in Iterator (or a concrete iterator base class) to be defined as returning, while an empty iterator can implement it with just raise StopIteration(). This is actually very similar to point 2. now that I think more about it…

Anyway, all the cases I’ve described only arise, in my mind, in a sort-of explicit manner, and I’m not sure whether they can be mapped to the implicit case (A & B having the same method with incompatible return types, and as a result of that incompatibility the return type magically becoming Never). In my mind, a silenceable warning would be the best option.

By the way, thanks (to you, but also everyone else involved) for the hard work on intersections: it will clearly be a very impactful change to the expressiveness of the type system, and as a typing user I’m really excited about it!

Edit: For some reason I hadn’t seen it but you had already answered this: perfect! Then I don’t have any objection and every option above is good; sorry for the extra post.

1 Like
22

Thanks for explaining @mikeshardmind - I can’t think of an issue with the restriction being exclusively on the use of Never

I would recommend updating the OP :slightly_smiling_face:

1 Like
23

Perhaps you’ve done this already, but it might be worth comparing how these rules [1] compare to what ty describes here:

  1. which I’m sure are just the tip of the iceberg ↩︎

24

I’m pretty heavily in favour of this approach, not because I disagree with the usage arguments brought up so far, but because I don’t think that this should be forbidden at the level of the type system. Using version 1 the definition of A & B wouldn’t just be “the set theoretic intersection of A and B” or “The meet of A and B” but rather “The intersection of A and B when the typing spec thinks that is a reasonably useful type, otherwise undefined”. I don’t think that a fundamental typing feature like that should implement a linting rule.

Doing that not only makes the theoretic foundation of the type system more complex, it also affects a lot of downstream features. For example, this function:

def test_subtype[S, T](val: object, class1: type[S], class2: type[T]) -> TypeIs[S & T]:
    return isinstance(val, class1) and isinstance(val, class2)

can no longer be annotated like that. I don’t think that the type system should really care whether there’s reasonable objects that actually make this function return True. Its purpose is to tell us what values can ocurr where, whether those values are what the programmer intended is much better checked in a linter (or optional rules for type checkers, which effectively are linting rules).

25

Well, it would help if there was an agreement to have different categories of rules for typecheckers within the type system.

The pragmatic purpose of a type system is to statically check the program for errors and violations of expectations detectable via type theory.

No, it wouldn’t be. It would be changing what it means to be a valid subtype, and the result is still the set-theoretic intersection, just resulting from the new definition of a valid subtype.

Under definition 1, that function can be implemented like that. You wouldn’t have a class where it ever gives the wrong result unless you type ignored an invalid class definition. (and the moment you type ignore base definitions, all bets are off on what the type system says)

With definition 2, it’s also still implementable, but the behavior would diverge across typecheckers, with some warning on that when detectable at the intersection and some not.

I’m really hesitant to reccomend an “optional” rule here, but I’m trying to find a way to make sure intersections are easier for users to end up with useful results.

1 Like
26

Oh ok, I misunderstood the idea then. Just to make sure, version 1 would say that even in this case:

class A:
    def f(self) -> int: ...

class B(A):
    def f(self) -> Never: ...

we get a type error because B isn’t a valid subtype of A?`

In that case, what part of your example here would error and what would the error be?

If we say that subtypes cannot have methods that return Never, then A & B wouldn’t be an error automatically, it would just be equivalent to Never, right? Annotating a function argument with Never is currently valid (if somehwat useless most of the time).

27

Yeah, this case is an error under option 1. Under option 2, it’s an optional warning. I lean toward option 1 for it’s consistency, as well as that this is a small shift in a direction that enables effect typing to be reasonable to implement in the future, but I offered option 2 in case there’s a reason I missed on why option 1 would not work for python, typecheckers, or existing libraries.

Under option 1, there’s no error at this location, and A & B is possible to reduce to being equivalent to Never, but a typechecker would not be required to do that reduction. (Checking all intersections like this, rather than only observed concrete types would increase computation required)

Under option 2, the subtyping rules are unchanged, and there is a detectable case where the intersection is likely a mistake of some kind, and an optional to implement warning would notify here something along the lines of “Warning: A and B appear to be impossible to satisfy in a useful way simultaneously due to method foo”

Option 2’s recommended warning (notably, not a type system error) rather than change of rules is something we don’t have a real existing language for with the specification, but working through some examples, it became clear having such warnings would make using intersections much easier for users if we aren’t okay with changing subtyping here.

28

Thanks for the explanation, I get it now.

I agree that it’d be great if there was some mechanism that told users if A & B is most likely not what they mean. I also see the problems with the warning version 2 wants to create just not really being a thing in the typing spec currently. But I’m not sure if version 1 actually improves that situation.

If we modify the subtyping rules like that the places where users actually see that as an error directly is when they manually write a subclass with a somewhat odd function signature. I think that most of those cases are likely to be intentional. The situations where these subtypes are likely to be accidents is when they are implied by an intersection, but there the users will only get an error if the type checker correctly reduces the intersection to Never and if the variable is then used in some way that is incompatible with that, likely with an attribute access. I.e. it’d be something like this:

def func(var: A & B):
    other_func(var)   # this produces no error
    var.attr          # something like "error: intersection is empty"

Is that an actually helpful error message and location? I think that for this kind of error to be understandable by most users, it would have to be at A & B and it should occur regardless of how the variable is then used in the function.

29

Well, we could go with a mix of both options, but I wanted to keep it optional if evaluating it for all intersections due to computation time. I’ll give this some more thought, and I appreciate the perspective on this point.

typecheckers that have rules for detecting unreachable code would already have to implement the reduction under option 1 as well when that rule is active, it’s just not a type error to have something equivalent to Never as a function parameter. Maybe that’s an indication that not having the warning under option 1 at the intersection is already not saving computation for most users?

Keeping in mind that the following is still allowed:

class A:
    def foo(self) -> int:
        return 1

class A2(A):
    def foo(self) -> int:
        raise SomeError  # raising is still always possible, even with a declared return type

    def bar(self) -> Never:  # not overriding a method with a non-never return type
        raise SomeError

I don’t think this rules out any useful cases that aren’t using Never to reconcile unreconcilable interfaces.

30

But, under type theory, Never is a valid subclass of int (and all other types). By LSP, this should be allowed.

But then, if you were to call A2().foo(), you lose that subsequent code is unreachable, which is a useful feature.

Since that happens in type checker land, I think it would be easy enough for them to have some internal “unreachable” marker that behaves the same as Never except it’s not used for intersections.

I also know there’s been complaints that the unreachable code is not typed checked, so errors slip in there (i.e. return Exception instead of raise Exception). If there is a different type of Never/unreachable, then the type checkers could type check those blocks.

31

How much of python’s typing system is actually based on type theory? Asking out of genuine curiosity, because there are some assumptions of the typing spec that are a bit “dubious” (or rather, of all the things I’ve explored, only one in particular I find dubious)

32

It’s completely possible to formulate a rigorous type system where Never is a subclass of int, but B isn’t a subclass of A. Also note that the Liskov substitution principle only is a requirement in one direction, it says that if S is a subtype of T then certain properties that objects of T have must also be shared by objects of S, but not necessarily the other way around. Or in other words, it only stops you from having badly behaved subtypes, it doesn’t require that nicely behaved types actually are recognised as subtypes.

This also already is the case in Python. In this example:

class A:
    var: int

class B:
    var: int

The two types share exactly the same properties, but they are not equivalent types because Python classes (that aren’t protocols) also need to be explicitly declared as subtypes.

I’m not sure if it’s possible to put an exact number on it, but I’d say a good amount. A lot of (especially older) features are set up somewhat adhoc and primarily out of a practical consideration rather than some theoretical thought process. But more recent features generally take care to adhere to a solid theoretical foundation and there’s been a lot of effort put into formalizing the older features and bringing them under the theory umbrella.

Some features also are “broken” when viewed under some type theories but perfectly fine under others. For example, in a lot of type theories the subtyping relation is required to be a partial order, which Any breaks. But by using a gradual type theory we don’t have that restriction and Any works perfectly fine.

From what I can tell, the question we need to be asking here isn’t whether this change to subtyping rules is fine from a theory point of view because it would just define Python to use a slightly different type theory than before. Rather, the question is which version of the type theory we want to be using.

1 Like
33

How about this:

This stays valid because it has always been valid and seems useful as Guido noted:

class A:
    def f(self) -> int: ...

class B(A):
    def f(self) -> Never: ...

Independent of that, the following intersection becomes an error:

class A:
    def foo(self, x: int) -> int:  ...
class B:
    def foo(self, x: int) -> str:  ...

type AB = A & B  # type error: intersection of A and B not possible

Because the rules for allowed intersections don’t have to be as permissive as is at all possible. It’s fine to forbid something that’s technically possible, simply because it’s confusing. I would really rather not mess with existing assignability rules.

Relatedly, I don’t really think this should be allowed either:

class C:
    def foo(self, x: int) -> int:   ...

class D:
    def foo(self, x: str) -> str:  ...

type CD = C & D  # error

Yes it can be satisfied by this:

class CAndD(C, D):
    def foo[T: (int, str)](self, x: T) -> T: ...

but that seems like way too much work for type checkers to figure out (consider also cases with multiple arguments, for example). I think it’s reasonable to require that the user spell out the common subclass explicitly.

I’d just go with a simple rule: “if the return types of methods are incompatible due to disjoint bases, no intersection is possible.”

Such a restriction can always be lifted later if it turns out that this is actually overly restrictive. (Such later lifting of restrictions has happened many times in the typing spec. What’s always painful and controversial, on the other hand, is adding restrictions later.)

34

I won’t be proposing intersections under that. Intersections should follow automatically from subtyping rules, and there’s various reasons to change the subtyping rules for functions and methods when it comes to evaluating resulting return types[1] involving intersections and overloads, and there aren’t practical reasons to restrict the C & D case.

  1. I didn’t include the details here, but this significantly improves solvability of return types to the point where it becomes fully decidable scaling in linear time with the number of intersection operands, rather than being undecidable in many cases, including two of the motivating cases. ↩︎

2 Likes
35

The pattern Guido noted is fundamentally type-unsafe though.

If someone[1] has created a function for lists (your type A) and you want to pass in a stack (your type B), the type checker cannot tell you whether this will succeed.
You just have to try, and see whether the functioncall crashes.
(And that’s fine in my opinion. Noqas exist because sometimes type-unsafe techniques are useful. But the noqa also acts as documentation that points to the core issue.)

My initial thoughts for creating the stack class would be to create a Protocol for stacks, then just use lists in production. There’s no need to disable methods that will be prohibited by the type checker anyway.
With that solution the type-checker would prohibit passing a stack into a function that is designed for lists, and hopefully when the type-checker figures out there’s a problem there you can find a good solution involving either unit tests or run-time validation.

  1. a library outside your control ↩︎

5 Likes
36

It’s runtime-unsafe but not technically type-unsafe (at no point does the type checker assign a wrong type to any value).

But I admit your protocol plan is better.

37

Python’s type system isn’t sound. As a result, the term “Type-safe” is a bit loaded in discussions where the underlying rules of the type system are the issue at hand.

Going to the example of using a list as a stack by subclassing and adding new error conditions, this violates substitution, it just does so in a way not all type systems model.

list.sort() performs an in-place sort so long as the list contains items that are partially orderable, and no errors external to the logic of the program are thrown (ie. signals, resource limits, hardware faults).

Changing the conditions for an error to increase the cases in which an error can occur is a violation of substitution, and many type systems reject doing so. As it is, python doesn’t, but that doesn’t mean a subclass is “type safe”, just that the current expressible type system allows it.

Using composition rather than inheritance allows doing this without such a violation.

Type checkers don’t have to do any significantly new work here. They don’t need to determine how a user might implement such a subclass, just that one could exist. The checks required for this already exist as part of overload resolution, with only a minor change at one step that doesn’t introduce new functionality needed for typechecker logic.

3 Likes
38

Thanks for the initial feedback from everyone who participated.

I think I have a good direction to propose from here that will be closer to option 1 for the subtyping change, but with some additional nuances to help adress points raised here.

I think I’m going to have to hold on on fully specifying isinstance behavior, but I will still include that isinstance is not equivalent to an intersection in the proposal, as well as include reccomended typechecker behavior while leaving the end result up to typecheckers. I will want to revisit this later, but it doesn’t need to be a prerequisite for intersections that it is fully specified.

Any discrepancies possible for typecheckers that don’t follow the recommendation (whether at all or only initially), will be possible for those typecheckers to handle between them and their users without it making public apis diverge.

4 Likes