pyright icon indicating copy to clipboard operation
pyright copied to clipboard

Unsoundness with protocols for polymorphic functions

Open jonathan-laurent opened this issue 6 months ago • 2 comments

Problem

In the example below, the second call to apply_twice causes a runtime error but it is accepted by pyright 1.1.375. In contrast, it is rejected by pyright 1.1.360 and by mypy 1.11.1 (using the alternative version below that does not use PEP 695 features).

from typing import Protocol

class PolyIdentity(Protocol):
    def __call__[T](self, arg: T, /) -> T: ...

def apply_twice(f: PolyIdentity, /) -> tuple[int, str]:
    return f(1), f("a")

def id[T](x: T) -> T:
    return x

def incr(x: int) -> int:
    return x + 1

apply_twice(id)
apply_twice(incr)  # no error with pyright 1.1.375 (but error with 1.1.360)
Version without PEP 695 features
from typing import Protocol, TypeVar

T = TypeVar("T")

class PolyIdentity(Protocol):
    def __call__(self, arg: T, /) -> T: ...

def apply_twice(f: PolyIdentity, /) -> tuple[int, str]:
    return f(1), f("a")

def id(x: T) -> T:
    return x

def incr(x: int) -> int:
    return x + 1

apply_twice(id)
apply_twice(incr) # mypy error

Comments

I am aware that this part of the typing spec is currently ambiguous and undergoing some work, so maybe this issue should be seen as asking a question rather than reporting a bug.

In my opinion, the most natural semantics for the PolyIdentity protocol above (by far) is to describe a polymorphic function of one argument. Thus, id is an acceptable implementation but incr is not since it can only accept integers. Having such a semantics would bring some form of rank-2 polymorphism to the language.

So my questions would be:

  • In the future, how is the PolyIdentity protocol most likely to be interpreted? Will it be forbidden? Will it represent a one-argument polymorphic function? Will it be given another semantics?
  • Under this interpretation, should the current pyright behaviour be considered a bug?

jonathan-laurent avatar Aug 07 '24 12:08 jonathan-laurent