Chapter 1. Introduction to typing
This chapter covers
The Mars Climate Orbiter disintegrated in the planet’s atmosphere because a component developed by Lockheed produced momentum measurements in pound-force seconds (U.S. units), whereas another component developed by NASA expected momentum to be measured in Newton seconds (metric units). Using different types for the two measures would have prevented the catastrophe.
As we will see throughout this book, type checkers provide powerful ways to eliminate whole classes of errors, provided they are given enough information. As software complexity increases, so does the need to provide better correctness guarantees. Monitoring and testing can show that the software is behaving according to spec at a given point in time, given specific input. Types give us more general proofs that the code will behave according to spec regardless of input.
Programming language research is coming up with ever-more-powerful type systems. (See, for example, languages like Elm and Idris.) Haskell is gaining in popularity. At the same time, there are ongoing efforts to bring compile-time type checking to dynamically typed languages: Python added support for type hints, and TypeScript is a language created for the sole purpose of providing compile-time type checking to JavaScript.