本章要點

? 為什么存在類型系統

? 強類型代碼的優點

? 類型系統的類型

? 類型系統的共性

火星氣候探測者號在火星大氣層解體，原因在于Lockheed開發的一個組件使用磅力秒（美國單位，可簡寫為lbfs）來測量動量，而NASA開發的另外一個組件則使用牛頓秒（動量的公制單位，可簡寫為Ns）來測量動量。如果為這兩種測量結果使用不同的類型，本可以避免這場災難。

在本書中，你將會看到，向類型檢查器提供了足夠的信息后，它們為消除各類錯誤提供了強大的方法。隨著軟件變得越來越復雜，我們越來越需要保證軟件能夠正確運行。通過監控和測試，能夠說明在給定特定輸入時，軟件在特定時刻的行為是符合規定的。但類型為我們提供了更加一般性的證明，說明無論給定什么輸入，代碼都將按照規定運行。

通過對編程語言的研究，人們正在設計出越來越強大的類型系統（例如，Elm或Idris語言的類型系統）。Haskell正變得越來越受歡迎。同時，在動態類型語言中添加編譯時類型檢查的工作也在推進中：Python添加了對類型提示的支持，而TypeScript這種語言純粹是為了在JavaScript中添加編譯時類型檢查而創建的。

顯然，為代碼添加類型是很有價值的，利用編程語言提供的類型系統的特性，可以編寫出更好、更安全的代碼。