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!

18 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.