I think your point about disingenuous arguments made by static typing proponents is mostly reasonable, but I don’t think those are the only arguments to be made for strong static typing.
Other benefits of strong static type systems are compiler-enforced documentation (through types) and ease of refactoring. Of course, working in a typed system does constrain you, but I would argue that the cost/benefit ratio is usually quite good. I don’t typically feel very constrained when writing a program in Haskell, compared to Python. I do generally stick to “boring” Python code that would have passed a type checker if Python had one. It does depend a little on the type of application. For writing a compiler, I prefer Haskell, but for doing data-munging and one-off scripts, I prefer Python.
However, arguing about the cost/benefit ratio of programming language features is often difficult, since the benefits and costs are hard to quantify. I do think that it isn’t reasonable to measure the cost of a type system by porting a program from a dynamic language to it, since doing large scale rewrites from a different language is not a typical task. It’s also hard to tell which parts of the porting process are “extraneous” and which parts aren’t. If I port a program from Python to Lisp, I will also have to do some significant extra thinking to make it work, but it isn’t because of static typing of the target language. Porting between different languages is just inherently difficult, and will always involve non-trivial “extraneous” effort. Maybe it’s more work when going to statically typed languages, but it’s not a reasonable measure in any case.
> Other benefits of strong static type systems are compiler-enforced documentation (through types) and ease of refactoring.
I do agree if "compiler-enforced" is your target then by definition you'll choose compiler enforcement.
For me the cost is too high. I'd rather solve my documentation needs through other far less costly means.
> ...ease of refactoring.
This is one of the lies espoused by the strong static typer. The claim here usually is that the compiler will tell you where you're broken through each step of the refactor.
The irony is that the effect is the opposite of what is claimed: requiring a refactor to be formally/machine-verified correct through each iteration is a huge drag on refactoring.
In a non-strongly typed language I can iteratively refactor and execute parts of my program even if a formal verified/strong-type prover would reject the program.
This equates to way better throughput/speed over the formal static verifier/typer.
Formal static verification may give you a host of benefits but in what most of us are doing Time is the most important resource by far. And formal verification/strong-type systems are downright hostile to Time. Which is especially offensive because the claims of stability can be readily achieved through much more efficient and agile techniques than formal verification.
Things are of course not so black-and-white. It is hard to discuss these things at a general or abstract level, since things are often different in practice than they are in theory. But my point was to show that there are actual reasonable arguments that you can make in favor of and against static typing, without being disingenuous. For example, you can argue that static types hurt more than they help during refactoring, but the claim is not so obvious that anyone who says otherwise is simply a static typing zealot.
Other benefits of strong static type systems are compiler-enforced documentation (through types) and ease of refactoring. Of course, working in a typed system does constrain you, but I would argue that the cost/benefit ratio is usually quite good. I don’t typically feel very constrained when writing a program in Haskell, compared to Python. I do generally stick to “boring” Python code that would have passed a type checker if Python had one. It does depend a little on the type of application. For writing a compiler, I prefer Haskell, but for doing data-munging and one-off scripts, I prefer Python.
However, arguing about the cost/benefit ratio of programming language features is often difficult, since the benefits and costs are hard to quantify. I do think that it isn’t reasonable to measure the cost of a type system by porting a program from a dynamic language to it, since doing large scale rewrites from a different language is not a typical task. It’s also hard to tell which parts of the porting process are “extraneous” and which parts aren’t. If I port a program from Python to Lisp, I will also have to do some significant extra thinking to make it work, but it isn’t because of static typing of the target language. Porting between different languages is just inherently difficult, and will always involve non-trivial “extraneous” effort. Maybe it’s more work when going to statically typed languages, but it’s not a reasonable measure in any case.