Collecting examples of unsoundness

Typing
1

We all know the Python type system is not fully sound, but there isn’t any concrete collection that shows this. I have created a new repo:

collecting examples of unsoundness. The examples already there range from extremely simple (using # type: ignore) to rather complex (using unpacked TypedDicts).

I’d love to have more examples, so if you can think of anything that’s not covered yet, please send a PR! The rules are simple:

  • Write a function with the signature def func(x: int) -> str
  • Make it actually return the input int at runtime
  • Have mypy and pyright accept the code without errors

The simplest example is this:

def func(x: int) -> str:
    return x  # type: ignore

A more interesting one is:

class Base:
    def __init__(self, x: int) -> None:
        self.x = str(x)

class Child(Base):
    def __init__(self, x: str) -> None:
        self.x = x

def doit(t: type[Base], x: int) -> str:
    return t(x).x

def func(x: int) -> str:
    return doit(Child, x)

(This relies on the fact that type checkers allow unsafe overrides for __init__.)

This isn’t intended to make or to start any argument, merely to document better how the type system behaves in practice. If you have any examples to share that aren’t covered in the repo yet, please let me know!

21 Likes
3

Here’s one:

def func(x: int) -> str:
    z = x
    x = 1 + abs(x)
    x **= -x
    return str(x) if isinstance(x, int) else z
4

Nice, looks like that’s because this hits the overload at typeshed/stdlib/builtins.pyi at 2408c028f4f677e0db4eabef0c70e9f6ab33e365 · python/typeshed · GitHub which returns Any.

5

While I think this is an interesting and useful project, it’s going to be difficult to exhaustively show all of the unsoundness via example rather than by the rules themselves that are unsound, because the unsoundness often doesn’t arise without multiple levels of indirection.

I may take some time later to try and construct a few of the more involved issues and PR them.

Here’s a few I noticed are missing:

  • Allowing subclasses to have a more restrictive variance of a reused generic parameter
  • Missing modeling for descriptors
  • Mutable collections typed as Collections.abc.*
  • Removable Hashability
  • Incorrect modeling of datamodel methods which are cooperative between operands with NotImplemented returns
1 Like
6

Yes, that is the reason but it is an invisible Any. I think that the fact that something as basic as integer arithmetic implicitly involves Any is worth considering as a separate case from the general use of Any.

Maybe it does not count as a separate example of unsoundness in the type system itself but it arises because it would be too awkward to express the real runtime behaviour of int.__pow__ accurately in the type system without dependent types. (I would argue that the runtime behaviour is actually the problem although many would disagree.)

7

Yes, I think it’s an instructive example and I just added it to the repo. Probably almost every use of Any or # type: ignore in typeshed could be used to achieve unsound behavior; it doesn’t make sense to collect all of those but I think it’s useful to collect a few more.

8

I really like the idea of the project, I had a bit related idea in Typing vs Runtime Behaviour - there are some examples thay may be included to unsoundness.

9

How about this?

value: int

class IntGetter:
    def get(self) -> int:
        return value


class StrGetter:
    def get(self) -> str:
        return "hello"


class Meta(type):
    def __new__(cls, name, bases, attrs) -> type[StrGetter] | type[IntGetter]:
        return IntGetter


class C(StrGetter, metaclass=Meta):
    pass


def func(x: int) -> str:
    global value
    value = x
    return C().get()
10

Nice, could you send a PR to my repo?

11

Here’s one, exploiting the weirdness of float:

from typing import TypeIs

def is_float(x: object) -> TypeIs[float]:
    return isinstance(x, float)

def func(x: int) -> str:
    return hider(x)

def hider(x: float) -> str:
    if not is_float(x):
        return x
    return "OK"

print(func(1))

Edit: I created a PR for this.

2 Likes
12

Here’s one that’s bothered me for a while (I was actually composing a post for this forum to discuss it). I’ll open a PR.

from collections.abc import Set


def func(x: int) -> str:
    result: Set[str] = set()
    other: Set[object] = result
    other |= {x}
    return next(iter(result))
4 Likes
13

I think that might be the same as unsoundness/examples/stdlib/mutable_inplace.py at main · JelleZijlstra/unsoundness · GitHub

14

Indeed it is. I noticed while opening a pull request. I was positively surprised to see that it was already in there.

15

Am I mistaken or is the root cause that sets are not invariant, despite being mutable?

16

collections.abc.Set is covariant, but not necessarily mutable. The builtins.set and MutableSet types are invariant.

Here’s how they’re defined in the typeshed stubs for typing (where typing.AbstractSet equivs collections.abc.Set):

1 Like
17

Am I mistaken or is the root cause that sets are not invariant, despite being mutable?

I don’t think that’s it. Note how the example uses the covariant and immutable collections.abc.Set.

I believe the root cause is that type checkers allow in-place operations like |= for any type that implements __or__, because according to the Python docs “If a specific method is not defined, or if that method returns NotImplemented, the augmented assignment falls back to the normal methods.”

Technically this is correct, because any type that implements collections.abc.Set would in fact support |= at runtime. But while it’s correct that it supports the operator, doesn’t mean that it’s safe. Because it breaks the covariance that the type claims to offer.

5 Likes
18

But while I’d love to get more in depth, I don’t want to draw this thread away from its intended purpose.

2 Likes
19

This is more that type checkers don’t clearly differentiate between a descriptor in the class dictionary vs instance dictionary

from typing import Callable

class Desc:
    def __call__[T](self, arg: T) -> T:
        return arg

    def __get__(self, instance: object, owner: object) -> Callable[[object], str]:
        return str

class C:
    desc: Desc
    def __init__(self):
        self.desc = Desc()

def func(x: int) -> str:
    return C().desc(x)

Adding reveal_type(C().desc) mypy gives:

Revealed type is “def (builtins.object) → builtins.str”

pyright gives

Type of “C().desc” is “(object) → str”

Changing desc: Desc to desc: ClassVar[Desc] and pyright complains on the instance variable assignment, mypy doesn’t.