Revisiting variance

Typing
1

I mentioned in another thread that:

but this hasn’t been a topic with much discussion around it. It’s on a list of things I’ve been tracking where python’s type system isn’t fully correct, and this lack of correctness has caused complications or unsoundness in other areas.

As of the acceptance of TypeIs, the soundness hole that exists here is now something that can cause a problem. This was previously framed as an issue with TypeIs . While I think there are other issues with TypeIs which will need addressing, I think this is not one of them.

The general form of the problem with TypeIs, taken from that thread:

The problem here is that Sequence is covariant, and the narrowing behavior is only safe with a covariant type. A list passed to this function results in unsafe narrowing

Fixing this in the least disruptive manner possible would be rather complex, and require determining when the variance is being relied upon and by whom. In the problem case, the variance is relied upon by the function accepting a sequence, but not enforced for things passing to the function.

It would be impossible to have such a minimally disruptive fix without tracking total program wide variance for variables, as the larger case from that thread:

shows that it would be possible to erase knowledge that a data structure was invariant in a scope in which variance isn’t cared about, and then later pass it to a function that relies on covariant behavior.

Fixing this in the simplest way would mean requiring variance to match for assignability, and would create problems for people using Sequence[T] when they mean Sequence[T] | MutableSequence[T], to allow Any sequence of T, not relying on the difference in variance

Any fix of this alone would not fix all of the specification issues around TypeIs or with Sequence[str] vs str, but is a relevant component to each of those discussions

1 Like
2

Is this actually an issue with variance or with objects being members of different types at different points in their lifetime? For example, this slightly modified example has the exact same behaviour and doesn’t use type variables at all:

import asyncio
from typing import Protocol, runtime_checkable


@runtime_checkable
class SomeProtocol(Protocol):
    value: int


class Thingy:
    def __setattr__(self, name: str, value: object, /) -> None:
        super().__setattr__(name, value)

    def __delattr__(self, name: str) -> None:
        super().__delattr__(name)


async def takes_object(x: object):
    if isinstance(x, SomeProtocol):
        await asyncio.sleep(10)
        print(x.value)


async def takes_thingy(x: Thingy):
    x.value = 1
    t = asyncio.create_task(takes_object(x))
    await asyncio.sleep(1)
    del x.value
    await t  # so that the error shows up if someone copy pastes this.


if __name__ == "__main__":
    asyncio.run(takes_thingy(Thingy()))

and so does this using a typed dictionaries instead:

import asyncio
from typing import TypedDict

from typing_extensions import TypeIs


class SomeTypedDict(TypedDict):
    value: int


def is_some_typed_dict(x: object) -> TypeIs[SomeTypedDict]:
    return isinstance(x, dict) and "value" in x and isinstance(x["value"], int)


async def takes_object(x: object):
    if is_some_typed_dict(x):
        await asyncio.sleep(3)
        print(x["value"])


async def takes_thingy(x: dict[object, object]):
    x["value"] = 1
    t = asyncio.create_task(takes_object(x))
    await asyncio.sleep(1)
    del x["value"]
    await t  # so that the error shows up if someone copy pastes this.


if __name__ == "__main__":
    asyncio.run(takes_thingy({}))

Really, at no point is any part of the type system or the runtime really wrong. When the object is checked for membership in SomeProtocol, SomeTypedDict, or Sequence[B], it genuinely does belong to those types. Similarly, when the outer functions modify the objects they do so completely safely as members of Thingy, dict[object, object], and list[A]. The problem here seems to come from assuming that the type of the object doesn’t change after the runtime type checks.

Because of that I don’t think any change to type variables specifically would actually prevent all bugs like this. What you’d need is a system that tracks which objects can change to which types at which points in the code. It seems like that would be a huge undertaking and render a lot of structural types effectively unusable.

3

It’s an issue with how variance is currently calculated and treated. There are related other issues and issues of a similar form as was noted in the original post, as well as some examples you presented, but these are broken independently of each other despite appearing to be related, in the following specific ways:

  1. narrowing dict → a specific typed dict should also not be allowed, but for different reasons here. The safe use here would require the original construction of that dict to be as an instance of that typed dict.

  2. runtime checkable protocols are inherently unsafe as well (as are use of __subclasscheck__ / __instancecheck__, and abc.ABC.register, all of these circumvent the type system’s knowledge and what is checked by it, instead defering to runtime where anything is possible this is different from TypeIs which is specified to only allow safe narrowing when used in a specific manner, though there are issues with what is and is not restricted here at the moment)

This is actually why variance matters in the first place and why variance not being checked at assignability is a problem. You can’t have a mutable container type that is covariant, and the covariance is why narrowing from Sequence → Sequence[specific] is considered okay.

It also is a place where the type system is wrong. I use that word intentionally here, as TypeIs is specified such that it says this is safe, and it is not due to an issue with it interacting with this problem.

This is unnecessary, the problem is contained to places where variance is incorrectly handled, tracking variance alone is enough in the worst case.

4

The code sample referenced above (the is_seq_b function) strikes me as a buggy implementation of a type guard function.

It’s trivial to create examples of type guard functions that misuse TypeIs (or TypeGuard). These will produce no type errors and mask actual bugs in your code. Here’s another example.

Code sample in pyright playground

from typing import TypeIs

def is_int(x: int | str) -> TypeIs[int]:
    # Buggy type guard function
    return True

def func(x: int | str):
    if is_int(x):
        print(x + 1)

func("") # Crash

I don’t think this is a problem with TypeIs, with the handling of variance, or with the type system in general. Not all bugs in your code will be caught by a static type checker. The static type system is a tool that can be used to improve the robustness of your code. You get to decide how to use (or misuse) features of the type system, and your results will vary accordingly.

TypeIs is a relatively advanced typing feature that most Python developers will never be aware of or use directly in their code. For more sophisticated developers who want to make direct use of this feature of the type system, there will always be the potential for misuse.

Perhaps what you’re raising here is the need for improved education. A typing system guide that provides some guidelines for proper use of TypeIs would be welcome if anyone would like to contribute.

3 Likes
5

The code sample reference above is in line with the accepted specification of safe narrowing using TypeIs.

The section of the PEP in which it was accepted labeled “Writing a safe TypeIs function” specifically says

For a function returning TypeIs[T] to be safe, it must return True if and only if the argument is compatible with type T , and False otherwise. If this condition is not met, the type checker may infer incorrect types.

There has been nothing amending this.

If not for the issue with variance here, this would be correct. (Though there are other issues with TypeIs that I’d be happy to discuss in the linked thread about TypeIs)

I understand that right now the issue with variance is so small that most people are writing it off as an issue with things it interacts with, but this is not the case, it’s a separate issue that right now, in the current type system, only presents itself in places where there are other issues.

6

I know you didn’t want to get into arguing that full list right now, but it might be helpful to do so, especially since I know that list contains examples of every single issue and you had a particularly compelling example showing this involving higher order function types with rust linked to show how it is something a type system can check, and the consequences in other type systems. This seems like something that should be fixed to clear the road for other things people want of landmines.

I don’t think this is a constructive comment to the discussion at hand. People want bugs that are an issue of types and interfaces to be caught by type checkers, and this is one of those. If you don’t think type checkers should catch type errors where they have the information to do so, I’m not sure what a type checker’s purpose would even be.

7

By your argument, basically every form of type narrowing is unsafe. For example, this program type checks fine, but crashes at runtime:

import asyncio


async def f(x: str | None = None):

    async def inner():
        await asyncio.sleep(1)
        nonlocal x
        x = None

    asyncio.create_task(inner())

    if x is not None:
        await asyncio.sleep(2)
        print(len(x))

asyncio.run(f("hello"))

You could construct a similar example using threading and even remove the awaits.

To me, this means that the type system cannot detect all possible runtime crashes, and that’s OK. Typing is a tool that can help make writing Python code safer, but it can’t fully eliminate the risk of crashes in a highly dynamic language.

If there are ways to help prevent such crashes without removing a lot of useful type checking behavior, I would support implementing them. But I don’t know what that could look like, and I’m fine with leaving this particular hole unplugged; I don’t think it’s a major problem in practice.

3 Likes
8

Thank you for not just dropping that list here, and no I don’t think it’s appropriate to do so, that list is not in a suitable state to be presented constructively to those working on the type system. As to the comment about rust, rust’s type system isn’t pythons. It may make a great example of how getting variance wrong can allow much worse issues, but I wasn’t prepared to fully elaborate on the consequences for HKTs or higher order function composition, and was trying to address it without doing so as there’s no guarantee anyone will ever work on HKTs in python.

9

This is a different problem than the one presented involving variance, and requires doing something abnormal, use of nonlocal to modify something.

It’s actually rather tiring to see “This other thing is also unsafe, so your specific issue isn’t an issue”, when the specific issue is actually solvable within the type system, even if the broader other thing isn’t.

10

Your original example involves two concurrent coroutines mutating the same list, which is also somewhat abnormal.

I’m not sure why this is different. It’s all instances of the same pattern: you use type narrowing to establish that an object is currently of one type, then something changes so that the condition no longer holds. I think for virtually any form of type narrowing that type checkers support, you can construct a similar example.

Even your Sequence example could be made unsafe without any reliance on assignability between list[] and Sequence[]. Imagine you have a Sequence class that when it is iterated over, queries a database and returns a list of objects, either A or B objects depending on what’s in the database. You pass it to is_seq_b() and check that it contains only B objects, but someone inserts an A object into the database before you do sum(i.use_count for i in x).

1 Like
11

Only one of them mutates the list, which is perfectly fine in async land. Passing to a function that only accepts a Sequence, not a MutableSequence, means that the caller knows the function (which might be in some library) will not be mutating it. Sorry that a minimal example of the problem doesn’t reflect why this could occur in “normal” code.

Because of this part right here “then something changes so that the condition no longer holds” isn’t possible in one of the cases if variance is fixed, but is in the other. you can’t have a mutable sequence that you’re allowed to narrow like this because you can’t have a mutablesequence that isn’t invariant (TypeIs in the positive case is input type & typeis conditional type, which is empty with invariant containers)

replacing the object entirely like you did is a different issue, but while we’re here:

    x: list[int | str]
    if isinstance(x[1], int):
        y = x[1] ** 2
    else:
        y = parse_text(x[1]) ** 2

Things like this are currently allowed, and would also be preventable by forcing you to narrow a specific object you hold, not a reference to a mutable list (other than with nonlocal…). Such a requirement should not even be seen as a downside, as it requires less work (not indexing into a list multiple times), and issues with “incorrect” narrowing are only going to become more of a problem with freethreading.

Writing such an object would be remarkably foolish for a number of reasons and goes into “you’re doing odd things that definitely can’t be accounted for anymore”, but it would be possible to fix this if we want to make stable iteration something markable in the type system

12

It does seem like most of these examples are instances of the same thing, a type narrowing condition check holding at one point in time and then changing before the usage of that value in a way that is only safe with that narrowed type. What is different is how that is achieved, my examples used typed dictionaries or protocols (whether we use @runtime_checkable or a TypeIs is completely irrelevant for this behaviour), Jelle’s use a nonlocal variable or a nondeterministic iterator, and Michaels uses generic protocols with differing variances. But all of them result in bugs because some variable is safely narrowed but then changes types.

Michael, it reads like you’re attempting to change things such that the type system would prevent narrowing types in ways where problems like this could occur. For your example using generic types with differing variances that might be feasible (though even that seems like a huge undertaking), but what would you do with the other cases? The only solution to my examples I can think of is to never allow narrowing to any typed dictionaries, protocols, or structural types in general. But with Jelle’s examples there doesn’t seem to be any good solution that still allows for type narrowing at all.

13

As I already said, these appear to be similar issues but are not Identical. These are each independently different ways in which something can go wrong with narrowing under the current behaviors of type checkers.

  1. I’d fix this variance issue
  2. For the dict/typed dict case, I’ve already brought up other changes I think are necessary to increase both usability and safety here: Structural subtyping, EAFP, and exceptions which inform structure, and I think TypeIs likely needs a note here (Note that TypedDict is the only structural type where this issue currently exists due to the ability to remove keys, if NotRequired is expanded to protocols, it would apply to them too)
  3. for the use of nonlocal to modify function locals out from under narrowing? I’m fine leaving that unsolved.

Not all of this is going to be solvable at the type system level for preventing issues, but some of it can be.

14

And here’s the concrete reason this is a variance issue.

Premises:

  • Variance is a property of a type.
  • TypeIs was deemed necessary to allow user defined functions which could narrow generic types safely
  • If TypeIs can’t narrow generics, it shouldn’t exist, as isinstance should be enough.
  • TypeIs relies on the variance of the input type for narrowing to work, as it is defined to take the set theoretic intersection between the input type and the TypeIs checked type in the positive case.

Therefore, variance is part of an API contract, and the erasure of variance (longstanding issue predating TypeIs) makes it impossible to write a safe TypeIs function that can narrow generic types.

Wtih an example, the definitions of G, A, and B do not matter however:

G should be a generic type, that takes a single covariant type variable
A should be a type
B should be a type that is a subtype of A


Tco = TypeVar("Tco", covariant=True, bound=A)

def narrower(i: G, t: Tco) -> TypeIs[G[Tco]]:
    ...

def public_api(x: G[Tco]):
    if narrower(x, B):
        # x is G[A] & G[B], if variance can be erased,
        # this is unsafe, as for invariant types,
        # this should be an empty intersection
        # the erasure of variance allows a subtype of G which is invariant
        # for which narrowing would be unsafe.
        ....

With the erasure of variance, it’s possible to have a subtype of G which is invariant and violates the public APIs stated expectations here. (This is the current state of affairs)

The specific issues that arise from this are limited currently, but this will become a larger issue as people continue wanting things that operate on higher order types

15

I do think this is a real issue that should be addressed in some way, because combining reasonable as-documented use of features of the Python type system can result in wrong type inference, and that’s not a good experience for users of Python typing.

I don’t think it is correct to say that the root problem is “erasure of variance”. I don’t think “erasure of variance” is a term that accurately describes anything that currently happens in the Python type system.

I don’t think the suggested “fix” of making e.g. list[int] not assignable to Sequence[int] is correct, realistically possible, or desirable. It would be a cure far worse than the disease.

Variance is not an arbitrary property of a generic type. It is determined by the use of the type variable in methods of the type. If the type variable appears in return position of methods, this allows it to be covariant, without breaking substitutability of subtypes. If it appears in argument position of methods, then it can be contravariant without breaking substitutability of subtypes. If it appears in both positions, then it must be invariant.

Because subtypes can add new methods, but not remove super-type methods, this naturally means that it is possible and correct for an invariant generic type to be a subtype of a covariant generic type: if the supertype only uses the typevar in return position, but the subtype uses it in both argument and return position. This is precisely the situation for list[int] and Sequence[int].

This is not “erasure of variance” – it is correct subtyping in the presence of variance. Variance is not erased; e.g. it is not possible for a covariant generic to be a subtype of an invariant or contravariant generic. It is only possible for an invariant generic to be a subtype of a contravariant or covariant generic.

The problem described here really is parallel to many of the other mentioned cases in this thread: type narrowing, even fully correct type narrowing, is not necessarily safe in the face of mutability from outside the local scope. Rust avoids this problem entirely with its strict mutable aliasing rules. Python has no such luxury.

Disallowing any type from being a subtype of a type with different variance would be incorrect, and would also be massively disruptive to the typing ecosystem. Passing a list[int] where a Sequence[int] or Sequence[int | None] or similar is needed, is extremely common in real-world code bases, and absolutely necessary to make the type system usable at all. The only way it would be feasible to consider changing this would be if Python had built-in runtime-immutable versions of all built-in container types, with zero-copy conversion from the mutable container to the equivalent immutable container, so that you could build a container (mutably) and then still convert it and pass it to a destination that requires the immutable version (and possibly covariance in the contained type as well). (I’d personally love to see this happen someday, but it’s a much bigger lift than changing some type system rules.)

Short of that, I don’t see any feasible fix for this problem in the type system. Instead, I think that the typing spec (and docs for features like TypeIs) should be much clearer about the limitations of type narrowing in general, and the mutation invariants that must be maintained for it to be fully safe.

5 Likes
16

I wrote a guide to type narrowing for inclusion in typing.readthedocs.io: Add guide to type narrowing by JelleZijlstra · Pull Request #1798 · python/typing · GitHub. This was on my todo list for a while as a followup to PEP 742, but this discussion prompted me to also add a section covering soundness problems with type narrowing.

2 Likes
17

This is definitely something that happens right now.

def erases_variance(x: list[T]) -> Sequence[T]:
    return x

This erases a constraint on valid subtyping relations for x

We don’t generally think of it in terms of a generic type but in terms of the type variable, however, we need to think of it in terms of both to correctly handle higher order function types that compose functions. If we’re fine ruling out HKTs from ever being possible to express in python, I’ll drop this and just leave things as they currently are, marking TypeIs as unsafe to use, but I was under the impression that HKTs were still considered by most to be a desired feature that had not been ruled out.

The fix isn’t to disallow subtyping with different variances but to disallow assignability with different variances. Unfortunately, most people currently view subtyping as the only restriction to assignability, but there’s a level of issue there.

type AnySequence[T] = Sequence[T] | MutableSequence[T]
type AnyMapping[T] = Mapping[T] | MutableMapping[T]

(etc) It would require more verbosity somewhere, hopefully common cases covered in typing, rather than requiring users to do all of this.

It would also likely mean that for protocols, the variance should be viewed as calculated or invariant, rather than just calculated, except when provided, in which case it should be possible to express a stricter variance than what would be calculated.

This is a solvable problem. If it isn’t because people don’t have the appetite for the required changes, we shouldn’t have runtime narrowing tools that claim to be safe in specific cases but which can’t be in this context; those we have such as TypeIs be removed or amended to just say it isn’t ever safe and that you are subverting the type checker.

18

I don’t think this would be a reason to drop this.

From discussions elsewhere, here’s a probably non-exhaustive list of things which are unsafe for just narrowing.

  1. isinstance or issubclass, involving types that define __instancecheck__, __subclasscheck__, inherent from abc.ABC (including abc.collections.*), and runtime checkable protocols, or involving types that use a # type ignore in their definition at all, or in types that are only expressed in stubs and the expression hides an incompatability. These apply to instances of types with the first argument, and types as the second argument.

  2. TypeGuard, ever. this should be deprecated and removed, it’s worse than cast because it can’t be made safe, so it incorrectly presents to users as safer than cast when it is not. conditional cast use is more clear to users about what safety does or does not exist.

  3. TypeIs, when the input type at runtime does not exactly match the annotation or when the existing guidance for a safe TypeIs function is not followed.

The problem with this is that users reasonably expect things that run at runtime and supposedly check these things to be safe to narrow with. This is a reasonable expectation, especially since runtime should have more accurate information available, not less; However, even following the guidance that exists, it’s not safe in at least these cases.

If handling variance differently removes the third one from needing to be on this list and TypeIs becomes safe to use as documented, that’s worth doing with or without future HKTs.

19

I guess you can choose to say that, but I don’t think it’s a useful description of what’s happening in that code. This function is simply an upcast, because list[T] is a subtype of Sequence[T]. It’s equivalent to this code:

class Base: pass
class Child(Base): pass
class OtherChild(Base): pass

def upcast(x: Child) -> Base:
    return x

You could just as well choose to say this upcast function also “erases a constraint on valid subtyping relations for x”, because OtherChild is a subtype of Base, but not a subtype of Child, in the same way that Sequence[SubtypeOfT] is a subtype of Sequence[T] but not a subtype of list[T]. That’s just how subtyping and the type lattice work.

If this is a motivation for a change to variance, it would be useful to provide some examples to clarify this problem and how a change to variance would help.

You can count me among “most people”. I don’t think this point of view is unfortunate, though :slight_smile: I’d be opposed to a change to the typing spec that makes a subtype not be assignable to a supertype. Substitutability (and thus assignability) is IMO central to the meaning of subtyping.

It would require more verbosity, and it still wouldn’t solve the usability problem, because usability requires being able to write a function that operates on e.g. Sequence[Base] and being able to still pass it a list[SubtypeOfBase], which is precisely what you are aiming to prevent with this change.

I haven’t seen any suggestion for a type-system-level “fix” to variance that I think would be an overall improvement to the type system, even if we were to entirely disregard the transition pain and compare only the end states.

I think variance is the wrong focus here. The unsafety with narrowing Sequence[T] is equivalent to the unsafety with narrowing the type of a mutable attribute of an object which other code may have references to; this latter problem doesn’t involve variance at all. This attribute narrowing is clearly known to be unsafe in the face of shared mutability, but both mypy and pyright still choose to do this narrowing, because in practice the pain of not doing it is worse than the unsafety of doing it. Even Pyre, which actually tried disallowing this unsafe attribute narrowing (I should know, I was there), was forced to back off in the face of real-world experience and allow it again (though it remains more conservative than mypy or pyright, forgetting the narrowing after a function call.)

The real problem in these cases is shared mutability. IMO the best immediately available option is to document that shared mutability makes some kinds of narrowing unsafe, but we still choose to support the narrowing because it is useful in many cases that don’t involve shared mutability, and the type system isn’t capable of knowing whether shared mutability is occurring or not.

If we want a fully-sound fix, IMO the direction to explore (whether in the language or the type system) would be actual runtime immutability and/or ownership rules, not changes to variance which only help with a subset of the problem, and at high cost in consistency and usability of the type system.

I don’t think that a correctly-written TypeIs guard is subverting the type-checker. It is performing narrowing which is locally safe but may not be safe if other references to the same object are concurrently mutating it. This is exactly the same level of safety provided by other existing forms of type narrowing that type checkers still choose to do anyway.

7 Likes
20

The unions there would accept either with the required changes to variance to enable this, it becomes an explicit indication that a function isn’t relying on things that are only safe with a specific variance.

Within the current definitions, yes. It’s probably worth pointing out that all of the academic work that would refer to a “type lattice” involves type inference and consistency checking of compiled programs where the compiler has a full view of the entire code graph and can fully assemble all constraints on a type to ensure there is validity, this is something not present in python. Absent that perspective, there’s still more that we can do than type checkers do today.

It’s impossible to write a correct TypeIs function under the current rules that would actually require TypeIs, rather than isinstance. Any invariant generic type could be narrowed invalidly with a combination of “correct” TypeIs functions. Any non-generic type doesn’t need TypeIs.

I don’t think the type system should allow the narrowing of mutable data structures at all Get a non-mutable element from it and narrow those on demand. Yes, this can still be subverted with nonlocal but that’s extremely limited by comparison. The variance fix happens to address precisely this issue, just in a different way than some people might expect.

Last time I brought up things in this direction more specifically, I was told off for getting too academic with it. I don’t feel like it’s worth hashing all of the issues that python has to deal with that other languages don’t need to again, just to have the same result when most people aren’t even willing to acknowledge that variance is part of the details about what is valid to do with a type and therefore should matter when considering assignability, even in the face of an example that shows unsafe narrowing that would be prevented by considering it and an example of where the variance is being relied upon, and that reliance subverted.

considering how many times people have brought up more immutable data structures or full arbitrary immutability and been shot down, I would bet on the entire python ecosystem, even the things that don’t make sense in rust, being rewritten in rust before this is ever a viable solution. This sounds good on paper to anyone that doesn’t know the history and futility of actually going that route and comes off like you’re trying to just shoo the problem away to somewhere it won’t get fixed.