1 Introduction to Typing

The Mars Climate Orbiter disintegrated into the planet's atmosphere because a component developed by Lockheed produced momentum measurements in pound-force seconds (US units) while another component developed by NASA expected momentum to be measured in Newton seconds (metric units). Using different types for the two measures would’ve 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 this point in time, given this particular 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 or 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 while TypeScript is a language created for the sole purpose of providing compile-time type checking to JavaScript.

1.1 Who This Book Is For

1.2 Why Types Exist

1.2.1 0s and 1s

1.2.2 What are Types and Type Systems?

1.3 Benefits of Type Systems

1.3.1 Correctness

1.3.2 Immutability

1.3.3 Encapsulation

1.3.4 Composability

1.3.5 Readability

1.4 Types of Type Systems

1.4.1 Dynamic and Static Typing

1.4.2 Weak and Strong Typing

1.4.3 Type Inference

1.5 In This Book

1.6 Summary