There has also been a good amount of discussion generated by organizations such as Jane Street concerning the benefits of static typing and type inference in practice. Notably, the free documentation (that is completely coupled with the code) that you get when you design software that takes advantage of the type system.
Really, how would you scientifically show that parametric polymorphism is "useful?" "Useful" isn't a very empirical property, it isn't something you can reliably measure. In a scientific paper, you can't just say something like:
> When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck.
without justification! You have a citation, or perhaps it is something just accepted universally (which it isn't, of course). At the very least, you have to weaken the statement a bit...like:
> When it comes to maintaining and evolving these systems, the lack of explicit static typing is probably a bottleneck.
You can't talk in absolutes without evidence. But you know, the benefits of static typing are clear via anecdotal experience, we only really argue about whether or not the benefits balance out the disadvantages of static typing (and how those disadvantages can be mitigated, and if that is enough...). Again, in arguing about this we are firmly in the area of design and not science.
RE: Parametric polymorphism being "useful" - a pedant like me would claim for it to be of use, one has to demonstrate one clear instance of PP being of use - trivial or not - after which PP gains the attribute "useful" ;)
It doesn't speak to strong dynamic versus strong static at all.
Speaking of holes, of course dynamic typing can have holes also: if an interpreter or compiler misses a type check, the consequences are that the wrong operation is applied to an object. The result is corruption, crashing.
The correctness and completeness of a type scheme is orthogonal to static versus dynamic.
Of course, useful has a low bar, but it also has a magnitude (X is useful if it is used, it might not be very useful though).
Incidentally, stock markets have been big on Lisp and Smalltalk, two languages not known for static typing. It turns out that language X is always used in the stock market, where X is the latest hot language (Scala, Haskell, Clojure...).
You can apply the same intuition and things mostly work, but there can be a few surprises.
These theorems are a huge part of the "if it compiles it must be correct" feeling that functional programming often provides.