Pulse check on Intersections draft work

Typing
1

I’m nearing readiness to start working on finding a typechecker to work with on a reference implementation + a PEP proposal.

I’d like to check with the community to make sure the behavior of 2 specific cases is something they don’t have issue with before pushing through the final stretch.

I can’t guarantee I won’t just put the objection in a “rejected alternatives” section, but I’d at least like to be aware of any objections and consider them properly in case there is reasonable room to do better.

I’d like to make a change to assignability and subtyping semantics.

Right now, the type system does not differentiate between Never, as a result of logical exhaustive negation (ie, case match or isinstance chaining) and Never, as a non-return effect from a function.

This difference doesn’t generally matter for most subtypes, but if intersections where to be user expressible, one can imagine cases where intersections shouldn’t be used due to incompatible return types of methods, yet could be “satisfied” by just making the method always error instead.

This is a “hole” in the expressibility of the type system.

There are two ways to handle this that will prevent issues.

  1. Methods of subtypes must be capable of returning a value if the super type’s corresponding method can return a value.

  2. Recommend a warning for typecheckers to implement that is not mandatory when detecting such subtypes, as well as intersections that provoke the need for such subtypes.

There is also the option to “do nothing” for now, and just trust library authors not to create such situations for their users.

While I personally lean toward option 1 here as it paves the way to better handling of Never, and potential future extensions of the type system toward supporting typing effects, I’d be fine with the second option.

The “do nothing” option is one I will reject for any initial proposal here unless this is an absolute deal breaker for typecheckers or important libraries

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


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


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

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

def should_error_or_warn(x: A & B):  ...
    # A.foo is (int) -> int, B.foo is (int) -> str, 
    # there is no definition of foo for A & B that satisfies both without removing
    # the ability of the method to return a value.
    # this is asking a caller to create a suspiciously defined subtype

def allowed(x: C & D):  ...
    # Because C.foo and D.foo's parameters are disjoint, the disjoint return types can be mapped soundly

I’d like to make a change to isinstance semantics.

Right now, isinstance is treated as a “pseudo-intersection”. I don’t think this is the right long-term option.

I’m fine if the answer to this is “This isn’t a big enough issue” or “this is a pre-existing problem that can be solved separately”, but if there’s enough appetite to make the change at the same time, I believe it is an appropriate improvement to make as an associated change at the same time, and I am willing to ensure that the reference implementations provided have this change as well.

Proposed change:

Instead of treating the type being checked as having the default generic (ie list in isinstance(x, list) being list[Any]), the semantics should be understood to only narrow on the outer type, given the actual behavior of isinstance at runtime.

eg:

def foo(x: Sequence[int] | int):
    if isinstance(x, Sequence):
        reveal_type(x)
        # `Sequence[int] | Sequence & int`, not `(Sequence[int] | int) & Sequence[Any]`

Here only the outer type has been checked. Treating this as an intersection would actually widen the type, rather than narrow it, which is both counter-intuitive and not in line with the behavior at runtime.

This is effectively a limited user expression of existential types. I am not proposing a generalized user expression of this, General expressibility can be done separately in the future as a way to improve expressibility of things like TypeIs functions.

Some type checkers may already effectively be behaving in this way, but I’d like the language to be in the specification if possible so that users do not expect intersection behavior from isinstance

13 Likes
2

I have checked on the intersections discussion a while ago but haven’t been able to catch up thoroughly. I have some minor clarifying questions, apologies if they’re very basic:

It sounds like the latter meaning would better fit the NoReturn spelling, right?

Since intersections aren’t a feature in the current system, but you’re arguing for a specific change to go along with a proposed version of intersections, I’m not sure how to really interpret this statement. Or to read the assumed semantics in your example with the & operator. I guess you’re implying there’s a possible version A of the draft proposal that provides the intersection feature without this requirement of “consistent-returnability”, and a version B with both, and you’re describing problematic cases in A that are avoided by B? Since the new rule would affect existing code, it’d be helpful to include such an example.

It seems like you’re proposing a new type of entity (related to “existential types” which I’m not familiar with), since that’s required to define how Sequence[int] | Sequence & int works with Sequence meaning ~something~ other than Sequence[Any]. That feels like a much bigger point to me than tweaking how the new intersections relate to isinstance checks, so I’d suggest framing the point that way - e.g. the title should be something like “New category of type object: ‘outer-only’ generics, to reflect isinstancechecks”. And I assume folks would ask if there’s any interaction those with the rest of the type system that might need to be specified.

Thanks for continuing to push forward on this hard problem!

3

Oops, I could have been more specific there. The result Sequence[int] | Sequence & int comes as a result of a definition of isinstance that can be better expressed by existential types, but is not included here. It does mean Sequence[int] | Sequence[Any] & int here, I have no intention of changing the general case of SomeGeneric without specialization, this is a unique special carveout for the 2nd parameter of isinstance for now, with room to do better later, covering only the place in the standard library where it will come up naturally.

There are ways to accurately reach the same result via a series of programatic steps without implementing existential types internally by a typechecker.

(re: rule on subtyping change)

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

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


class Opt1Error(A, B):
    def foo(self, x: int) -> Never:  # currently allowed
        raise TypeError


def if_opt2_should_warn(x: A & B):  ...
    # A.foo is (int) -> int, B.foo is (int) -> str, 
    # there is no definition of foo for A & B that satisfies both without removing
    # the ability of the method to return a value.
    # this provokes the need for a user defined subtype that is "suspicious"
    # for this function to be called.

Maybe, but I’m hesitant to try and differentiate between these without actually defining effects as anything more than something inferable from the location and use of Never. The distinction between the causes of having Never I’m looking for doesn’t require users to change how they write Never to NoReturn, it can be detected entirely by where and how it is used

There’s a potential for distinctions to be more useful with more effects defined, but in that case, NoReturn loses its value, as you’d then specifiy NonTerminating, Raising etc.

4

This doesn’t look quite right from what we’ve talked about offline.

Sequence[int] | Sequence[object] & int is, but choosing the specialization here as object only works because Sequence is a covariant container. Avoiding widening the type via Any is less obvious if you swap Sequence for list in the example, as that requires & list[*] (using * as a placeholder here).

This isn’t an unknown concept, but you do need to spell it out in more detail when you propose it and avoid accidental lazy shortcuts that aren’t correct.

I agree with the proposed change if you can manage that.

1 Like
5

The use of Any there is wider than necessary, but also unlikely to cause issues and doesn’t require a new concept. I intend to propose it with Any, while also noting a more precise option typecheckers may choose to implement to reduce the friction of implementing this. I think this is a place where gradual improvement is the best course.

Working this out further:

def foo(x: Sequence[int] | int):
    if isinstance(x, Sequence):
        for value in x:
            # value is now known to be `int | object`, using Any results in `int | Any`
            # intersection would have resulted in value being `int & Any`
            foo(value)  # Accepted, but actually unsound
            value.foo()  # proposed change errors here even with Any, strictly intersection behavior allows this
6

This bit highlights how to avoid such a problem, as well as where the differences would be on false negatives caused by isinstance introducing Any

def problem_avoidance(x: Sequence[int] | int):
    if isinstance(x, int):
        reveal_type(x)  # (Sequence[int] & int) | int
    elif isinstance(x, Sequence):
        reveal_type(x)  # Sequence[int] & ~int
    else:
        assert_never(x)


def covariant(x: Sequence[int] | int):
    if isinstance(x, Sequence):
        reveal_type(x)
        # Known: Sequence[int] | Sequence[object] & int
        # Best with current + intersections: Sequence[int] | Sequence[object] & int
        # Probably acceptable with current + intersections: Sequence[int] | Sequence[Any] & int
        for value in x:
            covariant(x)  #  problem is caught if Any isn't introduced by isinstance
        
def not_covariant(x: list[int] | int):
    if isinstance(x, list):
        reveal_type(x)
        # Known: Some list assignable to `list[int] | int`
        # Best with current + intersections: list[int] | list[Any] & int
        for value in x:
            not_covariant(x)  #  Needs a new concept to catch the potential problem
7

I may be missing something (I once assumed Intersection would be easy, which it clearly isn’t :-), but this appears to forbid a useful pattern where a subclass can disable a method defined in a base class, by overriding it as always raising an error.

For example you might want to define a stack by subclassing list and disabling sort, insert and remove (and modifying __setitem__, __delitem__ and pop).

2 Likes
8

I’m not sure I fully understand your two options. However I generally think that type checkers should error at A & B. I think most users don’t actually want that intersection.

In my personal opinion the case of C & D should also be disallowed by intersections and flagged as not possible. I think this is how Mypy currently does it in isinstance(some_c, D).

I’m generally not a fan at all of these fancier intersections that are theoretically possible, but questionable from a practical standpoint. I’m aware that some subtype can create this kind of type with overloads, but why do we ever need this type of intersection?

I’m really excited to finally have the ability to intersect protocols and mixin classes. We obviously need to look at the cases you present (and thank you for that!), but I also think we should limit some of those cases, because they are too complicated for the average user.

Since isinstance semantics aren’t defined by the typing spec, they vary a lot across type checkers. So I think unifying them makes a lot of sense. In your specific example Mypy reveals Sequence[int]. If x were int it would reveal __main__.<subclass of "builtins.int" and "typing.Sequence[Any], which is Mypy’s way of intersections and means int & Sequence[Any].

I personally think this is very useful from a practical perspective. There are sometimes pretty large unions and having Mypy’s isinstance implementation pick the relevant union members is useful. I would want to avoid to avoid a type like Sequence[int] | Sequence & int | Sequence & str | Sequence & float | ..., which is very hard to understand especially for people that are not very experienced with type systems.

9

Whilst the type of C & D might not be immediately obvious, to me it was pretty clear after only a few seconds of thinking about it. And restricting it seems more annoying than not? Especially if it’s restricted internally as well as just for users.

On the other hand, I agree here - I see this a lot in ty output and it’s a pain.

1 Like
10

There’s not really a way to avoid such inferred types when dealing with narrowing if striving for both accuracy and soundness. I don’t expect users to need to write out large expansions manually.

We could change how the information is presented, but that’s a tool choice.

We could also come up with shorter notation based on the operations rather than the result:
something like: Sequence[int] | int, +Sequence

I’m not prepared to propose new notation just to shorten revealed types that get a bit weird because of python having a mix of features that makes it more complex to accurately capture, but if anyone wants to take the above and run with it, feel free.

Well, mypy would be wrong there.

T = TypeVar("T", int, str)

class E(C, D):
    def foo(self, x: T) -> T:  ...

Some of these examples may look like “toy examples”, and they are. They’ve been simplified to get to the heart of the behavior, and I’m not intending to argue merits, that’s been done already and various motivating use cases need an answer on what will and won’t be allowed.

Every point I’ve brought up has come from working through various motivating examples for intersections, and making sure that someone could read the proposal and understand how that motivating use case would be improved or enabled by having intersections, and the expected resulting behavior.

1 Like
11

I have encountered many use-cases for this, for example in optype there are the CanRound1 and CanRound2 protocols that intersect to CanRound:

This is even mentioned in the docs:

[…] Additionally, optype also provides their (overloaded) intersection type: CanRound[-T, +R1, +R2] = CanRound1[R1] & CanRound2[T, R2].

Similarly there are the optype.CanPow* protocols:

(docs)

3 Likes
12

Is your hope to entirely ditch class CanRound and write it as type CanRound[...] = CanRound1[...] & CanRound2[...]?

13

Yes exactly.

14

It would forbid that, yes. This gets into the question of if replacing an expected working method with one that always errors is actually satisfying LSP just because we’ve modeled the type system in such a way that we can’t differentiate a raised exception from “invalid use”, from functions that are designed to never return (infinite loops, exception handlers that always reraise, etc), with the fact that we expect “errors can always occur”, because exceptions can come from external sources (eg memory allocation failures), and that we don’t have effects only Never, which is always the absence of a value, but says nothing itself about the conditions that caused an absence of a value.

All of these are actually distinct cases, and it’s my opinion that the more useful interpretation is that functions/methods that must always error should not be seen as a valid replacement for ones that are expected to produce a useful result. There are some significant downsides to treating this as a valid replacement when evaluating method return types that involve intersections.

If the concern is how to effectively reuse part of a type without this, for the specific case, you can get some amount of static enforcement of “use as a stack” by defining a protocol that only contains the parts of the interface intended for use, and ensuring that’s the seen type without needing to create erroring methods, or you can wrap access to an underlying list without subclassing list, or use collections.deque as a stack, which is probably the best of these options.

This does generalize:

  • Only expose the API you want used, even if the type has a broader API
  • Implement it by composing behavior, rather than by inheriting it.
  • Use a more appropriate data type
15

Agreed that a protocol is probably the best way to do this.

My concern is more that this may be a common pattern that currently works and type-checks. So making this a general rule (not just one when intersections are involved) could break existing working code.

I’ll drop my objection if someone shows a plausible search showing this pattern isn’t used or is very rare.

1 Like
16

I don’t know if there’s a reasonable way to check this without first implementing the rule, and even then, only for code that’s public. It’s not enough to do any sort of astgrep like search, as return typed as Never in a subclass would only be flagged if the parent type declared the same method with a non-never return type. Could probably hack together something later.

Even if it is an existing pattern, there’s then the question of if it’s an existing pattern we should support.

I don’t consider making the type system more accurate breaking, if it was correctly working code, it continues to be. Though I do get that it still isn’t a free change and that users will have to either add ignores or change the types to get their typechecker into the previous accepting state.

2 Likes
17

If it does end up a problem as a general rule, you could modify this option to only an optional warning on intersections that provoke this case. It would still prevent the case we discussed of library authors accidentally asking their users to combine logically incompatible interfaces.

1 Like
18

@mikeshardmind how would something like pathlib fit into this?

A lot of the guards in that module wouldn’t be recognised by Version and platform checking - so would they be considered “always errors”?

19

No, these aren’t typed as always raising. In this case, the stubs reflect the reality better.

Additionally, as it’s still fine to always raise from a function typed as returning a value, this would be fine to inline the annotations by typing __new__ here as if it was to succeed.

What this prevents is a case like:

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

def func(x: A & B):
    ...

# user attempt

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

func(AB())

The mechanism of prevention here is that because int and str are disjoint types, only Never is a suitable return annotation, and (A&B).foo can never be expected to be successful.

There’s nothing stopping this definition:

class A2(A):
   def foo(self, x: int) -> int:
       raise SomeException 
       # still fine to raise in a function typed as returning,
       # though this is still a pretty suspect subclass IMO

But this definition wouldn’t be possible to pass as compatible with A & B

3 Likes
20

This being allowed may have been lost in how you presented the original post.

Adding some context from discussion elsewhere, this is acting as a small guard-rail to prevent users from going down a rabbit hole and just telling them they have incompatible demands. The actual interactions with Never being less than fully expressive are larger than this, but this was what was the smallest set of behaviors we had discussed that still helps users stop before they get down the rabbit hole rather than realize later there was an issue.

The only case that would create new places an ignore is needed rather than just changing the return annotation is preexisting multiple inheritance with overlapping method definitions with disjoint return types that were replaced by a method that always errors. Actually disjoint types aren’t all that common, or would already involve forbidding subclassing if typing.Final was the reason for disjointedness.

4 Likes