[Python-ideas] Typecheckers: there can be only one

[Nick Coghlan]

On 7 September 2016 at 19:41, Paul Moore <p.f.moore at gmail.com> wrote:
> Frankly, this is the only model that makes sense, precisely because of
> the issues you raise. And it's an existing model used by linters like
> pyflakes, so there's no reason to assume it will be any less
> acceptable for type checkers.

Exactly - in a dynamic language like Python, running a typechecker is
a form of testing, rather than a necessary part of getting the code to
work in the first place.

For interactive-use-only code like the Jupyter Notebook I use to
download background images for my laptop [1], neither testing nor
typechecking are needed - I don't care if it works for all possible
cases and for all possible users, I only care that it works when I'm
the one running it. Code written for learning purposes, personal
automation, ad hoc data analysis, etc, largely falls into this
category.

For most other applications, an automated regression test suite will
be a better tool than a typechecker for preventing errors you actually
care about preventing. ("print('!dlrow elloH')" will typecheck just
fine, but probably isn't what you meant to do)

Similarly, a structural linter like pylint is smart enough to pick up
basic things like attempts to read non-existent attributes.

Where a typechecker starts to become attractive though is when you
start to hit the limits of automated testing regimes that involve
actually running the software and you've gone beyond the kinds of
errors a structural linter can find:

- combinatorial explosions make it impossible to test all code path combinations
- some error paths are simply difficult to trigger without extensive
investment in API mocking
- your code coverage has reached the point of diminishing returns (you
need a lot more test code for each new line of coverage)
- you're integrating multiple projects together and tracing the cause
of runtime test failures can be difficult
- you're engaging in large scale automated refactoring and want to be
confident the result is at least somewhat sensible

Like automated tests and structural linters, typecheckers should be
adopted only when the pain of *not* having them exceeds (or is
expected to exceed) the inconvenience of using them (and the precise
location of that threshold will vary by individual and by context).

Cheers,
Nick.

[1] http://nbviewer.jupyter.org/urls/bitbucket.org/ncoghlan/misc/raw/default/notebooks/Digital%20Blasphemy.ipynb

-- 
Nick Coghlan   |   ncoghlan at gmail.com   |   Brisbane, Australia