1.1.2　類型和類型系統的定義

本書討論的是類型和類型系統，下面就先來定義這兩個術語。

類型：類型是對數據做的一種分類，定義了能夠對數據執行的操作、數據的意義，以及允許數據接受的值的集合。編譯器和運行時會檢查類型，以確保數據的完整性，實施訪問限制，以及按照開發人員的意圖來解釋數據。

有時候，我們會簡化討論，忽略操作部分，而只將類型簡單地視為集合，代表該類型的實例能夠接受的所有可能的值。

類型系統：類型系統是一組規則，為編程語言的元素分配和實施類型。這些元素可以是變量、函數和其他高級結構。類型系統通過兩種方式分配類型：程序員在代碼中指定類型，或者類型系統根據上下文，隱式推斷出某個元素的類型。類型系統允許在類型之間進行某些轉換，而阻止其他類型的轉換。

定義了類型和類型系統之后，我們接下來看看類型系統的規則是如何實施的。圖1.3從更高層面展示了源代碼的執行過程。

圖1.3　編譯器或解釋器將源代碼轉換成可被運行時執行的代碼。運行時是一個真實的計算機或者一個虛擬機，例如，Java的JVM或瀏覽器的JavaScript引擎

在高層面上，編譯器或解釋器將把我們編寫的源代碼轉換成機器（或運行時）能夠理解的指令。當運行時是一臺物理計算機時，轉換的指令將是CPU指令；當運行時是虛擬機時，則有自己的指令集和工具。

類型檢查：類型檢查確保程序遵守類型系統的規則。編譯器在轉換代碼時進行類型檢查，而運行時在執行代碼時進行類型檢查。編譯器中負責實施類型規則的組件叫作類型檢查器。

如果類型檢查失敗，則意味著程序沒有遵守類型系統的規則，此時程序將會編譯失敗，或者發生運行時錯誤。1.3節將詳細說明編譯時類型檢查與執行時（或運行時）類型檢查的區別。

類型檢查和證明

類型系統得到大量形式理論的支持。例如，柯里–霍華德（Curry-Howard）對應，也叫作“證明即程序”，就展示了邏輯與類型理論之間的密切關系。該對應說明，我們可以將類型視為一個邏輯命題，將從一個類型得到另一個類型的函數視為邏輯蘊含。類型的一個值相當于證明命題為真的一個證據。

下面我們以一個接受boolean作為參數并返回一個string的函數為例加以說明。

Boolean到string

這個函數也可以解釋為“boolean蘊含string”。給定命題boolean的證據，這個函數（蘊含）能夠得到命題string的證據。boolean的證據是該類型的一個值：true或false。有了這個證據后，該函數（蘊含）將得到string的證據：要么是字符串"true"，要么是字符串"false"。

邏輯與類型理論之間的密切關系說明，遵守類型系統規則的程序相當于一個邏輯證明。換句話說，類型系統是一種語言，我們用它來寫出這些證明?？吕铷C霍華德對應很重要，因為它為“程序將正確運行”這種保證帶來了邏輯上的嚴謹性。