A more useful and less divisive future for typing?

[davidfstr (David Foster)]

@mikeshardmind

there’s no clear long-term direction for typing, nor a clear answer to the question “Who is this for?”

“Who is this for?"

IMHO:

• Typing annotations provide the most value to long-lived Python programs that are expected to become large and/or be maintained by many individuals.
• Type annotations prevent some of the most common classes of programmatic errors:
  • Misspelled/broken references to functions/methods and variables.
  • Failure to handle potential Nones.
  • Missing imports (especially of exceptions).
• Type annotations provide reliable machine-verified documentation that cannot get out of date.

Long-term direction for typing

IMHO:

• The type system should be extended over time to describe & characterize common patterns used in real-world Python code.
  • That is, I propose the same kind of direction that TypeScript appears to have in characterizing patterns seen in real-world JavaScript code, even if some of those patterns are messy.

@mikeshardmind

There’s no good way to learn how to handle typing in Python.

Yes. There is a longstanding issue to write typechecker-agnostic HOWTO documentation.

As far as I can tell, there hasn’t been enough energy for anyone to step up and do this yet. I know I myself have not yet found enough bandwidth to write the section on TypedDict that I promised to a while back. (I have not forgotten.)

@mikeshardmind

@Jelle

The biggest disconnect is probably around soundness. You clearly care deeply about making the type system sound, but for many type checkers full soundness has not historically been a goal.

For me personally, yes this would be the largest disconnect.

@mikeshardmind

Quite bluntly, I don’t think something should claim to be a type checker if its primary purpose is not to check for soundness

Indeed I expect disagreement here: I do not personally think that a lack of (perfect) soundness disqualifies a type checker as being useful, as I have argued before:

• Unsound type systems are still useful

Also, as Eric mentioned, the definition of “sound” is not exactly black & white.