[throwawayffffas]

The whole type checking experience in python has disappointed me deeply and is seriously affecting my work.

I see the appeal for type-checking and yeah it has caught many bugs. But the language is quickly running blindly to the worst of all worlds in regards to typing.

1. You have to exhaustively write types in many cases where they can be obviously inferred.

2. The type checking is just a lint step. i.e. we are still paying for the duck typed typing system.

3. We no longer get to use the duck typed typing system making a lot of generic code require obscure annotation incantations to pass the lint check while it's correct python code.

My ideal typing system would be around constraints introduced by the code and completely inferred unless the user wants to tighten the constraints. i.e

Instead of

  def foo(a: int, b: int) -> int:
    return a + b

You would write:

  def foo(a, b):
    return a + b

And upon checking if you tried to do foo(5, {})

It would tell you that there is no + operator for int and dictionary that is required by the foo function.

My ideal typing system would allow you to constraint the types as well like so

  def foo(a: int, b: int):
    return a + b

The return type is not required in this case because it can be inferred by the function definition. For other cases it could be defined as well to constraint that we don't want None for example.

[HelloNurse]

Declaring types only where one wants to introduce a constraint would be nice, but unfortunately calls with obvious wrong types like "foo(5, {})" are a minority; in most cases types in a call depend on types of the calling function's parameters, and the type checker can only deduce unknown type from unconstrained type.

Moreover, the extremely dynamic execution and lack of compilation in Python means that determining in a lint step whether "there is no + operator for int and dictionary" is essentially impossible: if you find some __add__ or __radd__, you need to trust its declaration that it accepts certain types or not and hope it's still there at runtime; if you don't find it, it might exist at runtime when operator + is actually used.

A compiled and sufficiently static language, on the other hand, can inspect source code and libraries and reason about potentially infinite sets of definitions and prove that functions exist or don't exist.

[throwawayffffas]

I have the sneaking suspicion that for the vast majority of code it could be done.

I don't think the operator overloading is such a big issue since you can do the same kind of tracing for the overloaded operator.

The main issues would be metaclasses and all sort of monkey patching etc. i.e. anything that could mutate a type at runtime because the linter can't know if the mutation has happened.

Unfortunately I do not have the time nor patience to introduce the sixth type checker.

[HelloNurse]

You need to distinguish the prevention of actual type errors during the execution of a Python program, which would require mutilating the Python language, and linting Python code to find proven or likely defects, which is merely fraught with complications (open world and closed world assumptions, expecting more or less adversarial behaviour from callers of a function, etc.) and necessarily dependent on adding optional type declarations.

[rzmmm]

Ocaml is probably closest to that. The ML language family has roots in generic code with global type inference.