Typecheckers: there can be only one

There's been discussion here and on python-dev regarding PEP 526 that assumes there will be multiple type checkers for Python. I really can't see this happening. If typing annotations become common or maybe considered best practice, the Zen of Python "there should be one-- and preferably only one --obvious way to do it" will take effect. Firstly, the interpreter will need to have type checking built in. Just about every intro book and tutorial for Python says how great it is that you don't have an edit-save-compile cycle, just fire up the Python interpreter and start typing. Having to run a separate type checker will be considered as ridiculous as a C compiler that didn't run the preprocessor itself. Secondly, PyPI will collapse if there isn't just one. How can we express dependencies between packages that use different type checkers? When type checkers themselves have versions? When a dev team uses one type checker for 1.x and then switches to another for 2.x? That's a special circle of hell. -- cheers, Hugh Fisher

On 7 September 2016 at 10:28, Hugh Fisher <hugo.fisher@gmail.com> wrote:
The intention (and current reality) is that type checkers are *static* checkers, not runtime checks, in the same way as linters like pyflakes. So yo run a checker over your code as a QA step as part of your testing cycle, it has no runtime effect. So your users and dependencies are unaffected by your choice of typechecker. 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. Hope this clarifies the situation. Paul

On 7 September 2016 at 19:41, Paul Moore <p.f.moore@gmail.com> wrote:
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/not... -- Nick Coghlan | ncoghlan@gmail.com | Brisbane, Australia

On Wed, Sep 7, 2016 at 9:56 PM, Nick Coghlan <ncoghlan@gmail.com> wrote:
The average programmer such as myself will expect that if I write code specifying the type of a variable or whatever it should *do something*. It's code, I wrote it, it should be interpreted. Assuming PEP 526 is implemented, suppose as a very new programmer I write foo: dict = 0 (If anyone thinks even new programmers wouldn't write that, you've never taught an introductory programming course.) It takes very little programming experience to know that is flat out wrong. I cannot think of any other programming language with type notation where this would not be immediately flagged as an error. But Python will silently accept it? That's the kind of one liner people put on presentation slides when they want to make fun of how bad programming languages like JavaScript are. A more subtle example that came up recently on one of the lists (which I cannot attribute it properly right now): c : complex = 1.0 My C compiler is smart enough to figure out it should add an imaginary zero to the RHS. As an average programmer, I'd expect that Python would be at least as smart and likewise convert 1.0 into a complex value. Or it could raise an error saying that the RHS is not a complex number. Given the code I've written, either makes sense. What I would not expect is for the interpreter to silently assign a scalar 1.0 to c and continue. That's just ... WTF? Type annotations are code, not tests. -- cheers, Hugh Fisher

On 8 September 2016 at 00:00, Paul Moore <p.f.moore@gmail.com> wrote:
Type annotations are code, not tests.
Not in Python they aren't.
Well, to a certain extent. One can try something like this in REPL: from typing import get_type_hints import __main__ s: str class C: x: int get_type_hints(C) get_type_hints(__main__) Although please remember that the PEP is still provisional and implementation details may change. -- Ivan

On 08.09.2016 00:00, Paul Moore wrote:
If you need to read the documentation in order to understand a product, something's wrong. Especially given the simplicity of the examples. Some smartphones are delivered without a manual because they are considered to be as intuitive as breathing or walking.
Type annotations are code, not tests. Not in Python they aren't.
Unfortunately, that's not true. :) Sven

On Thu, Sep 8, 2016 at 8:00 AM, Paul Moore <p.f.moore@gmail.com> wrote:
Type annotations are code, not tests.
Not in Python they aren't.
The interpreter certainly thinks they're code rather than comments or docstrings, even before PEP 526. I type this into my Python 3.4 interpreter:
def foo(x:itn): ... return x
and the interpreter raises a NameError because 'itn' is not defined. Annotations look like code, they're mixed in with names and operators and literals and keywords, and all the standard syntax and semantic checks are applied. -- cheers, Hugh Fisher

On 8 September 2016 at 19:46, Hugh Fisher <hugo.fisher@gmail.com> wrote:
This is why I quite like the phrase "type assertions", particularly for the variable annotation form - as with assert statements, annotations are tests that you can write inline with your code rather than necessarily putting them in a different file. That doesn't make them not tests - it just makes them inline self-tests instead of external ones. The fact that assertions are checked by default (but can be turned off), while annotations are ignored by default (but can be checked with the appropriate optional tooling) has more to do with the relative maturity of the typecheckers than it does anything else - at this point in history, you still need to be on the lookout for bugs in the typecheckers themselves, rather than assuming that because a typechecker complained, there must be something wrong with the code. Folks with the kinds of problems that typecheckers solve are likely to be prepared to put up with the inconvenience of also dealing with bugs in them. By contrast, folks that just want to run some Python code that they already know works well enough for their purposes will want Python to keep working the same way it always has. (Hence why all of the typechecker developers chiming into these discussions point out that they always err on the side of *not* complaining about *correct* code, even if that increases their chances of missing some situations where the code is actually wrong) Cheers, Nick. -- Nick Coghlan | ncoghlan@gmail.com | Brisbane, Australia

On 8 September 2016 at 10:46, Hugh Fisher <hugo.fisher@gmail.com> wrote:
Apologies - I was thinking you were referring to variable annotations (and even there I was forgetting that the proposal had been changed to allow runtime introspection). What I should have said is that annotations do precisely that - they *annotate* the code objects with information. They don't in themselves have semantic consequences (and that's something the various PEPs have been at pains to establish - code that doesn't explicitly introspect the annotations will run the same with or without them). Paul

On Thu, Sep 08, 2016 at 07:46:41PM +1000, Hugh Fisher wrote:
Right. Python has supported annotations since 3.0. Folks have been able to confuse themselves by "declaring" (annotating) the types of function parameters for almost a decade, and yet your fears of newbies being confused by the lack of type checks by default has not eventuated. But I'll grant you that you are partially right: I completely expect that some people will (through inexperience or ignorance) write x: dict = 1 and be surprised that Python doesn't flag it as an error. That's a matter for education. Beginners to Python are confused by many things, such as the (non)fact that "ints are passed by value and lists by reference". I daresay that some people will point to this as a Python "WAT?" moment, just as they already point to the fact that Python doesn't flag x = 1 + "foo" as an error until runtime as a WAT moment. Okay, fine. It is kinda funny that the Python compiler can't tell that numbers and strings can't be added together even when they are literals. Currently we can write: x = 1 assert isinstance(x, dict) and the interpreter will allow it. The only difference is that assertions are on by default and annotations are off by default. (To be clear: annotations will set the special __annotations__ variable, but by default the annotation is note checked for correctness.) Assertions can be used as checked comments in Python, and annotations can be seen as similar: they are *checked type comments* for third-party tools. And, just maybe, Python 5000 or thereabouts will mandate that every Python interpreter include a built-in type checker capable of at least flagging errors like `x: dict = 1`. But it will be off by default.
I agree -- annotations are code. -- Steve

On 8 September 2016 at 07:31, Hugh Fisher <hugo.fisher@gmail.com> wrote:
It wouldn't surprise me in the least if education focused environments like the Mu text editor and potentially even Jupyter Notebooks decide to start running a typechecker implicitly, as many IDEs already do that. That way, if students do add type annotations (even if they're missing from all of the example code presented), they'll be enforced automatically. That's a decision to be made by instructors and development environment developers based on their assessment of their target audience though, it isn't something that needs to be baked into the core runtime design. Cheers, Nick. -- Nick Coghlan | ncoghlan@gmail.com | Brisbane, Australia

On Sep 7, 2016 4:28 AM, "Hugh Fisher" <hugo.fisher@gmail.com> wrote:
It already did: - mypy - pytype - PyCharm has an integrated one - pylint will add support in the future
A lot of people would disagree.
Remember: you don't have to run it. You can prototype to your hearts content and then have it run as a commit hook. So you still have the nice, tight cycle that you mentioned.
Secondly, PyPI will collapse if there isn't just one.
Too late!
Add the type checker to the dev dependencies; as long as it's PEP 484-compatible, the user couldn't care less.
When type checkers themselves have versions?
CPython has versions.
When a dev team uses one type checker for 1.x and then switches to another for 2.x?
That's the dev team's problem.
-- Ryan [ERROR]: Your autotools build scripts are 200 lines longer than your program. Something’s wrong. http://kirbyfan64.github.io/

On Wed, Sep 07, 2016 at 07:28:30PM +1000, Hugh Fisher wrote:
As Ryan has already pointed out, that has already happened.
Like there is only one linter? PyFlakes, PyChecker, Jedi, PyLint... which is the One Obvious Way? But it doesn't really matter if the Python ecosystem eventually converges on one single linter or one single type checker. That's just a matter of market share. If there's one linter that is just so good that it completely dominates the community, well, that's fine. What matters the language allows the existence of multiple checkers competing on quality and features.
Firstly, the interpreter will need to have type checking built in.
"Need" is very strong. I dare say that *eventually* some Python interpreters will have *some* soft of type checking built-in. Possibly even CPython itself. But it will always be an optional, off-by-default, feature, because if it is mandatory, the language you are using won't be Python, it will be some more-or-less close subset of Python. (Like StrongTalk compared to SmallTalk, or TrueScript compared to Javascript.) Fundamentally, Python will always be a dynamically-typed language, not a statically-typed one. Guido has been clear about that ever since he first proposed the idea of optional static typing more than a decade ago. Nothing has changed. http://www.artima.com/weblogs/viewpost.jsp?thread=85551
Right. And that won't change.
I fear that you haven't grasped the fundamental difference between gradual static typing of a dynamically-typed language like Python, and non-gradual typing of statically-typed languages like C, Haskell, Java, etc. Your statement seems like a reasonable fear if you think of static typing as a mandatory pre-compilation step which prevents the code from compiling or running if it doesn't pass. But it makes no sense in the context of an optional code analysis step which warns of things which may lead to runtime exceptions. I think that a good analogy here is that type checkers in the Python ecosystem are equivalent to static analysis tools like Coverity and BLAST in the C ecosystem. In the C ecosystem, it doesn't make sense to ask how you can express dependencies between packages that have been checked by Coverity versus those that have been checked by BLAST. The very question is irrelevant, and there's no reason not to check your package by *both*. Or neither. Or something else instead. -- Steve

On 7 September 2016 at 10:28, Hugh Fisher <hugo.fisher@gmail.com> wrote:
The intention (and current reality) is that type checkers are *static* checkers, not runtime checks, in the same way as linters like pyflakes. So yo run a checker over your code as a QA step as part of your testing cycle, it has no runtime effect. So your users and dependencies are unaffected by your choice of typechecker. 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. Hope this clarifies the situation. Paul

On 7 September 2016 at 19:41, Paul Moore <p.f.moore@gmail.com> wrote:
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/not... -- Nick Coghlan | ncoghlan@gmail.com | Brisbane, Australia

On Wed, Sep 7, 2016 at 9:56 PM, Nick Coghlan <ncoghlan@gmail.com> wrote:
The average programmer such as myself will expect that if I write code specifying the type of a variable or whatever it should *do something*. It's code, I wrote it, it should be interpreted. Assuming PEP 526 is implemented, suppose as a very new programmer I write foo: dict = 0 (If anyone thinks even new programmers wouldn't write that, you've never taught an introductory programming course.) It takes very little programming experience to know that is flat out wrong. I cannot think of any other programming language with type notation where this would not be immediately flagged as an error. But Python will silently accept it? That's the kind of one liner people put on presentation slides when they want to make fun of how bad programming languages like JavaScript are. A more subtle example that came up recently on one of the lists (which I cannot attribute it properly right now): c : complex = 1.0 My C compiler is smart enough to figure out it should add an imaginary zero to the RHS. As an average programmer, I'd expect that Python would be at least as smart and likewise convert 1.0 into a complex value. Or it could raise an error saying that the RHS is not a complex number. Given the code I've written, either makes sense. What I would not expect is for the interpreter to silently assign a scalar 1.0 to c and continue. That's just ... WTF? Type annotations are code, not tests. -- cheers, Hugh Fisher

On 8 September 2016 at 00:00, Paul Moore <p.f.moore@gmail.com> wrote:
Type annotations are code, not tests.
Not in Python they aren't.
Well, to a certain extent. One can try something like this in REPL: from typing import get_type_hints import __main__ s: str class C: x: int get_type_hints(C) get_type_hints(__main__) Although please remember that the PEP is still provisional and implementation details may change. -- Ivan

On 08.09.2016 00:00, Paul Moore wrote:
If you need to read the documentation in order to understand a product, something's wrong. Especially given the simplicity of the examples. Some smartphones are delivered without a manual because they are considered to be as intuitive as breathing or walking.
Type annotations are code, not tests. Not in Python they aren't.
Unfortunately, that's not true. :) Sven

On Thu, Sep 8, 2016 at 8:00 AM, Paul Moore <p.f.moore@gmail.com> wrote:
Type annotations are code, not tests.
Not in Python they aren't.
The interpreter certainly thinks they're code rather than comments or docstrings, even before PEP 526. I type this into my Python 3.4 interpreter:
def foo(x:itn): ... return x
and the interpreter raises a NameError because 'itn' is not defined. Annotations look like code, they're mixed in with names and operators and literals and keywords, and all the standard syntax and semantic checks are applied. -- cheers, Hugh Fisher

On 8 September 2016 at 19:46, Hugh Fisher <hugo.fisher@gmail.com> wrote:
This is why I quite like the phrase "type assertions", particularly for the variable annotation form - as with assert statements, annotations are tests that you can write inline with your code rather than necessarily putting them in a different file. That doesn't make them not tests - it just makes them inline self-tests instead of external ones. The fact that assertions are checked by default (but can be turned off), while annotations are ignored by default (but can be checked with the appropriate optional tooling) has more to do with the relative maturity of the typecheckers than it does anything else - at this point in history, you still need to be on the lookout for bugs in the typecheckers themselves, rather than assuming that because a typechecker complained, there must be something wrong with the code. Folks with the kinds of problems that typecheckers solve are likely to be prepared to put up with the inconvenience of also dealing with bugs in them. By contrast, folks that just want to run some Python code that they already know works well enough for their purposes will want Python to keep working the same way it always has. (Hence why all of the typechecker developers chiming into these discussions point out that they always err on the side of *not* complaining about *correct* code, even if that increases their chances of missing some situations where the code is actually wrong) Cheers, Nick. -- Nick Coghlan | ncoghlan@gmail.com | Brisbane, Australia

On 8 September 2016 at 10:46, Hugh Fisher <hugo.fisher@gmail.com> wrote:
Apologies - I was thinking you were referring to variable annotations (and even there I was forgetting that the proposal had been changed to allow runtime introspection). What I should have said is that annotations do precisely that - they *annotate* the code objects with information. They don't in themselves have semantic consequences (and that's something the various PEPs have been at pains to establish - code that doesn't explicitly introspect the annotations will run the same with or without them). Paul

On Thu, Sep 08, 2016 at 07:46:41PM +1000, Hugh Fisher wrote:
Right. Python has supported annotations since 3.0. Folks have been able to confuse themselves by "declaring" (annotating) the types of function parameters for almost a decade, and yet your fears of newbies being confused by the lack of type checks by default has not eventuated. But I'll grant you that you are partially right: I completely expect that some people will (through inexperience or ignorance) write x: dict = 1 and be surprised that Python doesn't flag it as an error. That's a matter for education. Beginners to Python are confused by many things, such as the (non)fact that "ints are passed by value and lists by reference". I daresay that some people will point to this as a Python "WAT?" moment, just as they already point to the fact that Python doesn't flag x = 1 + "foo" as an error until runtime as a WAT moment. Okay, fine. It is kinda funny that the Python compiler can't tell that numbers and strings can't be added together even when they are literals. Currently we can write: x = 1 assert isinstance(x, dict) and the interpreter will allow it. The only difference is that assertions are on by default and annotations are off by default. (To be clear: annotations will set the special __annotations__ variable, but by default the annotation is note checked for correctness.) Assertions can be used as checked comments in Python, and annotations can be seen as similar: they are *checked type comments* for third-party tools. And, just maybe, Python 5000 or thereabouts will mandate that every Python interpreter include a built-in type checker capable of at least flagging errors like `x: dict = 1`. But it will be off by default.
I agree -- annotations are code. -- Steve

On 8 September 2016 at 07:31, Hugh Fisher <hugo.fisher@gmail.com> wrote:
It wouldn't surprise me in the least if education focused environments like the Mu text editor and potentially even Jupyter Notebooks decide to start running a typechecker implicitly, as many IDEs already do that. That way, if students do add type annotations (even if they're missing from all of the example code presented), they'll be enforced automatically. That's a decision to be made by instructors and development environment developers based on their assessment of their target audience though, it isn't something that needs to be baked into the core runtime design. Cheers, Nick. -- Nick Coghlan | ncoghlan@gmail.com | Brisbane, Australia

On Sep 7, 2016 4:28 AM, "Hugh Fisher" <hugo.fisher@gmail.com> wrote:
It already did: - mypy - pytype - PyCharm has an integrated one - pylint will add support in the future
A lot of people would disagree.
Remember: you don't have to run it. You can prototype to your hearts content and then have it run as a commit hook. So you still have the nice, tight cycle that you mentioned.
Secondly, PyPI will collapse if there isn't just one.
Too late!
Add the type checker to the dev dependencies; as long as it's PEP 484-compatible, the user couldn't care less.
When type checkers themselves have versions?
CPython has versions.
When a dev team uses one type checker for 1.x and then switches to another for 2.x?
That's the dev team's problem.
-- Ryan [ERROR]: Your autotools build scripts are 200 lines longer than your program. Something’s wrong. http://kirbyfan64.github.io/

On Wed, Sep 07, 2016 at 07:28:30PM +1000, Hugh Fisher wrote:
As Ryan has already pointed out, that has already happened.
Like there is only one linter? PyFlakes, PyChecker, Jedi, PyLint... which is the One Obvious Way? But it doesn't really matter if the Python ecosystem eventually converges on one single linter or one single type checker. That's just a matter of market share. If there's one linter that is just so good that it completely dominates the community, well, that's fine. What matters the language allows the existence of multiple checkers competing on quality and features.
Firstly, the interpreter will need to have type checking built in.
"Need" is very strong. I dare say that *eventually* some Python interpreters will have *some* soft of type checking built-in. Possibly even CPython itself. But it will always be an optional, off-by-default, feature, because if it is mandatory, the language you are using won't be Python, it will be some more-or-less close subset of Python. (Like StrongTalk compared to SmallTalk, or TrueScript compared to Javascript.) Fundamentally, Python will always be a dynamically-typed language, not a statically-typed one. Guido has been clear about that ever since he first proposed the idea of optional static typing more than a decade ago. Nothing has changed. http://www.artima.com/weblogs/viewpost.jsp?thread=85551
Right. And that won't change.
I fear that you haven't grasped the fundamental difference between gradual static typing of a dynamically-typed language like Python, and non-gradual typing of statically-typed languages like C, Haskell, Java, etc. Your statement seems like a reasonable fear if you think of static typing as a mandatory pre-compilation step which prevents the code from compiling or running if it doesn't pass. But it makes no sense in the context of an optional code analysis step which warns of things which may lead to runtime exceptions. I think that a good analogy here is that type checkers in the Python ecosystem are equivalent to static analysis tools like Coverity and BLAST in the C ecosystem. In the C ecosystem, it doesn't make sense to ask how you can express dependencies between packages that have been checked by Coverity versus those that have been checked by BLAST. The very question is irrelevant, and there's no reason not to check your package by *both*. Or neither. Or something else instead. -- Steve
participants (7)
-
Hugh Fisher
-
Ivan Levkivskyi
-
Nick Coghlan
-
Paul Moore
-
Ryan Gonzalez
-
Steven D'Aprano
-
Sven R. Kunze