https://github.com/JukkaL/mypy is the/one implementation of a static checker that conforms to PEP 484. (Naturally, as far as I know, JukkaL with mypy almost singlehandedly inspired the PEP.)
I encourage all use of the type system to ensure program correctness, but once you've had Hindley-Milner inference, it's hard to muddle along with something like this.
Something I find myself wanting to do occasionally, that you can do in C#, is instantiate a generic type with a default constructor. Like if I have a generic type T, I'd like to be able to do `new T()`.
I feel like that comment is a little disingenous or at least needs a caveat after reading this[0]. I know that casts are almost never needed in Haskell code whereas I needed them in my last Android application (correct me if there's another way).
That stackoverflow answer explains Haskell does type erasure. No, it doesn't work exactly the same as in Java, but nobody claimed it did. The OP claimed Java's type erasure annoyed him, while also claiming he had used Haskell a lot. I merely pointed out Haskell also erases types.
I cannot advise you on your Android application without knowing what you're trying to accomplish.
Though make the type system sufficiently more expressive than Haskell's and you have to give up on type inference again...
Though maybe you could restrict how expressive the type system is on something like a module (Haskell module) level, so that you can have type inference if you give up on some power? I don't know.
Type inference doesn't somehow fail if we go beyond Haskell's type system. The inferable subset of the language remains inferable. Haskell already has inferable (Hindley-Milner) and uninferable (higher-rank polymorphism, GADTs) parts. If we go beyond Haskell's type system, it actually becomes crucial for productivity to have powerful type (and term) inference. Agda and Coq both have much more powerful inference than Haskell; it's just that don't bother with using it to realize Hindley-Milner-style annotation-free bindings, because there's little use for it in proof assistants.
You can use both, actually. Type systems here days are more about type feedback (code completion, yeh!) than correctness (important, just not the central focus).
> So now two popular dynamic languages have type hinting of a kind: Python (unenforced annotations) and PHP (declarations). Great!
Don't forget Javascript, via Typescript (which predates both Python and PHP's typechecking): http://www.typescriptlang.org/
Typescript is a strict superset of Javascript that compiles very transparently to the equivalent Javascript, so I think it's close enough to what Python3 does to be included here.
The annotations are stripped out before runtime, but they are checked at compile-time for any errors that are possible to detect statically.
This allows me to write Python in a design-by-contract style with full, rich runtime type checks. My bug count has gone down dramatically, and when I do find a bug it's virtually always via a typecheck exception.
Yeah, isn't that amazing? I really think this "type" idea is a good one. I wonder if other languages have thought about following Python's lead and adding a type system.
No, but let me clarify. Bolting on a form of type checking to a weakly typed language seems orthogonal to the nature of a language like Python. If you find yourself saying "I wish I had a type system in this code base, its getting pretty big and a compiler that does type checking at compile time sure would make my life easier" maybe you should think about using a more appropriate tool.
I use Python a lot and it has its uses, but adding this type hint stuff just seems like an enabler for causing myself pain and denial when I should be using a more strongly typed language.
Python's type system is weak whether they self-identify that way or not. Types are implicitly converted in a variety of cases, notably True-ness. Meanwhile, runtime type identity is kind of meaningless; classes and individual objects can have their behavior meaningfully changed at runtime. The most you can say about any variable in Python is that it is a descendant of 'object' or else some primitive type.
One place where Python is pretty weakly typed is going the other way, where it accepts things like: true + true * 2 - false / true, even outside of if statements.
I've definitely been bitten by this before, accidentally passing in a book parameter instead of an int, and having some math work initially and then blow up months later.
Knuth argues against this kind of implicit bool to integer conversion in Concrete Mathematics.
There's a lot of history of languages without a real boolean type using integer 0 and 1 as the sentinel values indicating false-ness and true-ness.
And Python, in a nod to that, implements bool as a subclass of int, of which only two instances can ever exist (with False having a value of 0 and True having a value of 1).
So this isn't weak typing -- isinstance(True, int) is True in Python, and operations like the ones you're mentioning work because of that, for the same reason any other subclass of int would work.
Interesting, so technically isn't weak typing, but in practice to me it is a distinction without a difference. You could make int a subtype of string, and allow things like "1" + 1 == "11" and end up with many of the same problems of weakly typed languages.
Well, there's also ancient-history stuff going on here in that Python originally didn't have a boolean type, which mean using integer 0 and 1 was the standard practice. "True" and "False" as aliases for integer 1 and 0 were added in 2002, and the actual boolean type -- implemented as a subclass of int since that got automatic compatibility with existing code using integer values -- was added in 2003.
Well, that would violate the Liskov Substitution Principle.
But I think there's a fundamental divide about what weak typing actually is. For example, it's entirely possible in Rust to have implemented Add for i32 and String. Even this isn't weak typing in its traditional form.
AFAIK, in this sense weak typing refers to whenever the compiler will implicitly cast one type to another in order to satisfy a type constraint. C's number types do this. PHP does this on everything. Javascript has, eg., [] + [] == "". Python does not do this - all type casts are explicit in the implementation of the operator or function (which is implemented on the type, not globally).
It's reasonable to argue that the use of the phrase "weak typing" to mean "things I don't like about a type-system" is not only well established but maybe even more useful. It does, however, irritate Python programmers who don't want their language lumped in with PHP.
It is so because in the beginning python didn't have a boolean type. It used 0 and 1 integers instead. Later when bool was introduced it was a subclass of integers.
I think you should brush up a little on your python-bashing methodology. It might work on individuals that don't know enough about Python, but not for the rest of us.
Second, boolean evaluation of arbitrary types in Python is not "weak" -- it's well-defined through a standard language-level protocol, and it's always very clear what can and can't be evaluated as a boolean and what boolean values will result from doing so.
Static typing is considered unpythonic, but the typecheck library is closer to a sanity-checking model (like using assert). The advantage is that instead of the checks being in the body, they can be moved to the function header. It supports things such as checking ranges or regex matches, rather than just object types.
Even if people are only using it as a shim for what could be static typechecking, I think there's something to say about the practicality of it existing, if only for the reason that their ecosystem might already be Python-based.
I agree with everything you said here. Personally, I wish this had been your original post. It seems like a helpful jumping-off point for constructive conversation.
Yeah, imagine how retarded the type systems of the popular static typed languages were, that lead to such a baby-booming of dynamic languages. People were traumatized so hard that took years to reconsider a middle ground.
> Following Python's lead and adding a type system
Joking? Python really is almost the last of all dynamic languages to come up with syntax for that.
common lisp, scheme, perl, ruby, javascript, php have all syntax for optional typing already, only Guido was against it for years.
Which eventually led to Go being developed by Google, and python's downfall. They try to catchup now, but this proposal is only 10% of an optional type system. I miss the inferencer and the optimizations still.
Thanks for the link. I developed the annotation+decorator-based type checker in https://github.com/kislyuk/ensure before I saw typecheck-decorator (which looks like it has some cool features). One thing I'm proud of with ensure's @ensure_annotations decorator is that we actually went through a few rounds of optimization and are fairly confident in the decorator's runtime performance.
Optional type checking as a first-class citizen is a great tool to have, and it's good to see the syntax standardized.
But as alluded to in the Reddit thread, there are serious issues with this PEP. The use of comments and the lack of runtime type checking from the start not only limits the potential of this particular PEP, but undermines future efforts to bring that functionality in.
IMO it would have been better to put in the work and properly integrate type checking decorations into the interpreter and the grammar. The tack-on comments at the end of the line are especially un-Pythonic and jarring.
Edit: Just saw the string literal based forward references. Ugh. Another problem in the making.
This might sound odd, but lately I haven't noticed any bugs I've introduced to production that were type errors.
Inevitably my code will produce results of the right type, but have a logical error that makes either the answer flat out wrong or more or less inaccurate based on our cloud requirements.
I see your point in hobbyist vs. enterprise, but Python is already used in multiple big corporations and I don't think I have seen any result of it being a problem. If anything, the language gets more and more attention due to its spreading popularity on all levels. Isn't that just for the good of the language?
As I mentioned it is already used in several big corporations. From your point of view - is it a problem right now?
I remain on the fence myself, but that article mostly argues that it is useable and used in the enterprise, not that it's worthy of use at that project size and scale. I think that article, rather than being a strong technical piece, is a pretty good example of:
Nim the language[1] will probably still win with regards to mechanical sympathy. And perhaps also metaprogramming?
[1] As opposed to implementations... because I don't know what kind of crazy compiler (JIT or AOT) they do nowadays to make "slow" languages fast. So for all I know Python can still be fast, given enough manpower.
Interesting to me that they write "Python will remain a dynamically typed language, and the authors have no desire to ever make type hints mandatory, even by convention."
Having no experience with using gradual typing, I wonder if there's any stable equilibrium here between "thoroughly dynamic" and "type declarations everywhere".
In any case, as someone who started with Python and started preferring static types later on, I really hope this gets used.
Not quite. The PEP is (to me) quite explicit that the typing is never mandatory. So a comment-hint will never change the way the code actually runs, nor will lack of a comment or an unintentional comment cause a program to act strangely.
Already, anyone seriously using pylint or other "normal" python linting tools uses comments like that to give extra hints to the linter:
def blah(): # pylint: ignoresomething
type of thing. Yes, it's a bit weird, and yes, it does teeter right on the edge of the comments as syntactic value precipice, but I think lands just on the alright side.
I like it, let the developer choose where typing is most appropriate. Also runtime type assertions really help with identifying bugs, especially NoneType issues.
Nice. It really seems like static typing and functional programming are winning [1]. For the most part, I think that's very a good thing, and may help move the software industry forward.
I mostly like Python for its clean syntax but the examples contained in this PEP turn unreadable really fast. I don't look forward to this and I don't really see the point of it. I can see how it can be useful in theory but, in practice, I just see a symptom of language bloat.
The way I see it, if you find yourself in the situation where explicit type checking is important, there's probably something wrong with your process or team. Either your are not testing properly, or your team's mindset is more adjusted to another language.
The danger I see with this becoming widespread is Python becoming somewhat like C++ where it's very easy to come across code one can't easily read because it uses a different subset of features than you're used to. This sort of "language accents" so common in human languages is something that should be avoided in computer languages, IMHO.
One could argue that you'd need many fewer lines of test code if your compiler can prove a lot of stuff is correct at compile time. It's a personal preference thing but I prefer this situation and don't view it as having poor testing
It seems more like Scala syntax, which is much cleaner than C++ IMHO. But with Java becoming dynamic (and C++ techniques for same), is the future a smear of shared language features, like Bladerunner's cityspeak, or are these just intermediate forms as a new protolanguage capable of unifying these features comes into existence?
I suspect the latter. The static typing crowd is moving towards type inference - you mentioned the obvious examples already. Now we're seeing dynamic languages evolving towards static typing with inference.
I think that most people if they really think deeply about it would say that all things being equal that static typing is a good thing. The problem is that all things are not equal and that the cost of extra syntax, boilerplate, etc can completely outweigh the benefits of of that static typing (as the GP post clearly believes). I was a huge dynamic language fan until I started using Scala full time and since then I've gone completely the other direction to being a static fan. I suspect as more people start finding their way to tools which provide static typing guarantees without the syntax getting in their way so much that we'll find a nice middle ground.
From the acceptance letter:
"""
if you are worried that this will make Python ugly and turn it
into some sort of inferior Java, then I share you concerns, but I would
like to remind you of another potential ugliness; operator overloading.
C++, Perl and Haskell have operator overloading and it gets abused
something rotten to produce "concise" (a.k.a. line noise) code.
Python also has operator overloading and it is used sensibly, as it
should be. Why?
It's a cultural issue; readability matters.
Python is your language, please use type-hints responsibly :)
"""
I would add metaclasses, generators, etc. all these are already enough to write horrible things.
It is indeed all about "culture", readability is really the cornerstone of Python culture. Type hints when used responsibly are fantastic tool. You could be surprised but they really improve readability, it's like a succinct docstring. I discovered this while recently reading through one large codebase.
Moreover, typechecker will tell you when your "docs" do not reflect actual semantics.
Finally, I would like to point out that typing.py and Mypy are pure Python, no magic :-) At the same time "import typing" is very in the spirit of "import antigravity".
I hope Python gradual typing could become alternative to Java/C++/etc. BDSM-style typing and one day we could say: "Come join us! Typing is fun again" :-)
> C++, Perl and Haskell have operator overloading and it gets abused something rotten to produce "concise" (a.k.a. line noise) code.
That's fairly funny coming from a discussion about a language that overloads '+' for strings and numerics, and overloads ==/!= similarly. Perl uses '.' for string concatenation and '+' for numeric addition, and uses eq/ne for string equality, and ==/!= for numeric equality. There's a reason for that.
Overloading is not necessarily used that often in Perl. It's a module that's part of the core, but it's fairly clunky and I rarely see it in the wild except for that spots that it really makes sense (DateTime object boolean comparison comes to mind).
74 comments
[ 3.4 ms ] story [ 139 ms ] threadAnd if you don't want to create your own you could use https://pypi.python.org/pypi/obiwan
For new PEP 0484 features like generics, MyPy supports Python 3.2 and up, but PyCharm support seems to be work in progress: https://youtrack.jetbrains.com/issue/PY-15206
It's Java's that drives me absolutely insane. Type erasure makes me want to pull my hair out.
0: http://stackoverflow.com/questions/12468722/does-haskell-era...
I cannot advise you on your Android application without knowing what you're trying to accomplish.
Though maybe you could restrict how expressive the type system is on something like a module (Haskell module) level, so that you can have type inference if you give up on some power? I don't know.
Don't forget Javascript, via Typescript (which predates both Python and PHP's typechecking): http://www.typescriptlang.org/
Typescript is a strict superset of Javascript that compiles very transparently to the equivalent Javascript, so I think it's close enough to what Python3 does to be included here.
The annotations are stripped out before runtime, but they are checked at compile-time for any errors that are possible to detect statically.
This allows me to write Python in a design-by-contract style with full, rich runtime type checks. My bug count has gone down dramatically, and when I do find a bug it's virtually always via a typecheck exception.
I use Python a lot and it has its uses, but adding this type hint stuff just seems like an enabler for causing myself pain and denial when I should be using a more strongly typed language.
You likely meant "dynamic", not "weak". See here:
wiki.python.org/moin/Why%20is%20Python%20a%20dynamic%20language%20and%20also%20a%20strongly%20typed%20language
I've definitely been bitten by this before, accidentally passing in a book parameter instead of an int, and having some math work initially and then blow up months later.
Knuth argues against this kind of implicit bool to integer conversion in Concrete Mathematics.
There's a lot of history of languages without a real boolean type using integer 0 and 1 as the sentinel values indicating false-ness and true-ness.
And Python, in a nod to that, implements bool as a subclass of int, of which only two instances can ever exist (with False having a value of 0 and True having a value of 1).
So this isn't weak typing -- isinstance(True, int) is True in Python, and operations like the ones you're mentioning work because of that, for the same reason any other subclass of int would work.
But I think there's a fundamental divide about what weak typing actually is. For example, it's entirely possible in Rust to have implemented Add for i32 and String. Even this isn't weak typing in its traditional form.
AFAIK, in this sense weak typing refers to whenever the compiler will implicitly cast one type to another in order to satisfy a type constraint. C's number types do this. PHP does this on everything. Javascript has, eg., [] + [] == "". Python does not do this - all type casts are explicit in the implementation of the operator or function (which is implemented on the type, not globally).
It's reasonable to argue that the use of the phrase "weak typing" to mean "things I don't like about a type-system" is not only well established but maybe even more useful. It does, however, irritate Python programmers who don't want their language lumped in with PHP.
First off, see my other comment about Python's boolean type and the fact that it is an integral type:
https://news.ycombinator.com/item?id=9595988
Second, boolean evaluation of arbitrary types in Python is not "weak" -- it's well-defined through a standard language-level protocol, and it's always very clear what can and can't be evaluated as a boolean and what boolean values will result from doing so.
Even if people are only using it as a shim for what could be static typechecking, I think there's something to say about the practicality of it existing, if only for the reason that their ecosystem might already be Python-based.
Maybe you should reconsider yours?
If you look at how popular go is among pythonistas, it kind of shows that the issue was really a lack of type inference more than anything else.
A good summary what's wrong with the type systems of the java era: http://www.slideshare.net/ScottWlaschin/c-light
Joking? Python really is almost the last of all dynamic languages to come up with syntax for that. common lisp, scheme, perl, ruby, javascript, php have all syntax for optional typing already, only Guido was against it for years. Which eventually led to Go being developed by Google, and python's downfall. They try to catchup now, but this proposal is only 10% of an optional type system. I miss the inferencer and the optimizations still.
Optional type checking as a first-class citizen is a great tool to have, and it's good to see the syntax standardized.
But as alluded to in the Reddit thread, there are serious issues with this PEP. The use of comments and the lack of runtime type checking from the start not only limits the potential of this particular PEP, but undermines future efforts to bring that functionality in.
IMO it would have been better to put in the work and properly integrate type checking decorations into the interpreter and the grammar. The tack-on comments at the end of the line are especially un-Pythonic and jarring.
Edit: Just saw the string literal based forward references. Ugh. Another problem in the making.
Inevitably my code will produce results of the right type, but have a logical error that makes either the answer flat out wrong or more or less inaccurate based on our cloud requirements.
C was much more friendly. And faster too!
I wish they kept separate ways. Python for simple and powerful hobbyist programs and nim for the enterprise.
If we have two languages doing the same thing, we will abandon one group of enthusiasts. Then another language will come to fill the gap.
As I mentioned it is already used in several big corporations. From your point of view - is it a problem right now?
[1] - https://www.paypal-engineering.com/2014/12/10/10-myths-of-en...
http://en.wikipedia.org/wiki/Argumentum_ad_populum
Also, it doesn't take much google-fu to find a counterargument from someone apparently reputable:
http://www.quora.com/Why-does-Google-prefer-the-Java-stack-f...
[1] As opposed to implementations... because I don't know what kind of crazy compiler (JIT or AOT) they do nowadays to make "slow" languages fast. So for all I know Python can still be fast, given enough manpower.
Having no experience with using gradual typing, I wonder if there's any stable equilibrium here between "thoroughly dynamic" and "type declarations everywhere".
In any case, as someone who started with Python and started preferring static types later on, I really hope this gets used.
Already, anyone seriously using pylint or other "normal" python linting tools uses comments like that to give extra hints to the linter:
type of thing. Yes, it's a bit weird, and yes, it does teeter right on the edge of the comments as syntactic value precipice, but I think lands just on the alright side.[1] http://www.ybrikman.com/writing/2015/02/06/are-static-typing...
The way I see it, if you find yourself in the situation where explicit type checking is important, there's probably something wrong with your process or team. Either your are not testing properly, or your team's mindset is more adjusted to another language.
The danger I see with this becoming widespread is Python becoming somewhat like C++ where it's very easy to come across code one can't easily read because it uses a different subset of features than you're used to. This sort of "language accents" so common in human languages is something that should be avoided in computer languages, IMHO.
I think that most people if they really think deeply about it would say that all things being equal that static typing is a good thing. The problem is that all things are not equal and that the cost of extra syntax, boilerplate, etc can completely outweigh the benefits of of that static typing (as the GP post clearly believes). I was a huge dynamic language fan until I started using Scala full time and since then I've gone completely the other direction to being a static fan. I suspect as more people start finding their way to tools which provide static typing guarantees without the syntax getting in their way so much that we'll find a nice middle ground.
C++, Perl and Haskell have operator overloading and it gets abused something rotten to produce "concise" (a.k.a. line noise) code. Python also has operator overloading and it is used sensibly, as it should be. Why? It's a cultural issue; readability matters.
Python is your language, please use type-hints responsibly :) """ I would add metaclasses, generators, etc. all these are already enough to write horrible things. It is indeed all about "culture", readability is really the cornerstone of Python culture. Type hints when used responsibly are fantastic tool. You could be surprised but they really improve readability, it's like a succinct docstring. I discovered this while recently reading through one large codebase. Moreover, typechecker will tell you when your "docs" do not reflect actual semantics. Finally, I would like to point out that typing.py and Mypy are pure Python, no magic :-) At the same time "import typing" is very in the spirit of "import antigravity". I hope Python gradual typing could become alternative to Java/C++/etc. BDSM-style typing and one day we could say: "Come join us! Typing is fun again" :-)
That's fairly funny coming from a discussion about a language that overloads '+' for strings and numerics, and overloads ==/!= similarly. Perl uses '.' for string concatenation and '+' for numeric addition, and uses eq/ne for string equality, and ==/!= for numeric equality. There's a reason for that.
Overloading is not necessarily used that often in Perl. It's a module that's part of the core, but it's fairly clunky and I rarely see it in the wild except for that spots that it really makes sense (DateTime object boolean comparison comes to mind).