Here's a fully typed insertion sort [1] written in Idris. It's over 260 lines long, and it takes non trivial amount of effort to understand it fully, and know that what it specifies is indeed what was intended. Meanwhile, I can trivially read and understand a 10 line Python version in its entirety.
Of course, you could argue that it's an extreme case, and that in practice you probably wouldn't have such an exhaustive type specification. At that point you'd be agreeing that relaxing type constraints does provide a benefit, and we'd just be arguing about our respective levels of comfort.
[1] https://github.com/davidfstr/idris-insertion-sort/blob/maste...
There are plenty of real world scenarios where static checking gets in the way even if you're not trying to encode complex properties using the type system.
One problem is that static typing is at odds with modularization since type declarations are considered globally. For example, Ring HTTP abstraction in Clojure represents requests and responses as maps. Middleware functions [1] can update these maps to inject additional keys, or modify existing keys. These functions often live in separate libraries that know nothing about one another. A static type system precludes this since it would require you to provide a static declaration for every possible request and response map.
[1] https://github.com/ring-clojure/ring/wiki/Middleware-Pattern...
If you statically prove that you check that they keys are there before using them, then the type system can be satisfied.
Module X expects the "foo" key, then write a function that checks if it has the foo key and returns a type Maybe(HasFoo). It's less good than just treating the type as the union of HasFoo and HasBar or whatever, but if you fully decouple, then you have to be able to handle the case in which the mapping lacks a foo key anyways, and this will statically froce you to.
Remember, in the sense we are currently talking about[1], objects are untyped, it's variables that are typed. So there is no need to describe the type of this map that is passing around in concrete terms; it's perfectly cromulent to treat the map as a TypeA in one place and a TypeB in another place, so long as you ensure that the prerequisites for those types are satisfied by the object.
It is true that it is usually preferable in statically typed languages to demonstrate that the map satisfies the requirements for TypeA before type erasure (i.e. at compile time), but if you want total decoupling, then that is not possible (since the requirement that the map have keys X and Y would need to be enforced outside of Module A). This does not mean that a type system cannot help you though.
I think we are getting to the limits of what can be easily communicated via HN comments, so if you still don't understand, then perhaps I'll write a blog article explaining it more fully.
For example, there is middleware for parsing our request params into a :params key. There's another piece of middleware that parses the values of these keys. So, you may or may not have a :params key, and the types inside the params can be absolutely anything. Then you could just have completely separate middleware that might add something like a CSRF token to the request map. And so forth. Your only real option here is to treat the entire structure as Any type.
If you still don't understand the problem, I really don't know how else to explain this.
On the other hand, we can easily measure the effects of factors like sleep [2], overwork [3], and happiness [4] on code quality. If static typing was an actual factor, we’d see exactly the same kinds of effects.
There’s nothing wrong with enjoying static typing, but there’s simply no evidence that it plays any role past personal preference. Different people solve problems in different ways, and have different pain points. It's entirely possible that each type discipline appeals to different mindsets. That is a value in itself.
[1] https://arxiv.org/abs/1901.10220
[2] https://arxiv.org/pdf/1805.02544.pdf
[3] http://web.archive.org/web/20090824001133/http://www.curt.or...
[4] http://neverworkintheory.org/2014/05/01/happy-sw-devs-solve-...
All I'm saying is that if you forgo static checks to avoid "paying the cost" -- and I do agree they come with a cost -- all you're doing is paying the cost elsewhere. Remember all those people saying "I don't need static types, I just write lots of tests"? That's a cost [1]. Or "I don't need types, I've never had type errors"? That's also a cost, though a more insidious one: ignoring that some of the errors they did get could have been prevented with a use of types they just aren't familiar with.
I'm not arguing that static typing/analysis leads to better quality. I'm arguing that people who don't want to pay its cost actually pay it elsewhere.
To be honest, if pressed I would also argue that I wouldn't want a critical system with the potential to endanger lives to be written in a dynamically typed language. Then again, static types alone wouldn't be suitable either.
----
[1] I knew one guy who didn't write tests either. "I don't need tests because they are a waste of my time: I never make mistakes". Guess where he paid the cost? :P Even then, not even writing tests is also an acceptable tradeoff in some situations!
If you have a specification for what the code is supposed to be doing, and you do specification testing then you will have a high level of confidence regardless of the type discipline. The kinds of errors that will slip through in a dynamic language would necessarily be edge cases and undefined behaviors. These are typically the kinds of bugs that static typing can help you catch.
On the other hand, dynamic typing facilitates features such as hot loading. Just last week my team had a production issue where the service we were using changed the API, and the team managing it didn't notify us. We were able to update the code that talks to the service via the REPL with zero downtime. This is something that would've been a much bigger issue if we had to take the whole system down.
I worked on a research project (a subproject of the project described in this NYT article about Peter Neumann: https://www.nytimes.com/2012/10/30/science/rethinking-the-co...) that experimented with addressing data security and integrity issues using strong types.
For example, writing data to the wrong channel, or reading from the wrong channel, was a type error.
Most of the time, most operations could be statically checked, but sometimes they could not. You might, for example, attempt to send a message to a recipient whose privileges change during transmission. Static checking won't help for such cases; the system needed dynamic checking.
The project used a novel programming language with both static and dynamic typechecking. It specified a hardware platform with tag support for dynamic types.
Mention either static or dynamic typing and a controversy erupts as night follows day between advocates of one and advocates of the other. Why not see the costs and benefits of both? I imagine that the practical answer is that supporting one type discipline costs less in development resources than supporting two, but that doesn't mean that the rejected discipline is therefore wrong and bad.
I liked that the project in question's designers didn't engage in a spurious struggle over static versus dynamic types. They understood that both were valuable, that each offered some benefits that the other didn't, and so they used both.
You need a mix.
Most dynamic types then go on to say why bother at all with static. That's where we disagree. It's dynamic types people that tend to be all or nothing. Where as static type people say use them where it's helps catch the obvious errors, so you don't have to write so many tests.
I also find that runtime contracts as seen in Racket and Clojure provide another interesting approach. From my experience contracts make it much easier to specify actual business constraints.
insert x [] = [x]
insert x (y:ys) = if x > y then y:(insert x ys) else x:y:ys
insertSort xs = foldr insert [] xs
Yes, Idris' proofs are verbose. They're also a perfect validation of the properties that need to be proven, better than any test case in the world.
Unfortunately, Haskell type system can result in baroque code in many cases as well. The whole reason monads are so prevalent in Haskell is due to the fact that the type system tracks side effects. Here's an example of a problem this introduces from the core.async library.
https://groups.google.com/forum/#!topic/clojure/wccacRJIXvg
When I first wrote the core.async go macro I based it on the state monad. It seemed like a good idea; keep everything purely functional. However, over time I've realized that this actually introduces a lot of incidental complexity. And let me explain that thought.
What are we concerned about when we use the state monad, we are shunning mutability. Where do the problems surface with mutability? Mostly around backtracking (getting old data or getting back to an old state), and concurrency.
In the go macro transformation, I never need old state, and the transformer isn't concurrent. So what's the point? Recently I did an experiment that ripped out the state monad and replaced it with mutable lists and lots of atoms. The end result was code that was about 1/3rd the size of the original code, and much more readable.
So more and more, I'm trying to see mutability through those eyes: I should reach for immutable data first, but if that makes the code less readable and harder to reason about, why am I using it?
While I believe those make for a more streamlined language (I do prefer F# to Ocaml), it also means that you regularly need type signature to desambiguate things where nothing was needed in Ocaml.