Revisiting variance

Typing
21

I don’t see how this is supposed to work. If we have

type AnySequence[T] = Sequence[T] | MutableSequence[T]

def foo(seq: AnySequence[int | None]): ...

mylist: list[int]
foo(mylist)

For mylist to be assignable to the union AnySequence[int | None], it has to be assignable to one of the elements of the union, either Sequence[int | None] or MutableSequence[int | None]. According to the assignability change you propose (if I understand it correctly), list[int] would not be assignable to Sequence[int | None], because their variance differs. It’s also clearly not assignable to MutableSequence[int | None], because MutableSequence is invariant in its contained type, and int is not equivalent to int | None. What am I missing that would allow list[int] to be passed to foo in this case?

That’s a matter of perspective. I think that a TypeIs function that (for example) checks all elements of a sequence and narrows Sequence[object] to Sequence[int] is a “correct TypeIs function.” The safety problem is with the shared mutability of the underlying object, not with the correctness of the TypeIs function. The same safety problem applies in other narrowing cases (attributes, individual container elements, nonlocal) where type checkers also choose to narrow even though shared mutability makes it unsafe. It is true that TypeIs, by allowing users to expand their application of type narrowing, gives users more potential exposure to the unsafety of type-narrowing. I think this should be made clear in the documentation. Jelle’s PR is a good start.

I appreciate this point, because I think it puts the focus on the real root issue, and it’s a position that I sympathize with (and would have held myself a few years ago.) But this is one of those rare cases where we actually have something approaching a controlled experiment and empirical evidence on the effects of a proposed change to the type system. Pyre tried the approach of refusing to type narrow anything that might be mutated between the narrowing check and the use, and instead requiring authors to first pull it out as a local before narrowing it. The audience of Python authors was perhaps as favorable as one could find for this kind of experiment: professional software engineers, all working for the same company, with a team of people working full time to maintain the type checker and educate them about its use. And the result of the experiment was pretty clear: developers did not like this behavior, and they didn’t understand it. There was a never-ending stream of people complaining about Pyre failing to understand their clearly-correct code, and many of them just assumed the type checker was buggy and used cast or type-ignore comments to work around the lack of narrowing. The result was that the Pyre team changed course and went back to allowing some narrowing that is not necessarily safe with concurrent mutation.

It doesn’t address the “specific issue” of narrowing mutable things. It addresses only part of it, the even more specific issue of narrowing generic types. It doesn’t address the unsafety of narrowing attributes or individual container elements, which major type checkers currently do, even though it’s also unsafe in exactly the same way and for the same reason.

Well, that’s fair. I do think adding strong immutability or ownership to Python would be a very difficult lift. And I do think the status quo, with some unsoundness, is practically better than some attempts to fix it would be.

I think better soundness could be reached here fairly “easily” (and with better consistency than the variance change) by just being way more conservative about where narrowing is allowed. But given Pyre’s experience, I don’t think this would be very popular with users, and I doubt any of the type checkers will be eager to try it. It may be that something closer to Pyre’s current middle ground (where it will narrow e.g. mutable attributes but discard the narrowing as soon as it sees something “likely” to trigger arbitrary code execution elsewhere, like a function call) would be more tolerable: I’d be curious to hear if the Pyre team has thoughts on how well that’s worked out.

3 Likes
22

Thanks for the history about pyre there. I find it a little disheartening that even in that setting, people thought the type checker was wrong. There’s more on the other parts I need to think about more before responding to them, but I do think I might be able to clarify how this would be possible to work.

I spent more time trying to point out the variance issue to people who were saying it wasn’t one, than explaining how this would work, but it would require additional changes to TypeVariable calculated variance as well, which was at least noted briefly above.

type AnySequence[T] = Sequence[T] | MutableSequence[T]

In particular, this would allow type checkers to decouple the variance presented to users from the variance calculated in the function body, and how that is allowed to use it, because a function accepting this type is forced to remain compatible both with invariant and covariant use here.

The end result here would be that in this scenario, the user is allowed to pass in Sequence[T] or MutableSequence[T], and T may be covariant or invariant in the process. Inside the function body however, any operations which would rely on T being covariant, even if narrowed to Sequence[T], would not be allowed. It would also mean most uses of Sequence[T] would need to be replaced with the AnySequence[T], because passing AnySequence[T] to a function expecting Sequence[T] would then be a mismatch (as the T from AnySequence may be invariant, but Sequence[T] alone only presents covariant use and does not claim to be compatible with invariant use of T), so there would still be some churn and friction to adoption even if we could somehow ignore the cost of implementation itself, which we cannot.

Tracking the possible variances as a separate term and only allowing any combination of variances/types that remains valid will also prevent other issues down the line for anyone working on better support for function composition with both covariance and contrvariance, and HKTs if they ever are worked on with contravariance, but I’m not sure that it’s easy to demonstrate this one without an agreed-upon framework for HKTs in python, it’s pretty deep in the theory weeds. [1]

Perhaps this is “too clever” and not obvious enough, but such a decoupling would prevent the function body from doing something that relies on covariance when wanting to allow containers that should be treated invariantly, and for most users, this would be transparent, with the specific issue only coming up in a narrow case visible only to the function body author, but I’d much rather be spending time in discussions like these exploring options like this that could have a possible solution than arguing if it’s even a problem when a problem has been clearly demonstrated, because without discussing the pros and cons of possible solutions, people are (seemingly) presuming that any fix here would be too disruptive and (at least from my perspective) are trying to frame it as not worth solving because of the existence of other similar issues.

  1. There’s an interesting case study with how rust uses higher-order functions and encodes lifetimes using subtyping and variance rules to draw a parallel with, as well as to show that it’s a detectable problem from type information (there’s an open bug where rust gets this wrong in a case involving contravariance, but miri catches it) but this is not easy to relate to what we have in python without a stronger theoretical foundation to be discussing it from. ↩︎

1 Like
23

It’s not a matter of perspective at all. The current rules prevent it from being correct, and the below example shows that current type checkers definitely understand that this isn’t safe, it’s just the variance and being able to erase invariance which is a problem here

Code sample in pyright playground

from typing import Sequence, MutableSequence
from typing_extensions import TypeIs

def outer_allowed_unsafe(x: Sequence[int | str]):
    if unsafe(x):
        x[0].as_integer_ratio()

def outer_doesnt_narrow_unsafely(x: MutableSequence[int | str]):
    if unsafe(x):
        x[0].as_integer_ratio()  # error here
        
def unsafe(s: Sequence[object]) -> TypeIs[Sequence[int]]:
    return all(isinstance(x, int) for x in s)


def detected_unsafe(
    s: MutableSequence[object]
) -> TypeIs[MutableSequence[int]]:  # error here
    return all(isinstance(x, int) for x in s)

def issue():
    x: list[int | str] = [1, 2, 3]
    outer_allowed_unsafe(x)
    outer_doesnt_narrow_unsafely(x)

Is the argument here really that the type system should be unsound because soundness is unpopular? Shouldn’t the specification cover what is sound, and then if a type checker doesn’t want to implement it or users don’t like that rule, they either don’t implement that rule or users disable a rule they want to deal with? The logic that follows from this as a reason not to fix it means there’s no way to provide soundness here in a specification compliant way because the established type checkers wouldn’t want to.

Just split Sequence and MutableSequence so that one doesn’t inherit from the other, make variance matching a requirement of subtyping. Simple, effective, fixes this and the future problems it could cause, the union of Sequence | MutableSequence then works in the obvious way and isn’t “too clever”.

TypeIs is a higher order function type already. It’s a function type that operates on information about the types of values, rather than values and that this is why this is why the variance issue is an issue now and hasn’t been before. This will be more of an issue with more things that do higher order operations, and this isn’t the only new one of those. TypeForm is also in progress here.

24

I don’t think this is simple (or effective, but that’s another matter) at all. It would break so many perfectly reasonably pieces of existing code. Many classes have children that add methods in ways that change variance. And basically the entire point of Sequence and MutableSequence is that Sequence is a parent of the second, AnySequence would not be usable the way Sequence currently is.

I can appreciate the effort to make the type system catch as many bugs as possible. I also really like more esoteric things like Rust’s burrow checker or the many fancy language extensions to Haskell. But I think we also need to keep in mind that Python is a highly dynamic and originally untyped language that doesn’t have those same goals. Rust’s goal is to guarantee memory safety (unless a block is marked as unsafe), it seems that your goal is to have Python’s type system be as strict as possible. But that doesn’t really seem to be what most Python users and other devs here have in mind. So yeah, the type checker not catching a potential bug because doing so would be unpopular is a perfectly fine stance to have.

I think that if something like this were to move forward it would have to work in some way that has extremely few false positives. Just blanket banning subtyping when the variance of a type variable is changed is too broad to be palateble to most Python users. Though this is just my read of this thread, I am not a super involved long time contributor to Python so my thoughts here may be entirely misguided.

4 Likes
25

Good, it should break that code. It’s easy to frame this as a problem with TypeIs, but it isn’t. It’s a problem of having features that rely on variance while not requiring consistency of variance.

The other option is to remove TypeIs and prevent any form of HKTs from ever being accepted into the language.

It’s a gradual type system that isn’t enforced at runtime. It shouldn’t be about if it’s “popular”, the goal should be to describe the language. If people don’t want to adhere to it, they don’t have to, and can leave the parts that are too hard for them untyped.

This also isn’t about making python as safe as rust. I have no issue with people using Any, cast, or type ignores. I have an issue with things that are badly specified without considering the foundation they have to be built upon. TypeIs should not have been accepted with this pre-existing issue.

People can’t have their cake and eat it too here. You can’t add higher order functions that rely on variance to a language’s type system and at the same time say that variance can’t be relied upon.

26

The goal of tracking the variance separately (despite that it feels like it might be “too clever”) was precisely so that the existing uses wouldn’t be broken and only the new uses involving anything relying on variance would need to handle that.

I don’t agree with the specific expression there, but I do agree that TypeIs probably shouldn’t have been accepted without addressing this, especially since the authors were clearly aware of the potential here with stating that the resulting type should be an intersection with the original type.

27

Maybe I misunderstood. I thought that your proposal would mean that things like this would no longer be correctly typed code since it creates a subtype with different variance than its supertype:

class Parent[T]:
    def force_covariant(self) -> T: ...


class Child[T](Parent[T]):
    def force_contravariant(self, value: T) -> None: ...

You also said that a list[int] object would then not be assignable to a variable declared as Sequence[int]. That certainly is a very common use case that would then not be allowed.

1 Like
28

With what I proposed, paired with other things that could keep compatibility, such as defining Sequence in the typeshed using the AnySequence definition, but keeping the actual sequence definition available as something like typing.CovariantSequence, it could be done in a way that keeps current code working, but allows the expressibility needed to handle the new features (TypeIs was accepted for 3.13 and is the first feature in python’s type system to have a reliance on variance in this manner) safely

29

Ultimately, Python is designed by its community and even things like the SC are elected positions. Even if we don’t think that features should only be implemented if they are popular, that is how things do work currently. There certainly are many features that I personally would love but most other people wouldn’t and I don’t think that my ideas of what the perfect Python is should override other people’s preferences.

Can we not? I feel like my and other’s lack of concern of these specific bugs being found by the type system is very similar to your and Micheal’s lack of concern over bugs like the one involving a nonlocal variable being found by the type system. As you pointed out there are degrees to safety here and the currently specification of variances and TypeIs seems like a perfectly workable middle ground to choose.

1 Like
30

So the example I gave would still work as is? What is the idea behind Sequence (or CovariantSequence or whatever you want to call it) not being a superclass of MutableSequence anymore?

31

No, you can’t. TypeIs doesn’t make sense to have in the language if variance isn’t reliable. The following is identically safe in this context, so there’s no point to even having TypeIs other than to trick people into thinking this is safer than it is

def narrow(s: Sequence[object]) -> TypeIs[Sequence[int]]:
    return all(isinstance(s, int) for x in s)


def outer_one(x: Sequence[int | str]):
    if narrow(x):
        return sum(x)

def outer_two(x: Sequence[int | str]):
    if isinstance(x, Sequence) and all(isinstance(s, int) for x in s):
        return sum(cast("Sequence[int]", x))
32

I think you’re mixing people up. I’m the one who wanted to remove it as a superclass in order to keep it simpler.

33

With what I suggested (not with removing Sequence as a parent class of MutableSequence) there would still be at least a way to do it compatibly, but either the existing code would have do use AnySequence rather than Sequence, or we’d need some compatibility based definitions in the typeshed and new code relying on the variance would need to use that.

In the case of existing code changing, this would look something like

class Sequence(...):
    ...

class MutableSequence(Sequence(...)):
    ...

type AnySequence[T] = Sequence[T] | MutableSequence[T]
# same for mapping, etc

in the case of going out of the way to have the current name Sequence have the semantics of AnySequence for compatibility with existing code:

class _Sequence(...):
    ...

class MutableSequence(Sequence(...)):
    ...

type Sequence[T] = _Sequence[T] | MutableSequence[T]
CovariantSequence = _Sequence
# same for mapping, etc

Either of these specific options does require tracking variance of types separately from the types themselves, while still tracking it on the types themselves to reconcile the issue.

By contrast, @Liz 's option is more disruptive but easier to be correct about, though I would admit that there are other issues with the collections abcs and with structural types that could likely be packaged into a big typing2.0 fix to land at some future date.

There’s also the third option here, remove TypeIs, place a hold on accepting other things like it until we can untangle this. I do think TypeIs is catastrophically broken in the context of the current type system, and there hasn’t been a release with it existing yet, but we’re on the last beta now (we were much earlier in the process when this was originally raised as an issue…)

The fourth option of do literally nothing is always an option, but it doesn’t sit right with me here knowing this is no safer than a cast, there’s no reason to have it.

34

If people want to turn a list[int | str] into a list[int] they already can safely:

new_list = [x for x in old_list if isinstance(x, int)]

The variance issue is highlighting bigger issues with their code if they are mixing types in a mutable data structure, but wanting to narrow it to just one type.

I don’t think keeping a broken foundation around just because people are relying on it is a good thing. It just means they’re relying on things that are already broken, while holding back the ability to safely add features people want. This issue can’t co-exist with higher kinded types one of the most widely requested features for the language

35

As I said before and would appreciate if people would actually listen to and stop inverting cause and effect, this isn’t the root cause. It’s a currently observable effect. The variance issue existed before TypeIs, TypeIs exposed a particular case it could actually have a discernable effect on current parts of the type system

I can construct a case where it matters with only immutable containers, and without modifying references where the type system can’t predict it as well. (This is somewhat contrived, but I don’t do the kinds of narrowing that TypeIs allows, and TypeIs is the only place this can happen, so I had to construct a case using things I’d never personally write)

The root cause here is that variance should be part of the subtyping relation if there are going to be functions and types that rely on it, and this isn’t currently the case. TypeIs and other future additions are merely unearthing this problem, with the most obvious and least contrived version presenting like a mutability issue

36

I’m really trying to understand the issue you’re describing and your proposed fix, so please don’t take this as me derailing into another issue. But I don’t really see how your new example is related to variance at all. On my machine it errors on line 46, where you’re trying to merge an invalid flag value.

If you cut out the code that isn’t actually reached and simplify the rest more you end up with this (as far as I can tell) equivalent code that also breaks in the same way:

from typing import Any, Protocol, Self

from typing_extensions import TypeIs


class SupportsAdd[T](Protocol):
    def __add__(self, other: T, /) -> T: ...


class MutabilityIsADistraction[T: SupportsAdd]:
    def __init__(self, value: T):
        self.value = value

    def merge(self: Self, other: T) -> Self:
        return type(self)(self.value + other)


### demo


def unsafe_typeis1(collection: MutabilityIsADistraction[Any]) -> TypeIs[MutabilityIsADistraction[int]]:
    return isinstance(collection.value, int)


def indirection1(x: MutabilityIsADistraction[Any]) -> None:
    if unsafe_typeis1(x):
        x.merge("something")


def example() -> None:
    x: MutabilityIsADistraction[int] = MutabilityIsADistraction(123)
    indirection1(x)


if __name__ == "__main__":
    example()

From what I can tell the reason for the runtime bug not being caught by the type checker just is that you used Any. A Collection[Any] intersected with MutabilityIsADistraction[int] is a MutabilityIsADistraction[Any], or at least that is pyright’s current behaviour. This then obviously allows for unsafe operations since the merge call then doesn’t really get type checked.

37

The pep says that it should be an intersection consisting of

Collection & MutabilityIsADistraction[int] or Collection & MutabilityIsADistraction[Permissions] , depending on which TypeIs from the example. pyright was the reference implementation and is not matching what the pep specifies, which might be an additional reason to pull the plug on this before release?

This should reduce to either MutabilityIsADistraction[int] or MutabilityIsADistraction[int & Any] or not reduce at all (same for permissions) if following the rule about set-theoretic intersections.

It’s also ignoring a direct cast:
image

So we don’t have a type checker that implements this correctly to even discuss why “correctly” is incorrect and you can work it out by hand if you want. This is following all the rules laid out by the PEP, and will result in the wrong type if you work out the rules of the pep by hand…

3 Likes
38

Thanks for that example, that does appear to indicate a bug in pyright. Mypy and pyanalyze do handle a similar case correctly though (mypy Playground). I reported TypeIs does not narrow generics properly · Issue #8460 · microsoft/pyright · GitHub to pyright.

2 Likes
39

@Jelle I’ve taken @mikeshardmind 's example and moved it over to mypy-play which you’ve said implements it correctly I made a minor modification since on first attempt, mypy doesn’t appear to support the new generic syntax yet.

mypy also does not prevent the unsafe narrowing chain, and this is direct calls with no funny business with concurrency required.

1 Like
40

I’m not sure how that example demonstrates a hole in the type system; as far as I can tell it relies on the fact that constructing an IntFlag with boundary=STRICT can fail for some integers. But that’s not the sort of thing the type system can catch, just like int("not a number") is fine for the type system but fails at runtime.

Here’s a simpler example that is also accepted by mypy and fails with the same runtime error:

from typing import TypeVar
import enum

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

def xor(x: T) -> T:
    return type(x)(x ^ 74)
    
class Permissions(enum.IntFlag, boundary=enum.STRICT):
    none = 0
    a = 1 << 0

xor(Permissions.a)