I like types, but jeez, the vast majority of web systems over the last decade were written in dynamic languages. You're trying to claim absolute proof for a very subjective choice, and it sounds silly.
They've done some Web things.
C++ has very good support for dynamic typing. You can make C++ look almost like Javascript, if you want.
If you have a lot of dynamic typing, you may want to look at C instead.
x can be of a smart pointer type (let's call it "var") which acts as reference to an anyobject class instance, which comes in varieties like string_anyobject, integer_anyobject and so on.
The smart pointer class can have a few assignment operators and conversion constructors for usage like var x = "lit"; or x = 5.
That's because the vast majority of web systems are glorified CRUD apps, the easiest kind of application one can make.
When it comes to the real hard backend parts (not just some queue handling of video conversion tasks for example, but things like search engines, social graph stores, programs for finding the cheapest air tickets, etc.), they're usually done in languages like Java, Scala, C++, Go, etc.
Heck, even as web front-ends got more evolved, people developed several typing systems to assist us (Flow, Typescript, etc) to solve that need, we got Go, Hack. Optional types are also landing in PHP and even in Python -- there's a consensus among many people about a need for such things. And Google wrote their more complex apps in a Java lib that could spat out Javascript IIRC (GWT).
As for the non CRUD apps, from PostgeSQL, Chrome, Office and Photoshop to Pixelmator, OmniPlan, Notepad++ and Scrivener, nobody writes those in dynamic languages (where nobody obviously means: some outliers being excepted). One might argue that those are few (they are not, they are merely "fewer" than web systems. Still millions of programmers work in that space), but the point remains: for developing harder apps, people opt to static languages.
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.