Static types in Python
blog.zulip.org
blog.zulip.org
One comment to the article author: Tell people how to install mypy. I started by trying 'pip install mypy', then wondered why I didn't end up with a mypy executable (you need pip3 install mypy-lang, mypy is an unrelated package).
Consider the first example,
def sum_and_stringify(nums: List[int]) -> str:
return str(sum(nums))
I really feel like in order to get the best of duck typing, you need a good syntax for describing types by usage, not by explicit name. Please let me know if I'm missing something, and this is actually more expressive than the documentation suggests.
The concept of 'type' is overloaded with too many meanings these days. It started out as a what-storage-to-allocate and which-instruction-to-generate (int v float) concept (FORTRAN I, variables starting with I..N are ints, others real). Deep class hierarchies muddied the waters by overlaying the idea of whether or not a class implements a particular property or method, and how to locate the property or method that you want.
Python shows us that types and protocols/interfaces are two very different thing. In Python, asking 'isinstance()' is usually a bad idea unless you are doing something very low level, low level as in next stop is a C extension. The missing predicate in Python is 'hasprotocol()'. Abstract base classes can be used to accomplish that: isinstance(foo, SomeABC), but I think the intent could be more transparent with different syntax.
I like the idea of a hasprotocol or supportsprotocol predicate, certainly over usage of isinstance, since one of the beauties of duck typing is that it works without requiring the type hierarchy. The tricky part will be in allowing you to define your own protocols, like "has these attributes/methods". An example would be the difference (or lack thereof) between classes and namedtuples.
* https://docs.python.org/3.4/library/collections.abc.html * https://hg.python.org/cpython/file/3.4/Lib/_collections_abc....
def __subclasshook__(cls, C):
if cls is Iterable:
if any("__iter__" in B.__dict__ for B in C.__mro__):
return True
return NotImplemented
Interesting perspective. This would seem to be pretty well described by parametric polymorphism with constraints (Haskell-style polymorphism with typeclasses). In that context, too, we are often well served staying as generic as possible, and asking at runtime about the type of something is a bit of a code smell (and only possible where you have a Typeable constraint available).
# let f obj x y = (obj#m x)#n y;;
val f : < m : 'a -> < n : 'b -> 'c; .. >; .. > -> 'a -> 'b -> 'c = <fun>
Note the inferred type signature for this: the first argument is of type <m : 'a -> <n : 'b -> 'c; ..>; ..> - i.e. any object that has a method named m (and possibly some other unspecified members - that's what ".." means), with said method m having a signature that allows us to pass some 'a, and returning another object of type <n : 'b -> 'c; ..> - i.e. something with a method named n that accepts 'b and returns 'c. 'a and 'b' are then used as types of x and y, respectively, and 'c is the the result of f.
So effectively, this is full-fledged duck typing in the vein of Python objects, but captured on type system level.
Or: Maybe haskelltyping
# optionally: Number = Union[int, float, complex]
def sum_and_stringify(nums: Iterable[Number]) -> str:
return str(sum(nums))
Which is for practical purposes impossible.
Semantically, the presence of __add__ and __radd__ is a minimum, not sufficient.
Edit to add: To be clear, sure the result of calling this on any arbitrary sequence of addables might be semantically nonsense, but that's not the purpose of a type checker. It's only to verify type safety, i.e. you won't get runtime type errors if you give me at least this kind of thing.
A more constrained type throws away "the advantages of Python's duck-typing", but it also throws away disadvantages, and that can be precisely what you want.
We either disagree about the purpose of a type checker, or we disagree about what can constitute a "runtime type error". If a type checker can catch inconsistencies that would lead to my returning "semantic nonsense", at low enough cost, I absolutely want it to. Obviously it won't be able to catch all such inconsistencies in all cases.
sum_and_stringify :: (Show a, Monoid a, Foldable t) => t a -> String
sum_and_stringify = show . foldl mappend mempty
In the case of Python, though, coming from no static type system or verification at all, I would only ask of this tool to turn runtime checks (type errors caused by arguments lacking __iter__ or __add__) into static checks. Anything on top of that would be fantastic, I agree with you on that, but I wouldn't ask for or expect it.
Finally, thanks for all your comments - I appreciate the discussion.
Ah, we probably do agree more than it seemed. "The MyPy team has done its job even if that's not possible/reasonable" is a statement I'd endorse - especially in the short-to-medium term.
Discussing the Haskell...
String concatenation actually does associate; in fact String does form a Monoid over concatenation, and has an instance visible from Prelude - specifically the list instance, because Haskell strings are just `[Char]`.
The only really "nonsense" thing about using a string here that I see is that we wind up with quotes and escaping in the result when we `show` the string. If the purpose of this is "gather results and format for logging", that might be fine.
Numeric types don't have an instance of Monoid, because there are two to pick. You can pick them with newtypes, but here that's a bit awkward (`sum_and_stringify . map Sum`? feels redundant), and then the Show will give you something like "Sum { getSum = 3 }", which is probably not what you want either...
Using Num rather than Monoid probably has better ergonomics, and may be closer to intent anyway. That is to say:
sum_and_stringify :: (Show a, Num a, Foldable t) => t a -> String
sum_and_stringify = show . foldl (+) 0
I think the biggest issue here is that the example is so devoid of context (probably necessarily) that it's hard to say what good style would be. In actual code, a function with that name should probably have a very general signature - but we likely shouldn't be writing a function with that name. Why are we wanting to "sum and stringify" as one action in this way? Is that something that might change? Will the uses want to change together or are we just Huffman coding? With a domain-relevant name, we'd have a sense of what ways it makes sense to restrict the types.
> Finally, thanks for all your comments - I appreciate the discussion.
Likewise!
>Using Num rather than Monoid probably has better ergonomics, and may be closer to intent anyway. You're probably right on this point, in all honesty. I think I'm over-generalising the original intent.
>With a domain-relevant name, we'd have a sense of what ways it makes sense to restrict the types Yes, I think this is the classic helper function vs library function quandary. If you wrote it to help yourself right now, it's often good to be very specific with the name and signature. That way if later you need to add more functionality you can without changing the name or restricting the signature. If you wrote it as a library function, it's good to be generic, to let as many people use it as possible. And in this case there should never be a need to change the function, it does what it does. If you need something else you just create something else.
It's so catchy an acronym, and so seemingly self-explanatory, a lot of people don't realize it was originally framed in terms of knowledge, not syntax. So if syntax happens to be the same in N places, but in each of those places it is the way it is for a different reason, consolidating may not be "DRYing up the code". On the other hand, if I need to say "there's a text field here" in my markup and also in my logic, that could be more DRY even though the syntax looks nothing alike.
Tying this back here, we find as a corollary: when factoring out code we can ask ourselves "what piece of knowledge does this represent?" If it is knowledge about the language (this is a good way to sort things) it probably goes in a library, and should probably be very general. If it is knowledge about your domain (this is how we escape HTML), it probably goes in a domain-specific library, and it should probably be somewhat less general. If it is knowledge about your application, it probably goes in your application or an application-specific library, and should probably be pretty specific.
mypy will then tell you if you used your documented code wrong, according to your documentation
also sum excludes summing of strings if I remember correctly, so its any object that has an __add__ and __radd__ and isn't a string or subclass of string. which is just a bit insane to try and express on one line!
On the point of documentation, this is potentially a fair point if you consider that you probably wrote this function for a particular usage and you know at design time that you're really only ever going to give it a list of ints (if you strip the types away, the parameter is still called nums which suggests that's what was really intended). In reality, the function is actually much more powerful than that, and if included in a library, many people could use it for many more things than just that.
I think all this says is that design and documentation considerations for functions in distributed libraries may be different than those for functions used locally. Something I certainly agree with, but not really a criticism of the parent point.
Correct and concise documentation is incredibly valuable.
For documentation to stay correct, it must be checked and updated as situations change. Types and assertions can both play this role. Tests can play this role.
Names also play this role - they are not mechanically checked, but "is my use here consistent with the name" is a check any programmer is applying as they work. This actually argues a bit against renaming refactor tools - if I am changing a name, I should be making sure that it squares with existing uses. From this perspective, checking of function parameter namess is weaker than checking of function names, since the names of the parameters typically do not appear at the use site - very different than the assignment of other variables.
def sum(iterable):
r = 0
for v in iterable:
r += v
return v
>>> sum(['hello', ' world'], '')
TypeError: sum() can't sum strings [use ''.join(seq) instead]
Not sure if this is of interest to you, but the Nim[1] programming language offers a feature that allows you to do exactly what you described. It is called concepts and is documented here: http://nim-lang.org/docs/manual.html#generics-concepts
As a bonus, Nim is also quite Python-like.
> mypy considers an int object to be valid whenever a float object is expected.
> Use Iterable for generic iterables (anything usable in `for`)
Thus you should be able to get a more broadly correct (though still not 100% if you have your own types implementing __add__ and __radd__) like this:
from typing import Iterator
def sum_and_stringify(nums: Iterator[float]) -> str:
return str(sum(nums))
http://mypy.readthedocs.io/en/latest/class_basics.html?highl...
Of course type checking can catch some problems. The more extremist elements of the static types proponents seldom seem to ask the cost of adding types, and making some otherwise generic/overloaded operations harder to implement (e.g. - excess clutter in some "wordy" type systems, particularly in the C lineage where declared identifier names follow the other verbiage). We need more tools that allow us to easily nail down fixed interfaces to avoid errors, but still allow flexible / dynamic / metaprogramming type code when needed, without having to jump through hoops in either case.
Don't be a static typing extremist! (or throw the baby out with the bath-water, either, I guess)
Keep in mind, static types can also help performance, tooling (refactoring, cross-referencing, etc) and human understanding.
This is not an argument for or against static types; it is simply a longer list of what they can be useful for in the many situations.
I just don't want to be forced into a jail cell 100% of the time. I want an escape hatch to do the needful once in a while to do something that the language designer never planned for.
Note that I am referring to type systems with succinct syntax, type inference, structural typing and ADTs.
Here is a little list of drawbacks of static type systems with features like you describe (parametric types, ADTs...): Type dependency hell (banana, monkey, jungle, etc), having to fight/convince the type inferencer to accept any but the simplest things, having to type many things twice.
Looking at Haskell, "almost everything is inferred" is a lie in my experience. You are encouraged to write code using higher-order and highly parametric functions. If you do, the error messages you'll get if you don't annotate are plain sick. Another problem is that the type system provides no convenient escape hatches, while it's not powerful enough for typical programs. Many "successful" example designs I've seen are either _really_ simplistic (to the point where it's obvious that the better design wasn't chosen simply because the type system makes it really inconvenient), or have some _really_ terrible internals hacking in it (which might be the largest part, be impossible to understand by most developers, and break with the next compiler version).
Looking at C++, a practical example is vector. It's a useful tool (automatic memory management), and very likely to be all over in your function signatures. This is very bad in terms of modularity / reusability, because your functions are not defined using reasonably general types (pointers to arrays).
Many of these very real pains just aren't there with Python code, which has better modularity at the cost of being a little sloppier.
These days I look at static types mostly as tools for generating fast machine code (I doubt that much more than C types is needed here) and as tools for enabling nice syntax (OOP protocols like in Python can do that too, but they are very dirty). These things however are only needed at the very optimized parts of your average project.
So I think a good way in many cases is to go the Python route, and check types dynamically at strategic points to assert value integrity and enable transition to highly optimized (with static types) routines.
For now a few words that I hope I won't regret later (apart from the things I mentioned): The bulk of invariants / assertions in many real-life programs can't be expressed with mainstream type systems at all. They are too specific or only come to life dynamically. Things like: This array of integers is sorted ascendingly, and that index is a valid index into this other array which points to a number between 48 and 58. Or this table's column over there contains only values that are also present in that other table that just happens to be present now (but must be expunged from working memory after the next subtask). Checking if an integer fits in 8 bits and then converting to a byte is no safer in Haskell than in any other language.
So much to put the usefulness of mainstream types for static correctness in relation.
Now much of the tinkering that is going on in Haskell projects seems to be shoehorning yet one more real-world invariant in another crazy type. Maybe the next brilliant idea works for one more toy case in the end. Great, but the cost/benefit ratio is just bad.
I think the most important thing in software architecture is modularity, because the most pressing need in software development is the need for change. If my project is very modular, it's sufficient to have clear entry points to each module with very simple data types in the signature. The internals can be a dirty hack and rewritten later, or the module thrown away when the idea turns out bad. Interfaces on the other hand can't be changed as easily since they affect much more code. So a good approach is making interfaces that accept tables, augmented by a textual description of invariants so the user easily "gets" the meaning of the data and can reshape/preprocess the data as needed. This enables isolated rewrites of modules. It also enables creative use of data in unforeseen ways. Clever types on the other hand have a very strong influence not only on the design of module interfaces but also on the dependent modules' implementations, because 1) it's more cumbersome to reshape complex structures in a way suitable for clean implementation, and 2) because type systems can't usually transfer invariants to reshaped representations (and after all the goal was to let the compiler handle the invariants, so reshaping is a no-go).
In short, complex types _kill_ modularity because they have far too much influence on data layout.
For real world programs, what Haskell is great at is statically finding trivial interface usage errors like, don't call this with a NULL pointer, or this parameter must be a functor instance (because the actual data might be too ugly to admit). Turns out that that's all nice and well, but the machinery is a huge cognitive and economic overhead, while running some python client code of a sane API once typically brings such usage errors to light just as well (profane things. TypeError raised. Seems it tried to iterate over an int, so you must have gotten the argument order wrong etc).
Which is beside the point, since partial coverage of invariants is still very useful.
For when it's not, there's Idra, Coq and such.
These are difficult to encode in a way that lets the compiler check the code that sorts or calculates an index.
They are trivial to encode in a way that simply tags the values. I still need to be concerned with making sure my sorting is correct, but that's a very isolated concern. I still find it very useful to know whether I've called a function on the array that depends on it being sorted, and that doesn't require any heavy lifting at all.
They also have disadvantages in that they separate data which is only different by some aspects, but not most others. (For a simple example, the printing function is not interested in a "safe HTML" Tag. The effort needed for constant tagging and untagging (or using "Stringy" classes, or the cognitive overhead you need to pay if you found a clever way to remove the syntactical burden) is too big except in very few cases.
Fair enough. I have.
> There are just too many "tags" (often one per line or group of lines).
Where the burden outweighs the benefit, you always have the freedom of typing things too loosely - to be sure, without something like refinement types, there is a granularity you can easily try for that's just not worthwhile. But that's a pretty different thing than "can't be expressed with mainstream type systems at all." For me, the questions are 1) how far does this type move information in its use through the program, and 2) what part of these are likely to change in ways such that I'll want to be notified about this piece of code here?
Actually, in GHC 8.0 you can do exactly that, with the TypeApplictions extension.
Prelude> :set -XTypeApplications
Prelude> :t traverse @[]
traverse @[] :: Applicative f => (a -> f b) -> [a] -> f [b]Either that, or you might not work on toy projects.
In my own practice, most transformations don't involve relations over more than 5 variables with mostly obvious types. Yes, this is hard to use:
https://tronche.com/gui/x/xlib/window/XCreateWindow.html
But then 1) there might be nicer ways to design an API and 2) at these few places the implementor of the API can just insert value assertions.
It would be a toy project that only (or mainly) has those as all the types you need to remember -- so that just proves my point.
Also the 'type' of an email address is an unsolved problem -- if we're talking type checking. It's not a string, and it's not solvable with regex either. So bad example all around.
Also, in Haskell one needs to encapsulate the real constructor in its own module to make sure the data is only constructed through a sanitizing constructor. That's quite some overhead (and makes pattern matching impossible).
What might be useful instead is first class "tags". In Perl6, you can subset types to values that match a condition (for example, strings that match an email regex (cough)). They are still strings so can be used unchanged with other functionality that does not need the tag. It seemed quite usable to me (applications are limited, though). However the creator said it's still expensive because they haven't figured out / implemented how to transfer invariants, so they are checked at each function boundary.
In Python, you can use duck typing: subclass str, it's a dirty hack but works very nicely.
The real world solution to the whole mess seems to me to be just to design a good dataflow into the system, so it's clear where you have a valid email address. Typically it's very easy: Just assert the invariant at the boundary to the external domain (for example, HTML form parsing). Now whenever there is a variable "email" in your program you "know" that it is a valid email address.
Is there no reason you could not create an Email class and have the method require its argument to be of that type?
If you’re talking about runtime type checks rather than mypy, well, they’re just verbose static types with less safety. (May as well just embrace the duck typing at that point by accessing email.local_part and letting the AttributeError propagate.)
Subclassing str seems like the most horrible way ever to represent an e-mail address. I would definitely write a wrapper instead – exactly like Haskell.
What do you mean by "tables"? I think of a database table of rows/columns, or a matrix.
It helps if the language supports creation of indices / reshaping (table joins, filters, making hierarchies).
That's why you define your functions as taking generic Iterators instead, which generalize pointers to arrays. Or, in more modern style, generic containers.
You can wrap that in a type erasure layer (lookup any_iterator) if you want separate compilation.
Or, in yet more modern style as slices. Or, ...
The only thing I miss from pointers + indices is optional bounds checking. Otherwise, it's the perfect tool for productivity (because readability, writeability, portability, modularity).
You can also do full Python-style "duck typing" statically. It's called structural typing, with native support from languages like typescript, purescript, etc. It's used a lot in web dev because it works well with Javascript's object model.
Using an explicit map for dynamic attributes at least makes you aware what is guaranteed and what is optional.
This removes much of the neat magic that such a dynamic approach affords to languages like Ruby, JavaScript, and, to a lesser extent, Python.
This is true for the JVM definition of 'generics', but it doesn't mean that arbitrary operations on a collection of types can be easily expressed with a given (static) type system. Run time type information + a dynamic type can ameliorate some of this, but that's shoehorning optional types into a static type system, and I don't think that's quite what you meant.
Think about a generic operation to diff two data structures: you need access to the members of the struct in a generic way. I don't think this is easily solved with static types.
How do you figure? This would require macros or runtime type introspection.
A specific example might be "serialize this json type without having to annotate the fields with how to serialize them".
Not if you structure your data using an appropriate data structure, like a map. After all, this is all structs in dynamic languages are.
> A specific example might be "serialize this json type without having to annotate the fields with how to serialize them".
Aeson does this safely and statically using Haskell's powerful static Generics.
data Foo = Bar Int String deriving (Generic)
instance FromJSON Foo
instance ToJSON Foo
data Foo = Bar {baz :: Int, qux :: String}Sure—but it's in spite of static typing, not because of it. You certainly give up any guarantees of avoiding runtime errors by detecting typing issues at compile time.
But that's what I would do (at least in Java) for this kind of transient transfer object, if left to my own devices.
https://plus.google.com/110981030061712822816/posts/KaSKeg4v...
(I would put myself in the "moderate liberal" camp, even if the languages Steve Yegge lists for that group are not my choice languages)
https://manosnikolaidis.wordpress.com/2015/08/25/jackson-wit...
That is a property of the library not of the language.
Java generics seem easy enough to instantiate and use, but the mess when you implement one really discourages people from trying, usually. And if you do, the result is often a poster child for FUGLY code. Try declaring a java 8 lambda parameter that works with collections some time, and using that in a few places - serious COBOL-fingers and eye-burn time. Even a Pascal style "type" or C style "typedef" mechanism would have greatly reduced clutter when trying to create code that implements (java) generic operations.
Die, Java, die :-)
It feels like type inference meets duck typing, but that's a good thing.
C# has the dynamic keyword (not to be confused with type inference via the var keyword), which basically allows to break out to dynamic typing. I find this to be significantly saner than the other way around.
Even if they don't do it very often, even if the IDE infers properties most of the time anyway, even if there's less code to have to be refactored, and most of the refactoring that could be automated is still automated.
I would rather use types most of the time for clarity and to help the compiler / editor help me, just not always.
:-)
IMO writing a type annotation, or knowing whether a type is an int or a string, is the of minimal help in pushing errors into the type system. A good type system you don't even have to write the type of things, it's inferred.
Better 'statically typed' languages allow you to push more errors into the type system and give you tools for creating stronger abstractions.
I like the idea of a hybrid type system where statically typed and dynamically typed parts coexist, OTOH, I can imagine it being difficult to implement.
That discussion was an eye-opener for me regarding type systems; to this day, I cringe when somebody calls, e.g. Python or Javascript a "typeless" languange.
There is no generally agreed upon definition of what the distinction means.
Second, the context here is whether or not the type system of a language is strong or it is weak.
I stand by my assertion that describing type systems as strong or weak typing is essentially meaningless. It's so far from descriptive that all 'strongly typed' ever really means is 'I like this feature' and 'weakly typed' means 'I do not like this feature'.
There are alternative, accurate ways of talking about what people think they are trying to get at when they use the terms strong and weak in relation to languages. They should be used instead.
There is some controversy over the strong/weak terminology, IMO mostly because almost no language is clearly strong or weak based on the definitions generally used[2]. I find it useful to think about whether things are done implicity, or whether you need to specifically convert types. Perl will happily add "1" and "1" to get 2, because the + operator forces it to be interpreted as a numeric type. Python will not, and expects you to convert to a numeric type first. Of course, exceptions to the rule abound.
1: http://stackoverflow.com/questions/2351190/static-dynamic-vs...
(0) Bash is strongly typed. Everything is a string, so there can't possibly be any type conversions, implicit or explicit.
(1) Any language with subtypes is weakly typed. For example, Haskell with Rank2Types or above: every lens is a traversal in a canonical way, and indeed the type checker lets you supply a lens in a context where a traversal is expected.
(2) Rust is even more weakly typed: boxes (as well as other user-defined pointer types) are implicitly converted to references, iterable objects are implicitly converted to iterators, etc.
There's no precise technical definition of "strongly typed", but AFAICT, the intuitive idea is that a "strongly typed" language prevents you, or at least makes it difficult to do things that aren't likely to make sense, like treating the same datum as a number and as a string in different places. This is independent of whether the language has implicit conversions.
If it were true that everything is a string, then yes, you probably could say it's strongly typed. It's laughable, but it is. Some single celled organisms are animals, as well. Assembly is generally the strongest typed language you can get.
But it's not true. Bash supports associative arrays.
#!/bin/bash
declare -A array_var
array_var=( ["foo"]="11" ["bar"]="22" );
echo "$array_var"; # Empty line
echo "${array_var[foo]}"; # 11
scalar_var="baz";
echo $scalar_var; # bar
array_var="quux";
echo "$array_var"; # quux
echo "${array_var[foo]}"; # 11
> (1) Any language with subtypes is weakly typed. For example, Haskell with Rank2Types or above: every lens is a traversal in a canonical way, and indeed the type checker lets you supply a lens in a context where a traversal is expected. > > (2) Rust is even more weakly typed: boxes (as well as other user-defined pointer types) are implicitly converted to references, iterable objects are implicitly converted to iterators, etc.
You're making very strong assertions based on my comment when I made sure to to say "almost no language is clearly strong or weak based on the definitions generally used", and even provided examples where the same language could be considered both strongly and weakly typed, depending on what aspect you were referring to.
"Strong" and "weak" are themselves relative terms, so make no sense unless comparing to something else. That may be a shared reference language, or the perceived common level of languages with respect to what is being discussed. I replied to the sibling of my original comment with some info about how I think about this. It's rarely useful to think of a language as entirely strongly or weakly typed, but certain aspects of it may or may not be (again, relative to some benchmark).
> There's no precise technical definition of "strongly typed", but AFAICT, the intuitive idea is that a "strongly typed" language prevents you, or at least makes it difficult to do things that aren't likely to make sense, like treating the same datum as a number and as a string in different places. This is independent of whether the language has implicit conversions.
Well, treating the same datum as a number and a string in different places is exacerbated by implicit conversions, which allow that behavior to succeed. I wouldn't say it's independent, I would say one depends on the other.
Really, whether they are well defined terms or not, I think it's still still useful to use them with some disambiguating context, as they express a concept otherwise hard to convey (if it was easy to convey, they wouldn't be so ambiguous in the first place).
I think a case could be made that any subversion of requiring the exact type defined or requiring manual conversion is a weakening of the type system, for the definition of weakening that we are using. The important consideration is that neither stronger nor weaker are always necessarily better or worse.
I didn't say it's the only useful thing, but it's perfectly reasonable to measure the expressive power of a type system (or any other language feature, really) by how much it buys you.
> can be seen as a weakening
Covariance and contravariance support by no means "weaken" a type system - they allow you to express more statically, not less.
That's exactly what expressiveness is. If a type system is versatile enough, you can express what you need to express without bypassing type safety.
> anything except the specified type
Even in this sense, subtyping doesn't weaken a type system. The definition of subtyping is the subsumption rule: given `S <: T` and `x : S`, you can derive `x : T`. (TAPL, p. 182) For similar reasons, adding ML-style let polymorphism to a type system doesn't weaken it.
> strong and weak is orthogonal to safety and expressiveness
Then what exactly is it?
I wouldn't say so. Perl is expressive. That expression sometimes comes at a cost of safety, but not always. Safety and expressiveness are not necessarily related.
> Then what exactly is it?
The exactitude of requiring exactly what is expected, and not allowing any substitutions. I'll explain my reasoning below.
> Even in this sense, subtyping doesn't weaken a type system.
Subtyping doesn't even always make sense when talking about strong or weak types. Some languages don't even have subtypes, yet we can still talk about how strong or weak their typing is just by referring to how different types interact, and whether conversion between them is implicit or explicit. Again, I'll call on Perl, which is useful in that it's very, very far from the type systems you have been describing WRT Haskell and Rust (and many languages that use static typing and inheritance).
Perl has two types of typing, variable (data structure) typing, and value typing. Perl is fairly strongly typed when it comes to variable types. It's either a scalar (which can contain many things, including references to other types), an array, which contains scalars, or a hash, which contains scalars (I'll leave out typeglobs and filehandles since they are fairly specialized). Until a few years ago, you could not supply a scalar where a hash or array was expected (e.g., you could not push($foo,"string"), you could only push(@foo,"sting"); ). You could explicitly dereference a scalar containing an array reference to an array and push to that, but it was an explicit dereference which required a @ prefixed the scalar[1].
Perl is fairly weakly typed when it comes to values within scalars. It will attempt to automatically convert the type to the appropriate representation such that the operation makes sense. Thus, adding two strings containing numbers requires no explicit conversion. Concatenating two numbers a string doesn't either. Neither do any string or numeric comparisons, as the conversion is implicit within the operator, as it knows what type it expects. This is why the expressions "1" + "2" and 1 . 2 in Perl are completely unambiguous. The first adds 1 and 2, yielding 3, the second concatenates the strings "1" and "2", yielding "12". The original type presented doesn't matter, it's implicitly converted as needed.
Subtyping, in this case, is irrelevant, because it doesn't exist in this language for these types of typing. It's entirely valid to talk about strong and weak typing in both these aspects or Perl, but they are both different and neither really matches the typing you are referring to with "type systems", because this language functions at a different level. The only way I can see using strong or weak typing as a descriptor across many languages, is to define it as how exact the type of data you are supplying needs to be to match what is expected. That is "strong" has entirely to do with constraints and explicitness. Anything that allows implicit action, even using a subtype which is known to be safe without some indication that you are raising or lowering the type explicitly so it can be used, is a weakening of that constraint (even if it's provably safe. Again, we aren't saying it's strongly safe, just that it's strongly constrained by type).
This reasoning leads to one of your original examples questions:
> Rust is even more weakly typed: boxes (as well as other user-defined pointer types) are implicitly converted to references, iterable objects are implicitly converted to iterators, etc
Yes. In some aspects, Rust has weakened it's typing in very specific circumstances to allow for more expressive programming, by not requiring explicit conversion when it can be inferred by the compiler. In this respect, Rust is more "weakly" typed that it could be, but it's also no less safe, no less fast, and more expressive for doing so, which I'm sure we would both agree is a good trade-off to make in this instance.
I hope that explains my view, and my reasoning, sufficiently. Let me know anything about my reasoning that confuses you, and I'll try to explain better (and of course feel free to poke holes where you see them).
1: Perl experimented with allowing core functions that expected an array or hash to allow a scalar containing a reference to such to work without the dereference, but ended up backing out that change.
Sure, but I was talking about the expressiveness of the type system, not the term language. The expressiveness of a type system lies in how much it tells you about your program, without having to actually run it.
> Rust has weakened its typing
I was trying to use reductio ad absurdum to question the validity of your definitions. I expected "Haskell is weakly typed" and "Rust is weakly typed" to be self-evidently false propositions.
Expressiveness can be described as expressiveness. I'm not sure why we would need to use strong/weak as an alternative to that term. IMO, it makes the strong/weak terminology less useful by tying it to this concept, which is only really relevant in some languages.
> I was trying to use reductio ad absurdum to question the validity of your definitions. I expected "Haskell is weakly typed" and "Rust is weakly typed" to be self-evidently false propositions.
I'm not sure if this is implying that we disagree on something that you still see to be self evident, or it's meant to explain why you included that and you no longer think it's a position worth holding?
In any case, I think it's worth clarifying that I didn't call Rust weakly typed, I said it hda weakened it's type constraints in a select few cases to increase expressiveness, where it did not cost in safety. (Constraints because everywhere you put strong/weak I think you can append constraints to be more explicit). I don't think it's controversial to say "Rust weakened constraints the type system imposed in some cases where it could be done safely, such as in iterable objects implicitly being seen as iterators in some cases", as that's clearly a bit less constrained than it could be.
Expressiveness is always relative to what a system is meant to express. The purpose of a type system isn't to write your actual programs in it. You use a type system to make sure that programs written in another language (a term language) make sense. So a type system is expressive to the extent it accurately captures the distinction between programs that make sense and programs that don't. (Of course, Goedel tells us that no decidable type system can perfectly capture this distinction.)
As for strong/weak, I don't think the concept is very useful without a clear technical definition in the first place.
Well, it's definitely not very useful in our case. ;) In all seriousness, as I said previously, I think it's useful for conveying a mixed bag of things to people that aren't very well versed in the specifics. If the person knows something about type systems, you should naturally have more specific language to fall back on to express your intent better.
In any case, I think we are way past of this being worthwhile to continue. I think we've plumbed the depths of this topic, whether we agree or not.
> Rust is even more weakly typed
Out of curiosity: if I'm not mistaken, this was an implementation detail of LISP machines [1], and allowed bytecode-level optimizations.
However:
s/was/is/g
s/could/can/g
[Source: I'm a mypy core developer.]
If you take that seriously, compilers can't use type information to optimize. It feels like Von Rossum is making life hard for the PyPy compiler project again. If they had hard type information, they could do serious optimizations. Guido's CPython still uses a CObject for everything internally, so it doesn't benefit much from this.
The direction that everybody else seems to be taking is that function parameters, structure fields, and globals are typed, but local types are inferred as much as possible. C++ (with "auto"), Go, and Rust all take that route. Type information on function parameters and structure fields is an important item of documentation; if the language doesn't support that, you need to put it in separate documentation or comments. But writing elaborate type declarations for local variables is no fun, and the compiler can usually infer that info anyway.
Or perhaps, he realizes that to require these typechecks at runtime would either
- require a massive rewrite of the CPython interpreter
- cause a performance penalty in code that is statically typed (there are pure python libraries that allow this, and yes your code runs slower)
Further, it offers a relatively narrow amount of help to pypy, which has already come out and said that they have no interest in using annotations for efficiency gains, because they're a jit and they don't need them.
Von Rossum on PyPy (2016): "Otherwise, there are specialized versions of Python like PyPy that are still around."
[1] https://bitbucket.org/pypy/pypy/src/default/rpython/translat...
I think that's a fair trade off, and easily doable. Those who want it and respect it get the speedup, those who don't don't lose anything.
If you have to double check types at runtime, you've already lost.
Now if it isn't correct, you'll probably get a segfault or some nasty error and it'll blow up.
I've run into that with functions that take NumPy arrays. You can pass a Python array, but "+" behaves very differently. For a NumPy array, it's element by element addition. For a Python array, it's concatenation. You want to catch that.
Mypy is not about optimising anything, it's about static correctness guarantees. If you're developing PyPy, type hints shouldn't be making your life any better or worse.
Lastly, the 'direction' you describe that everyone else seems to be taking, is the exact same direction mypy has taken. Type annotations are only required at the method/function level.
My_dict: defaultdict[int, List[int]] = defaultdict(int)1) Not type checking at runtime is exactly what people mean by static typing, because the definition of static typing means the checks are done before execution.
2) This does not make it harder to optimize, on the contrary if they generated type assertions it would considerable slow things down on the boundary of typed and untyped code.
3) C++, Go, Rust, Haskell they are fully statically typed, the only difference is they support varying levels type-inference which means you don't need to "type out the type" but it's really orthogonal to the whole optional/static/dynamic typing issue.
(When you have a real type inference engine, you spend a lot of time trying to figure out what it did, or why it didn't do something.)
That being said, I have never encountered a program that was hard to understand because types were inferred rather than explicitly annotated. I use explicit type annotations in two situations:
(0) As a compile-time analogue of printf debugging. Not exactly a joyous thing.
(1) At module boundaries, to control what modules expose to each other.
Perhaps the parent was trying to talk about "HM type inference" or something, but "type deduction" is also a fine name for a subset of type-inference, and perhaps more explicit for C++ and Go.
(0) Generating a system of type equations, by recursively scanning the AST.
(1) Solving the system of equations. The nontrivial nature of this step is what makes type inference, well, inference.
In Go and C++'s case, the generated type equations come out already solved (that is, of the form `TypeVar = TypeExpr`), so there's nothing to infer!
"Type inference refers to the automatic deduction of the data type of an expression in a programming language."
https://en.wikipedia.org/wiki/Type_inference
Which you'll notice C++ and Go, are listed as languages with type inference.
But you're right that they don't have as nearly as strong type inference as rust, which doesn't have as strong as haskell etc.
Depending on how simple "deduction" can be, that arguably includes every language that includes expressions.
And if the deduction is required to include usage information, it quite arguably excludes C++/Go style "var": a variable declaration is not an expression.
Generally, that Wikipedia article doesn't seem very good - check the talk page.
Woah! Excellent news. Really cool that they found a way to use this opportunity to bolster Python 3 migration.
Or does type documentation not matter that much, once it's being enforced by a tool?
Improves IDE integration, especially IntelliJ PyCharm's jump-to-source
- the official docs are useless, return types are often not documented (wtf ?) and docs aren't structured and clean. Python documentation is a giant mess.
- mypy is a god sent I used it from day one to document my Python code, but it needs better integration with python doc tools, 3rd party linters and co.
I'm ok with optional type checking. A team can make it mandatory during continuous integration while not breaking legacy code, but I hope mypy will be directly integrated to Python in the future and not a 3rd party tool.
Instead of a list of possible returns with some kind of prototypes you may be left with description: "The returned object is always a file-like object whose file attribute is the underlying true file object.".
See for example documentation for tempfile.NamedTemporaryFile [1]. This time possible returns are not in the separate paragraph as is in many other cases. You can't click anything expect TemporaryFile(), so you have to search for proper reference. The information is there, but instead of quick glance you have to parse and search more text.
Hoo boy. That's not a good thing. A consistent type system doesn't have "false positives". Reading between the lines, this means "the type checker is incomplete and allows incorrect types."
What is the story here with constraints, polymorphism, etc?
Currently you need to import things like Callable, Tuple and these don't exist in Python2. It is especially odd since I am using MyPy comment syntax, so MyPy needs import statements even when all types are inside comments.
I like the way Haskell puts type information above the definition.
This is a direct backport of the same `typing` module that's in the stdlib starting in Python 3.5.
(I'm one of the mypy core developers and work at Dropbox. We're using PEP 484 and mypy on a lot of Python 2 code!)
def f() -> "Bar": ...
def f() -> Bar: ...
Javascript is the bash of the internet. It's not that great but it does have a "killerapp".
http://groovy-lang.org/releasenotes/groovy-2.0.html
[2] https://github.com/shedskin/shedskin
Citing some Groovy 2.x Release Notes to prove a claim of "stability" for Groovy is like quoting an advertisement for Parmolux washing powder to prove its "effectiveness" at washing out dirt.
Not many developers bother with Groovy's static compilation annotations. It's used mainly as a scripting language for testing Java classes, gluing together Java programs, as a build DSL in Gradle, and scripting in Grails. When static annotations are used, their use is typically small-scale.
The primary Python execution environment is commonly referred to as CPython, as it is written in C. Other major implementations use Java (Jython [Jython]), C# (IronPython [IronPython]) and Python itself (PyPy [PyPy]). Written in C, CPython has been conducive to wrapping many external libraries that interface through the C language. It has, however, remained non trivial to write the necessary glue code in C, especially for programmers who are more fluent in a high-level language like Python than in a close-to-the-metal language like C.
Originally based on the well-known Pyrex [Pyrex], the Cython project has approached this problem by means of a source code compiler that translates Python code to equivalent C code. This code is executed within the CPython runtime environment, but at the speed of compiled C and with the ability to call directly into C libraries. At the same time, it keeps the original interface of the Python source code, which makes it directly usable from Python code. These two-fold characteristics enable Cython’s two major use cases: extending the CPython interpreter with fast binary modules, and interfacing Python code with external C libraries.
While Cython can compile (most) regular Python code, the generated C code usually gains major (and sometime impressive) speed improvements from optional static type declarations for both Python and C types. These allow Cython to assign C semantics to parts of the code, and to translate them into very efficient C code. Type declarations can therefore be used for two purposes: for moving code sections from dynamic Python semantics into static-and-fast C semantics, but also for directly manipulating types defined in external libraries. Cython thus merges the two worlds into a very broadly applicable programming language.
def primes(int kmax):
cdef int n, k, i
cdef int p[1000]
result = []
if kmax > 1000:
kmax = 1000
k = 0
n = 2
while k < kmax:
i = 0
while i < k and n % p[i] != 0:
i = i + 1
if i == k:
p[k] = n
k = k + 1
result.append(n)
n = n + 1
return result
I know some may disagree but I have found runtime reification of types fairly useful in the Java world (partly because Java does not have good code generators like OCaml/Haskell and partly because Java is not that expressive).
https://jugad2.blogspot.in/2012/12/mypy-python-variant-with-...
but had not tracked it much after that. Must check it out again.
The good thing about types is not that you can just annotate (or not with good inference not) and validate that some type is what you expect it to be. It's that with a proper type system you can develop better abstractions.
It's amazing. Zulip is Slack done right. Their threading/light-weight topic approach is second to none.
Another example of this is most of the prismatic/schema-esque frameworks for python to do validation on datastructures. Instead of saying foo must be { "name": "String" } (where there is a framework-specific meaning behind the literal word "String") we should take advantage of the built-in types and say {"name": basestring}.
End rant.
python3 type_annotations.py
def sum_and_stringify(nums: List[int]) -> str: EDIT: Solved: Either just list or List[int] with import:
from typing import List
Thanks for all the help guys! By the way I took the example from the mypy page. A classical case of 'critical line missing from example code' (as perfectioned by Bjarne Stroustrup back when)
At least this works: def sum_and_stringify(nums: list) -> str:
def sum_and_stringify(nums: list[int]) -> str: so either just list or List[int] with import, got it.
A classical case of 'critical line missing from example code' (as perfectioned by Bjarne Stroustrup back when)
How I found it: quick google search for "mypy validate list"
sum_and_stringify(nums: List[int]) -> str:
The commented version is much more acceptable.
----
It should work with the Python 3 syntax if you quote your type annotation. I.e.
def f() -> "Bar": ...
def f() -> Bar: ...
Yeah, you need to write `from typing import List` to get the generic List class that you can parameterize with an item type. As you pointed out, you can use the builtin lowercase-l list without importing anything, but that doesn't allow you to specify the item type.
---
imo, this is brutal. I'll just wait and see whether I'm proven right or wrong, but the extremely poor aesthetics of the whole thing bode badly.
You listed 4 specific languages, but the following things are each inconvenient in them:
- C: it's inconvenient to implement a quick prototype
- Ocaml: it's inconvenient that the stdlib is so small
- Go: it's inconvenient for scientific/numerical code
- TypeScript: it's inconvenient to run server-side
Python rocks in all of them (edit: the big exception being frontend webdev), in particular for quick prototyping. I think mypy is an exceptional and fine contribution to the eco-system and I really appreciate their effort.
How much I would like Webassembly to be ready to open the gates to other languages on the frontend land. Anyone here has more information about webassembly / python on the browser? I would love to know what is the current state of the art of running python on the browser and contribute to make the dream come true.
I have on my radar Brython [0], py.js [1](seems to be abandoned) and pypy.js [2]
[0] http://www.brython.info/ [1] http://pyjs.org/ [2] http://pypyjs.org/
I don't know what "strictly typed Python" is, but the type checking discussed in this post is 1) completely optional and 2) static. You don't have to do it if you don't want to, and even if you do do it, it doesn't affect in any way Python's runtime behavior or flexibility. You can have a codebase that works fine yet at the same time fails mypy's checks.
Also, no, we are not moving towards "strictly typed Python", even if that were a thing. PEP 484, which laid out the standard type hints, included this line in bold under "Non-goals" [0]:
> It should also be emphasized that Python will remain a dynamically typed language, and the authors have no desire to ever make type hints mandatory, even by convention.
I used typing with PyCharm for one of my project and it helped me to find several bugs.