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

6 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 `int | Any`, which has the "safe usable interface" `int`
            # intersection would have resulted in value being `int & Any`, which is some gradual type with a bound of `int`
            foo(value)  # fine
            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