Typechecking of overloaded function implementation

[ethframe]

I wonder if it is actually possible to check that an implementation of overloaded functions behaves according to its signatures. In other words, to reject the following code:

@overload
def foo(a: int) -> int: ...
@overload
def foo(a: str) -> str: ...

def foo(a: int | str) -> int | str:
    return 0

because it's obviously incorrect.

It looks like that a simple type check against each overload signature should do the job. The idea is that if an implementation behaves according to the overload signatures, then by providing arguments with types narrowed to the types of arguments in any overload, all return statements will be either unreachable or will have the inferred type that is compatible with that overload due to type narrowing.

Maybe I am missing something and it would not work as I imagine? Or maybe there are some other concerns, like increased runtime due to multiple passes over one function?

[erictraut]

I think it would be theoretically possible to do this, but it's technically very difficult and computationally expensive. It's also not clear how such errors could be reported in an understandable way. I'm not aware of any type checkers in any language that do this. It would effectively require that the full implementation be type-checked multiple times, once for each overload signature. Errors would need to be reported independently for each pass, and they'd be jumbled together.

Overloads are a pretty advanced feature of the type system. Very few Python developers know that the feature exists, so those who do use them tend to be sophisticated and advanced developers and are typically able to make the implementation match the overload signatures, so I don't consider this a big problem to begin with.

[adam-grant-hendry]

@erictaut While you may be correct, at some point a programmer does have to subclass a method that contains polymorphic functions, so I'm inclined to disagree: I think it's a more common occurrence than you might initially surmise.