I would emphasize two of those points as being more significant than they sound from that list.

First, function type signatures aren’t merely a useful thing to read, they’re computer verified documentation. For example:

• If a function in JS takes a string as an argument, its docs need to state that that argument is a string. If the same function is written in Java, the docs don’t need to say that because the type signature already does.
• If a function in C++ takes two pointers and returns a pointer, the docs need to say how long the returned pointer lives for: does it live for the lifetime of the first argument, or the second argument, or some other duration? If the same function is written in Rust, the docs don’t need to say that because the type signature already does.

And you can’t forget to update these docs because the compiler checks them for you.

Second, the sorts of errors that type systems eliminate aren’t just null pointers and trivial errors like typos. The sorts of bugs that a type system prevents can catch can be arbitrarily complex. It only seems like it’s preventing local bugs because the type system makes them local. Without type signatures, they aren’t local.

I would also consider type checking of “ownership patterns” whether through monads, substructural types, lifetime analysis, or whatever else to also be a very important property of type systems, just one most currently type systems don’t give you much help with. Bugs in this area (especially in the case of concurrency) are demonstrably common and difficult to diagnose and repair.

On the other hand, I also think there are diminishing returns to trying to encode increasingly complex correctness contracts into the type system. Quickly it seems to me the difficulty of understanding how the contract has been encoded and how to use it properly outweighs the difficulty of avoiding the error yourself. The cost can be worth it in safety critical systems, I assume.

Based on the most common use of generics in the most commonly used language with generics (Java) I would say this is empirically incorrect. The top two motivations are clearly: tooling assistance, and preventing putting values of the wrong type inside generic collections.

Counterargument: Typescript, Mypy, Sorbet, even Gleam all provide type systems that don’t and cannot make the code faster. I think there’s also an important case between “detect nulls” and “units of measure” which is features like ADTs that allow for the whole “make invalid states impossible” thing to happen.

More fundamentally, I think this is a roughly accurate list of how much different features of a type system are used, but I think it’s not necessarily right to call that importance. For example, Typescript is definitely designed to support LSP features in Javascript even when the type system isn’t fully there, and it often gets sold on the typo handling stuff — these are key features to Typescript’s success. But Mypy can do this stuff as well, yet my impression is Mypy hasn’t found half as much success in Python codebases as Typescript has in Javascript codebases.

I suspect this is because Typescript does a much better job of modelling the implicit types that already existed in Javascript codebases than Mypy does for Python. (This is partly because Typescript is more powerful, but I suspect also because Javascript is less dynamic, and so easier to model.) This, then, is the more important feature of a type system: it can model the problems that developers are using it for. If it can’t do that, then it is not fit for purpose and will be adjusted or replaced. But if it is sufficient for that purpose, then people will use it in roughly the order your describe in your list.

That said, I do think “the problems that developers are using it for” is such a broad statement that it will look differently for different languages. For example, you probably don’t want to model complex concepts in C, so C’s type system can remain relatively simple. Whereas modelling functions of complex states in a way that prevents errors feels like a definitional statement for functional programming, so MLs and friends will typically have much more complex type systems.

How this applies to Go, though, I’m not sure. Go’s designers definitely want their types and modelled concepts to be as simple as possible, but the way they keep on adding more complex features to the language suspects that they’ve not found quite the right local maxima yet.

My experience is with Typescript vs Javascript, but I’ve converted two or three codebases over to Typescript at this point, and each time the act of defining types for functions where the types weren’t entirely clear has helped me find bugs. It’s also allowed me to remove overly-defensive code and make the code easier to read overall.

I think part of this is that Typescript has a more powerful type system that better models real-world Javascript code (whereas Mypy’s always feels like Java with some light sugar on top). But I also suspect that Javascript is a lot easier to model than Python, as there are fewer opportunities for wild, dynamic code, and even when there are, most Javascript developers tend to avoid that style unless it’s really useful.

For your example specifically, Array#every, which is roughly the equivalent of all(...), does include the requisite type information to correctly handle this case:

declare const items: Array<string | null>;

// `.every(...)` always requires a predicate to be passed in, unlike `all(...)`, which
// means this is probably exactly how you'd write this in Javascript without types
if (items.every(items => items !== null)) {
  for (const item of items) {
    console.log(item.startsWith("http://"));
  }
}

I have never had mypy catch an actual type error when doing this (meaning, a situation where an attempt was made to use a value of a type incompatible with the expected one described in the annotation). I have, however, gone down far more rabbit holes than I’d care to in an attempt to figure out how to express things in a way mypy will understand.

My experience is quite the opposite, mypy did catch lots of typing errors that would otherwise just cause issues in runtime (or maybe not, but it was definitely doing something not the way I wanted to express). One example from yesterday, I was using subprocess.run (actually a wrapper above it, more details below) and wanted to pass an env parameter (that is a Mapping), and I did something like:

subprocess.run(["foo"], env={"ENV", "foo"}

Do you see the error? Probably yes, since this is only one line of the code that I was working for, but I didn’t, and mypy gladly got the issue. And even better, this was before I tested the code, and once I run for the first time (after fixing all mypy errors), the code Just Worked (TM).

The other day I was refactoring the code of the same project and I was not running mypy in the tests yet. I decided to setup mypy in the tests just to be sure and boom, I forgot to change the caller in the tests. Since they’re mocked, they still passed, but the tests didn’t made any sense. While it was annoying to type the test methods itself (that I don’t think makes much sense), after that experience I decided that I definitely need mypy running in my tests too.

I concur that mypy is weird sometimes, and far from perfect. For example, I got some really strange issues when trying to write a wrapper for another method (again, subprocess.run) and typing its keyword arguments. Something like:

class RunArgs(TypedDict, total=False):
    ...
    env: dict[str, str] | None  # actually a Mapping[StrOrBytesPath] | None, but decided to simplify here

def run_wrapper(args: list[str], extra_env: dict[str, str] | None = None, **kwargs: Unpack[RunArgs]):
   env = kwargs.get("env")
   if extra_env:
       env = (env or os.environ) | extra_env
   subprocess.run(args, env=env)

And this caused some weird issues. Moving env to the method parameter instead worked and even simplified the code, but yes, far from ideal.

But even with the somewhat strange issue, I still thing that mypy was a huge plus in this project. The fact that I can refactor code and be confident that if the tests and mypy pass it is very likely that the code is still correct is worth the work that I have to do sometimes to “please” mypy.

I’ve definitely found errors when converting python programs to have type hints, but not as many afterwards; perhaps it’s just that having the type annotations makes it harder for me (and other people working on it) to write incorrect code? Either way, I fully agree that mypy/pyright work in ways that are just too annoying and I disable them in IDE and linting unless I’m required to have them.