Our Statically Typed Future
or When Static Typing Wins
Static typing is the wonderful promise that automated, static verification of type correctness can make programs easier to write, easier to read, easier to maintain, and more correct. For those who have experienced the “if it compiles, it works” epiphany in Haskell, this feels like a promise fulfilled.
Still, all but its most dogmatic proponents admit that static typing is not all unicorns and rainbows. Yet someday it may be. Here is a vision of a possible future where static typing has unconditionally won and consigned dynamic languages to antiquity.
- Static type systems are now sufficiently advanced so that any useful program can be statically type checked. Further, any conceptually straight-forward program can be represented using similarly straight-forward types.
- Errors from type checkers are meaningful and clear.
- There is no longer any class of program that can be written more clearly or simply in a dynamic language than a statically typed one.
- Interdisciplinary programmers (statisticians, scientists, engineers, artists, musicians, hobbyists) consistently choose static languages for their unrivaled ease of use and productivity across all disciplines.
- Teams using statically typed languages have put teams using dynamically typed languages out of work by consistently delivering products of higher quality in less time.
- Every advance in software for the last several decades has come about from research relating to static type systems.
- What’s more, no interesting program in the last several decades has been written in a dynamic language.
- Any that were, though there weren’t any, were soon thereafter rewritten more elegantly and correctly using a statically typed language.
- It is now universally understood and agreed upon that time spent learning the intricacies of modern type systems is objectively better spent than time devoted to any other software-related endeavor.
- Monad tutorials are a solved problem.
- Programmers now choose languages (and make all decisions for that matter) using rational arguments based on empirically verified facts, or alternately, outcomes of relevant, well-designed, peer-reviewed, large-scale studies that accurately represent the complex and dynamic real-world circumstances of software development.
- Emacs has been rewritten in Idris. During the rewrite, several type errors are discovered, including the one responsible for Emacs pinkie and the one responsible for Eric S. Raymond.
- A Coq-assisted proof for the existence of God is discovered. Realizing that maybe he doesn’t know better than everyone about everything, Richard Dawkins issues a formal, heartfelt apology for everything he’s ever said outside the realm of evolutionary biology.