Again, purely anecdotally, I've done similar things in both Typescript and Python, and I usually catch at least one silly type error in Typescript, but I rarely do in Python. That could be because the Python developers I was following were just so good, but I suspect it's more about the quality of the typecheckers. Typescript feels much better at finding errors in normal, idiomatic Javascript, whereas I feel that with Mypy, if I want the best results, I need to write code in a way that plays to its strengths.

I've been told that Pyright is better but I've not tried it out properly. But yeah, your experience largely matches with mine, for Python at least.

IMO type hints are mostyl about (significantly!) improving readability.

You very quickly get undecidable type checking with such a powerful typesystem. Then you need a way to handle that, usually the solution is to help the type checker along by providing a proof that your code inhabits the claimed type. Then you need a way to have the proof live together with the code, a proof language, and preferably a whole library of proofs people can build on.

If this sounds fun then you can go play with e.g idris or F*.

I'm not sure how a python annotation/type system could possibly do that? If numpy/pandas had different types for different cardinalities it would work today.

You just need those libraries to embrace it really, then you could theoretically have type constructors that provide well-typed NxM matrix types or whatever, allowing you to enforce that [[1,2],[3,4]] is an instance of matrix_t(2, 2).

I don't see how python could possibly make such inferences for arbitrary libraries.

I like typing that with strings like '(batch,r,a,s,channel,t)'. The tooling doesn't do anything special with it, but it makes the code understandable at a glance. Adopting libraries like einops and core routines like einsum in lieu of equivalent alternatives encourages the propagation of names (rather than rolling axes or whatever) anywhere it matters. Having a coding convention about the standard order of axes helps a bit as people get more familiar with that aspect of the codebase too, only deviating where necessary.

You want dependent types!

Create a class what enforces this and use the new class as a type?

The Annotated type is worth mentioning as well. Today in something like SQLModel you do (from the readme):

    class Hero(SQLModel, table=True):
        id: Optional[int] = Field(default=None, primary_key=True)

And that's fine. I wouldn't necessarily change anything here. Annotated gives you the option of approaching things in a different way, though.

    class Hero(SQLModel, table=True):
        id: PrimaryKey[Optional[int]] = None

I have some use cases where the alternative approach is useful, like quantification of class fields or function arguments.

> Dataclasses is notable because it's the only example (I'm aware of) of type hints effecting runtime behavior as part of the stdlib.

FWIW, `typing.NamedTuple` did this in Python 3.5, three years before dataclasses was introduced in 3.7.

    class Foo(typing.NamedTuple):
        a: int
        b: str

    f = Foo(a=1, b="hello")
    print(f.b)  # "hello"

    Foo = typing.NamedTuple('Foo', [('a', int), ('b', str)])

I managed to find type hints affecting runtime behavior in functools.register. https://docs.python.org/3/library/functools.html?highlight=f...

> To add overloaded implementations to the function, use the register() attribute of the generic function, which can be used as a decorator. For functions annotated with types, the decorator will infer the type of the first argument automatically:

That appears to be the only other case.

Dataclasses, like typing.NamedTuple, do not care about type hints:

    >>> @dataclasses.dataclass
    ... class D:
    ...   x: int
    ...
    >>> D('a')
    D(x='a')

    @dataclass
    class A:
        a: int = 0
        b = 1

    >>> A(a=1, b=2)
    TypeError: __init__() got an unexpected keyword argument 'b'

Protocols with @runtime_checkable fit your description!

> There are stubs for pandas, but they're not enough because pandas has a tendency to change return types based on the input, and that breaks quickly.

A mechanism like Haskell's type application seems like it could solve at least most, maybe all of those problems.

> The way everybody else seems to be going is strong typing at function interfaces, with automatic inference of as much else as can be done easily

Both mypy and pyright will do that. If your function return type is annotated, they will infer the type of the receiving variable. If you have two branches where a variable can receive two types, pyright will infer the union type. Similar for None.

Example:

    a = input()
    if a.isdigit():
        x = int(a)
    else:
        x = a
    reveal_type(a)
    reveal_type(x)

Pyright output, stripped of configuration noise:

    typetest.py:6:13 - information: Type of "a" is "str"
    typetest.py:6:13 - information: Type of "x" is "int | str"

Mypy doesn't allow this. It infers `a` as `int` and rejects the second assignment.

The only times I need to annotate local variables are (1) the function isn't typed, so it gets inferred as Any (2) I'm initialising an empty collection, so its type might get inferred as e.g. `list[Unknown]` (pyright; mypy can infer the element type).

Is there something inference-wise that you miss in Python compared to C++ or Go?

PS: The larger problem to me is the inconsistence between pyright and mypy, the leading type-checkers. Sometimes issues are raised between them and they work to achieve agreement, but I believe the two issues highlighted above (unions and collections) are design choices, unlikely to change.

With python you can have your cake and it eat it, though.

Mock up something fast, no type hints.

Now, take that POC and make it production ready, by using mypy and pydantic.

How does Ruby’s system look? Python’s type hints are fully optional and opt-in, typed and non-typed code works the same (even though type checkers may complain about the latter).

Additions to language always confront syntax expectations. Some people can see through syntax to semantic intent, alas I am not one and the utility of a syntactic form goes (to me at least) beyond expressiveness to comprehension: if your syntax confuses then how can anyone comprehend?

Haskell dies in syntax.