While on the subject of static typing, is anyone aware of any good argument against it?
However, once you pivot into needing maintainable software with more guarantees about correctness, static typing becomes extremely important.
The problem for python is that it originated as a language for less-formal programs but cultural and labor-market forces resulted in those programs getting shipped as production software. It's not so elegant when it's being bolted on, and there's a large subset of python developers today who genuinely don't need it.
Doesn't it just require you to express the interface you're already using and expecting to use?
> The problem for python is that it originated as a language for less-formal programs but cultural and labor-market forces resulted in those programs getting shipped as production software.
That's not a problem at all, as Python's type annotations and mypy clearly demonstrate.
> That's not a problem at all, as Python's type annotations and mypy clearly demonstrate
Gradual/Optional typing is a great way to solve the split needs, but I was making the argument for why people might not want to use static typing in python even though it's available.
Forgive me for asking, but did you made any point that provides any basis for refusing to use static typing?
I mean, failing to meet an artificial and unmettable and largely subjective bar regarding academic purity of type system implementations is not a valid argument. The average pythonista does not care about convoluted type theories if all he does is pass a string or int to a function, and doesn't want his program to blow up if they pass by mistake an int instead of a string.
Depends on the type system. Some type systems have a lot of ceremony around types and force you into contrived abstractions. For instance, in Scala, if you wanted to have a function that can print a name of an animal or person, you could overload the function, create a "nameable" trait and have both Person and Animal implement it, or create a union type.
In typescript you could just write
sayHello(thing: {name: string}) { ... }
or a union type
sayHello(thing: Person | Animal)
or even Pick out a group of parameters of both Person and Animal
sayHello(thing: Pick<Person | Animal, "name">)
Same with Omit
Types in typescript are incredibly flexible and useful despite being discarded at compile time. I hope python goes down this route.
Compile time structural typing like approaches tend to use typeclasses and implicits. Bit more boilerplate, but no runtime hit or risk of failure if reflection access is denied by the JVM security manager.
Intuitively, yes. However there is actually the Curry-Howard correspondence that states: A type is a theorem, a value with that type is a proof that the theorem is true.
In that sense static typing always has you prove something, but when going from dynamic to static typing it's not the proof that is the problem – you already have that. The problem is figuring out what you're proving or how to express that property in the language of the types.
This is what I don't get in these silly "anti-static typing in python" rants: the all-or-nothig logic with the goalpost moved to an impossible to reach place where even academic purity, which is met nowhere at all, is deemed too loose to justify the effort.
But the whole world already manages to implement and adopt static typing. Where's the practical problem?
Meanwhile, Python does indeed have a working static typing system, which is optional and does do wonders, but for some reason static typing detractors take a militant step against it.
Why?
Is this a contrarian thing?
I didn't intend to say "this is really hard, therefore let's not do it", I merely meant to provide additional background on the excerpt
> Static typing inherently requires you to prove things about your program
that you replied to. I assumed they were referring to this theoretical connection rather than a practical concern and wanted to elaborate for those previously unaware of this correspondence.
1. Static type checkers increase compile times. This is an acceptable tradeoff if they can catch bugs at compile time, but not if they still still allow bugs to occur at runtime.
2. If you're building a system which has to interact with other systems a lot, static types can be a hindrance if your static type system and their type system don't agree on fundamental things like how data should be modelled. This manifests itself as things like the Object-Relational Impedance Mismatch[1]. You would end up writing a lot (A LOT) of code to bridge the two, and in general, more code = more bugs.
3. Static type checkers can have bugs or quirky behaviour. This can lead to a lot of wasted time, and/or inelegant workarounds that makes your code less understandable (and therefore, more likely to have bugs in the future). This is one that I encountered recently: https://typelevel.org/blog/2018/05/09/product-with-serializa...
4. It's surprisingly hard to find any research that can demonstrate that static type checkers actually lead to fewer bugs.
[0] Python, Clojure for dynamically-typed languages, Typescript and Scala for statically-typed languages
[1] https://en.wikipedia.org/wiki/Object%E2%80%93relational_impe...
It should be noted that this potential impact on compile times amount to a few seconds.
> 2. If you're building a system which has to interact with other systems a lot, static types can be a hindrance if your static type system and their type system don't agree on fundamental things like how data should be modelled.
I fail to understand how failing to comply with a contract is a type checking problem, and one which goes away if you no longer perform validations.
> 3. Static type checkers can have bugs or quirky behaviour. This can lead to a lot of wasted time, and/or inelegant workarounds that makes your code less understandable (and therefore, more likely to have bugs in the future).
I'm not sure if your example is valid, as in your blog you quite openly state that the root cause of your bug was your failure to specify the right return type. You can't really fault a system by complying with the definition you've provided.
> 4. It's surprisingly hard to find any research that can demonstrate that static type checkers actually lead to fewer bugs.
A quick search in Google Scholar for "static type bugs" popped about 4k search hits, the first of which is an article on quantifying detectable bugs on javascript which states that switching to typescript allowed 15% of public bugs to be detected.
a) You're going to write unit tests anyway. Type errors are not especially likely to slip through good testing, nor are they the most interesting kinds of bugs that can slip through good testing.
b) Null is a value of the wrong type, and most type systems let that one through.
c) Values have a habit of coming from outside the boundaries of the type system. Sockets, files, etc. You will always have to deal with (or reject) arbitrarily wacky inputs at runtime.
c) Static typing leads programmers to overspecify data and make programs unnecessarily brittle. Many struct/record types could be replaced with maps + runtime checking that the appropriate keys are present, while letting other keys pass through. Then our programs would not so often require modification to support new uses. (TBH I think Go's type system, of all things, takes a decent step toward this one with its implicitly satisfied interfaces).
a. Yes tests are still needed but you need far less of them thanks to type you can focus testing on the critical logic instead of validating input and output types.
b. Solved issue in modern pl, even php considers null a value of separate type.
c. This is a good point, but with values coming from outside the system, I'm forced to do run time checking because of types which makes the whole program more less error prone.
d. This is a very valid point for most mainstream typed programming languages, row polymorphism is one technique which helps here. Every function only specifies the key's it needs to work so it can receive arbitrary records. I believe this is also possible in python by typing out dict keys and values.
In particular I would like to see the compiler enforce that you either return a legitimate value or raise an exception, and that the caller does not go down a path that calls for a value if an exception was raised. I hate that a reference can get 10 miles away before you discover there's no data there, and it being wrapped in Option or ? or a technically-not-null zero value doesn't mitigate that.
As the data moves further down into your core functions it should become more well defined and highly structured.
Basically you should parse messy data into the types you need and then you don't need to validate the data in each of your functions.
How to enforce this is a tricky problem for the compiler, maybe it's architectural pattern that can be enforced by libraries and frameworks.
I fail to see the point of this remark.
At best, you're arguing in favour of reinventing the wheel. With. Every. Single. Call.
At worse, you're somehow arguing in favour of being far less productive by having to fill in boilerplate code to run your own hand-rolled and error prone and hard to maintain typing checks.
Where's the value in this?
> b) Null is a value of the wrong type, and most type systems let that one through.
I really see no point in this assertion. So what if "most type systems" handle a specific type in a way you don't personally like? Are you writing your software based on Nond alone? Just specify your type and let the static type checker flag an error if it catches the possibility of a type seeping through an interface. Heck, Python's type hints system already support None, Optional, and even union types. You can also double-check with unit tests and runtime type checks. The TypeScript community considers this a solved problem. Why should this be of any concern to the Python community?
> c) Values have a habit of coming from outside the boundaries of the type system. Sockets, files, etc. You will always have to deal with (or reject) arbitrarily wacky inputs at runtime.
I fail to see the relevance of this point. With static type checks you specify the interface you're expected to support. You write and test your code based on that interface, and if the language enforces it then everyone, including your dependencies, also declare a contract that they comply with.
How is that a problem? At all?
> d) Static typing leads programmers to overspecify data and make programs unnecessarily brittle.
This assertion is quite wrong. At best, you're complaining that there might be a programmer somewhere that over specified an interface. How is this a problem? At all?
Meanwhile, let's look at the real world. Even if you intentionally turn a blind eye to what's already offered by Python's type hints, just look at how TypeSript handles interfaces. With it, you can quite literally specify that a function's input/output parameter is just an object that might have a key of acertain type. Then, to move the dial away from loose and into rigour, you can use type guards to infer more specific types. Why is this supposed to be a problem ?
I work in statically typed languages for a living. On the whole I think this is a sensible choice for my employer. Sometimes I don't like it. Sometimes when I have a choice (personal projects, or ancillary scripts/utilities) I'll reach for untyped Python. These are the reasons.
a) The type checker is a lifeline that will save you from one kind of error in untested code. But there are lots of ways to screw up untested code. You need testing anyway. And what will be caught statically by the type checker, will be caught at runtime during an adequate test suite.
b) Nullability invalidates the guarantee that a type system is supposed to provide: that values are the right type. The boilerplate, error prone check is necessary anyway to deal with the null. Yes, there are better type systems that don't have this problem. But static typing as actually practiced today (in general, I'm not talking about Python) has this problem very often.
c) This is true only if you're a library. Your type system can't statically guarantee anything about the bytes that will arrive on a socket, which is your actual interface when you're a network service. Parsing and validation must be done at runtime.
d) Over-specification of data is endemic to the culture of static typing. In the large, people think they need to map any values they receive to an internally defined struct or class, dropping any parts of the record they don't understand. Not doing this is seen as incorrect, irresponsible, or as you put it, less rigorous. But doing it leads to a lot of coding time wasted on mapping between representations and threading new fields through all the places a record is handled. Some static type systems offer facilities to help alleviate this problem. I'd argue that to the extent you're using those facilities, you're walking back down the spectrum towards dynamic typing.
A dynamically typed language's datastructures don't need to know anything about what they store. This is typically done behind the scenes as storing pointers to the data instead of the data itself, and then the data can be dynamically cast to the appropriate type when used. The result is that a list is simply a list and feels very natural for a programmer to interact with. On the other hand, a statically typed language's datastructures have to make one of three ugly compromises.
Java uses Generics, where the type is erased, causing interactions with datastructures to act dynamically typed while everything else in the language is statically typed. While this sounds as simple as dynamically typed languages, in reality the border between the statically typed and dynamically typed parts of the code are complex with odd syntax such as "<T extends Comparable<T>>" or "<? extends T>".
C++ uses Templates, where special functions called templates have extra syntax for the caller to specify what type is used. The template function is then copy-pasted behind the scenes with its variable type replaced with the specified type. This maintains the static typing but at a high cost as it leads to strange, complex syntax and ugly, hard to read errors.
Finally, C uses manual memory allocation. This prevents data structure libraries that easily work with multiple datatypes from being able to be created. However, C uses an interesting trick to provide support for simple arrays: the size of the array is the size of the element times the number of elements, and the memory address of index i is the base pointer of the array plus i times the size of the element. Using these mathematical sleights of hand, C can appear to provide datastructure support, but in reality this support only extends to arrays of a fixed size. I'm sure there are plenty of ways around this to actual build complex datastructures in C, but in my opinion none of those ways are nearly as friendly as dynamic typing, generics, or templates.
I remember that because of an essay on type erasure by a CS professor that researches language design. His comment is a sign your your language and compiler are well designed is the ability to do type erasure. And what's really important is to not do type erasure.
I think JavaScript's huge success in the last decade is primarily attributed to the plug-and-play dependency ecosystem and dynamic typing
Beyond that, not much
What's the barrier exactly? And keep in mind typescript's growing popularity and momentum, which states quite clearly that the javascript community is more than willing to tolerate added layers of complexity just to be able to use static typing.
It was also free. At the time, IDE's and compilers were pretty expensive in the Windows world.