Programming Languages: Application and Interpretation【譯15上】

02-19

初翻： @lotuc

原文：PLAI 第二版

GitHub：PLAI-cn

GitBook：PLAI-cn

翻譯聲明見 Github 倉庫

15 靜態地檢查程序中的不變數：類型

當程序變得更大或者更為複雜時，程序員希望能有工具幫助他們描述、驗證程序中的不變數。顧名思義，不變數指的就是關於程序組成元素的那些不會發生改變的陳述。例如，當我們在靜態類型語言中寫下x : number時，表示 x 中存放的總是數，程序中依賴 x 的部分都可以認定它是數的這個事實不會改變。我們將會看到，類型只是我們想要陳述的各類不變數中的一種，靜態類型檢測——一個分支眾多的技術家族——也只是用於控制不變數的眾多方法中的一個。

15.1 靜態類型規則

本章我們將專註於靜態類型檢查：即在程序執行前檢查（聲明的）類型。之前使用的靜態類型語言已經讓我們積攢了一些這種形式程序的經驗。我們將探索類型的設計空間及這些設計中的權衡取捨。儘管類型是控制不變數的一種非常強大且有效的方法，最後我們還是會考察一些其它可用的技術。

考慮下面這段靜態語言寫就的程序：

(define (f [n : number]) : number (+ n 3))(f "x")

程序開始執行前我們就會得到一個靜態類型錯誤。使用普通 Racket 寫就的同樣的程序（去除類型註解）只會在運行時出錯：

(define (f n) (+ n 3))(f "x")

練習題

如何判斷錯誤是在程序執行前還是運行時拋出的？

考慮下面這段 Racket 程序：

(define f n (+ n 3))

它也是在程序執行前就遇到錯誤——語法解析錯誤——終止。儘管我們認為語法解析和類型檢查有所不同——通常是因為類型檢測是針對已經被解析好的程序做的——但是將語法解析看作一種最簡單形式的類型檢查也很有用：它（靜態地）判定程序是否遵守某個上下文無關語法。隨後，類型檢查判定它是否遵守某個上下文相關（或者一個更豐富的）語法。簡而言之，類型檢查從某種程度上看是語法解析的泛化，它們都是通過語法控制程序遵循指定的規則。

15.2 關於類型的經典看法

我們先介紹傳統的包含類型的核心語言；然後我們將探索其擴展和變種。

15.2.1 簡單的類型檢查器

要定義類型檢查器，我們先需要就兩件事達成一致：我們靜態類型核心語言的語法，對應的類型的語法。

先回到我們之前實現過的函數作為值的那一版語言，其中並不包含賦值等其它稍複雜的東西（後面將講到添加其中的一些）。我們需要為該語言添加類型註解。按慣例，我們不對常量或基本操作（如加法）強加類型注釋；相反，我們把類型注釋加在函數或方法的邊界上。在本章討論的過程中，我們將探討為什麼這麼做。

鑒於此決定，我們靜態類型的核心語言變成了：

(define-type TyExprC [numC (n : number)] [idC (s : symbol)] [appC (fun : TyExprC) (arg : TyExprC)] [plusC (l : TyExprC) (r : TyExprC)] [multC (l : TyExprC) (r : TyExprC)] [lamC (arg : symbol) (argT : Type) (retT : Type) (body : TyExprC)])

每個函數都添加了其參數及返回值類型的註解。

現在我們需要對類型語言作出選擇。我們遵從傳統定義，即類型是一組值的集合的抽象。我們的語言中有兩類值：

(define-type Value [numV (n : number)] [closV (arg : symbol) (body : TyExprC) (env : Env)])

因此我們有兩種類型：數和函數。

即使數類型也並不那麼簡單直接：數類型應該記錄何種信息？大部分語言中，實際上有很多數類型，甚至沒有哪個類型表示「數」。然而，我們忽略了數的層級結構（譯註，第三章），對於我們來說有一種數的類型足矣。這樣決定之後，我們是否需要記錄哪種數的信息？原則上可以，但這樣我們很快就會遇到可判定性問題。

至於函數，我們有更多信息：參數的類型，返回值的類型。我們不妨記錄下這些信息，除非事後證實這些信息沒有用處。結合這些，我們得出這樣的類型的抽象語言：

(define-type Type [numT] [funT (arg : Type) (ret : Type)])

既然已經確定了語言中項和類型的結構，接下來我們來確定語言中哪些算是類型錯誤（並且，如果程序中不包含這裡列出的類型錯誤，它就會通過類型檢查）。顯然有三種形式的類型錯誤：

+的參數不是數，即不是numT。
*的參數不是數。
函數調用時函數位置的表達式不是函數，即不是funT。

思考題

還有其它形式的類型錯誤嗎？

事實上我們遺漏了一個：

函數調用時實參的類型和函數形參的類型不一致。

我們的語言中的所有其他程序似乎都應該通過類型檢查。

關於類型檢查器的簽名，初步設想，它可以接受表達式作為參數，返回布爾值指明該表達式是否通過檢查。由於我們知道表達式中包含標識符，所以很顯然我們還需要一個類型環境，它將名字映射到類型，類似於我們之前用到的值環境。

練習題

定義與類型環境相關的數據類型以及函數。

於是，我們開始寫下的程序結構大致是這樣：

<tc-take-1> ::= ;;類型檢查，第一次嘗試 (define (tc [expr : TyExprC] [tenv : TyEnv]) : boolean (type-case TyExprC expr <tc-take-1-numC-case> <tc-take-1-idC-case> <tc-take-1-appC-case>))

正如上面程序中列出的要處理幾種情形所表明的，這種方法行不通。我們很快將知道這是為什麼。

首先處理簡單的情形：數。單獨的一個數能通過類型檢查嗎？顯然可以；它所處的上下文可能想要的不是數類型，但是這種錯誤應該在其它地方被檢查出。因此：

<tc-take-1-numC-case> ::= [numC (n) true]

下面處理標識符。如何判斷標識符是否通過類型檢查呢？同樣，就其自身來說，如果是綁定標識符，總是通過檢查的；它可能不是上下文要求的那種類型，但是這種錯誤應該在其它地方檢查。因此，我們得出：

<tc-take-1-idC-case> ::= [idC (n) (if (lookup n tenv) true (error tc "not a bound identifier"))] ;不是綁定標識符

上面的代碼你可能感覺不太對：如果標識符未綁定的話，lookup會拋出異常，因此沒必要再去重複處理該情況（事實上，代碼永遠不會執行到error調用那個分支）。但是讓我們先繼續。

下面來處理函數調用。我們應該首先檢查函數位置，確定它是個函數，然後確保實際參數的類型和該函數定義時聲明的形式參數類型相同。例如，函數可能需要參數是數，但調用給的是個函數，或者反之，在這兩種情況下，我們都需要防止錯誤的函數調用。

代碼該怎麼寫？

<tc-take-1-appC-case> ::= [appC (f a) (let ([ft (tc f tenv)]) ...)]

對於tc的遞歸調用只能讓我們知道函數位置是否通過類型檢查。如果它通過了，怎麼知道它具體是什麼類型的呢？如果是個簡單的函數定義的話，我們可以直接從語法上取得其參數和返回值的類型。但是如果是個複雜的表達式，我們就需要一個函數能計算出表達式類型。當然，只有這個表達式是個類型正確的表達式時，該函數才能返回類型結果；否則的話它將不能得出正確的結果。換句話說，「類型檢查」是「類型計算」的一種特殊情形！因此，我們應該增強tc的歸納不變數：即，不僅僅返回表達式是否能通過類型檢查，而是返回表達式的類型。事實上，只要有返回值，就說明該表達式通過了類型檢查；否則它會拋出錯誤。

下面我們來定義這個更完善的類型「檢查器」。

<tc> ::= (define (tc [expr : TyExprC] [tenv : TyEnv]) : Type (type-case TyExprC expr <tc-numC-case> <tc-idC-case> <tc-plusC-case> <tc-multC-case> <tc-appC-case> <tc-lamC-case>))

現在填充具體實現。數很簡單：它的類型就是數類型。

<tc-numC-case> ::= [numC (n) (numT)]

與之相似，標識符的類型從環境中查詢得到（如果其未被綁定則會拋出錯誤）。

<tc-idC-case> ::= [idC (n) (lookup n tenv)]

到此，我們可以觀察到該類型檢查器與解釋器之間的一些異同：對於標識符，兩者做的事情其實一樣（只不過這裡返回的是標識符的類型而不是一個實際的值），對於數的情況，這裡返回了抽象的「數」而不是具體的數。

下面考慮加法。必須確保其兩個子表達式都具有數類型；如果滿足該條件，則加法表達式本身返回的是數類型。

<tc-plusC-case> ::= [plusC (l r) (let ([lt (tc l tenv)] [rt (tc r tenv)]) (if (and (equal? lt (numT)) (equal? rt (numT))) (numT) (error tc "+ not both numbers")))] ;+不都是數

通常在處理完加法的情形之後，對於乘法我們就一筆帶過了，但是這裡顯式處理一下它還是很有教益的：

<tc-multC-case> ::= [multC (l r) (let ([lt (tc l tenv)] [rt (tc r tenv)]) (if (and (equal? lt (numT)) (equal? rt (numT))) (numT) (error tc "* not both numbers")))] ;*不都是數

思考題

看出其中的區別了嗎？

是的，基本上完全沒區別！（僅有的區別是在type-case時使用的分別multC和plusC，以及錯誤提示信息稍有不同）。這是因為，從（此靜態類型語言）類型檢查的角度來說，加法和乘法沒有區別，更甚，任意接受兩個數作為參數返回一個數的函數都沒有區別。

注意到代碼解釋和類型檢查之間另一個不同點。它們的參數都得是數。解釋器返回加或者乘它們得到的確切數值，但是類型檢查器並不在乎具體的數值：因此該表達式的計算結果（(numT)）是個常數，兩種情形返回都是該常數。

最後還剩下兩個難一點的情形：函數調用和函數。我們已經討論過怎麼處理函數調用：計算函數以及參數表達式的值；確保函數表達式為函數類型；檢查參數類型和函數形參類型相容。如果這些條件滿足，函數調用得到的結果類型就是函數體的類型（因為運行時最終的返回值就是計算函數體得到的值）。

<tc-appC-case> ::= [appC (f a) (let ([ft (tc f tenv)] [at (tc a tenv)]) (cond [(not (funT? ft)) (error tc "not a function")] ;不是函數 [(not (equal? (funT-arg ft) at)) (error tc "app arg mismatch")] ;app參數不匹配 [else (funT-ret ft)]))]

最後還剩下函數定義。函數有一個形參，函數體中一般會用到；除非它被綁定到環境中，不然函數體應該不太可能通過類型檢查。因此我們需要擴展類型環境，添加形參與其類型的綁定，然後在擴展後的環境中檢查函數體。最終計算得到的函數體類型必須和函數定義中指定的函數返回值類型相同。如果滿足了這些，該函數的類型就是指定參數類型到函數體類型的函數。

練習題

上面說的「不太可能通過類型檢查」是什麼意思？

<tc-lamC-case> ::= [lamC (a argT retT b) (if (equal? (tc b (extend-ty-env (bind a argT) tenv)) retT) (funT argT retT) (error tc "lam type mismatch"))] ;λ類型不匹配

注意到解釋器與類型檢查器另一個有趣的不同點。解釋器中，函數調用負責計算參數表達式的值，擴展環境，然後對函數體求值。而這裡，函數調用的情形中的確也檢查了參數表達式，但是沒有涉及到環境的處理，直接返回了函數體的類型，而沒有遍歷它。對函數體的遍歷檢查過程實際是在檢查函數定義的過程中進行的，因此環境也是在這個地方才實際被擴展的。

15.2.2 條件語句的類型檢查

考慮為上面的語言添加條件語句，即使最簡單的 if 表達式都會引入若干設計抉擇。這裡我們先討論其中的兩個，後面會回過頭討論其中的一個。

條件表達式的類型應該是什麼？某些語言中它必須計算得到布爾值，這種情況下需要為我們的語言添加布爾值類型（這可能是個好主意）。其它語言中，它可以是任意值，某些值被認為是「真值」，其它的則被視為「假值」。
then-和else-兩個分支之間的關係應該是什麼呢？一些語言中它們的類型必須相同，因此整個 if 表達式有一個確定無歧義的類型。其它語言中，兩個分支可以有不同的類型，這極大地改變了靜態類型語言的設計和它的類型檢查器，而且也改變了編程語言本身的性質。

練習題

為該靜態類型語言添加布爾值。至少需要添加些啥？在典型的語言中還需要加什麼？

練習題

為條件語句添加類型規則，其中條件表達式應該計算得到布爾值，且then-和else-分支必須有相同的類型，同時該類型也是整個條件語句的類型。

15.2.3 代碼中的遞歸

現在我們已經得到了基本的編程語言，下面為其添加遞歸。之前我們實現過遞歸，可以很容易的通過去語法糖實現。這裡的情況要更複雜一些。

15.2.3.1 遞歸的類型，初次嘗試

首先嘗試表示一個簡單的遞歸函數。最簡單的當然就是無限循環。我們可以僅使用函數實現無限循環嗎？可以：

((lambda (x) (x x)) (lambda (x) (x x)))

因為我們的語言中已經支持將函數作為值。

練習題

為什麼這會構成無限循環？它是如何巧妙地依賴於函數調用的本質的？

現在我們的靜態類型語言要求我們為所有函數添加類型註解。我們來為該函數添加類型註解。簡單起見，假設從現在開始我們寫的程序使用的語法是靜態類型的表層語法，去語法糖將幫我們將其轉換為核心語言。

首先注意到，我們有兩個完全一樣的表達式，它們互相調用。歷史原因，整個表達式被稱為Ω（希臘字母大寫歐米茄），那兩個一樣的子表達式被稱為ω（希臘字母小寫歐米茄）。兩個一樣的表達式並非得是同種類型的，因為這還依賴於具體使用環境中對於不變數的定義。這個例子中，觀察到 x 被綁定到ω，於是ω將出現在在(x x)式子的第一個和第二個部分。即，確定其中一個表達式的類型，另一個式子的類型也被確定。

那麼我們就來嘗試計算ω的類型；稱該類型為γ。顯然它是一個函數類型，而且是單參數的函數，所以它的類型必然是φ -> ψ這種形式的。該函數的參數是什麼類型？就是ω的類型。也即，傳入φ的值的類型就是γ。因此，ω的類型是γ，也即φ -> ψ，展開即(φ -> ψ) -> ψ，進一步展開得((φ -> ψ) -> ψ) -> ψ，還可以繼續下去。也就是說，該類型不能用有限的字元串寫出來！

思考題

你注意到了我們剛做的的微妙但重要的跳躍嗎？

15.2.3.2 程序終止

我們觀察到，試圖直接地計算Ω的類型，需要先計算γ的類型，這似乎導致了嚴重的問題。然後我們就得出結論：此類型不能用有限長度的字元串表示，但是這只是直覺的結果，並非證明。更奇怪的事實是：在我們迄今定義的類型系統中，根本無法給出Ω的類型！

這是一個很強的表述，但事實上我們可以給出更強的描述。我們目前所用的靜態類型語言有一個屬性，稱為強歸一化（strong normalization）：任何有類型的表達式都會在有限步驟後終止計算。換句話，這個特殊的（奇特的）無限循環程序並不是唯一不可獲得類型的程序；任何無限循環（或潛在存在無限循環）程序都無法求得類型。一個簡單的直覺說明可以幫助我們理解，任何類型——必須能被有限長度的字元串表示——只能包含有限個->，每次調用會去除一個->，因此我們只能進行有限次數的函數調用。

如果我們的程序只允許非轉移程序（straight-line program），這點也無足為奇。但是，我們有條件語句，還有可以當做值任意傳遞的函數，通過這些我們可以編碼得到任何我們想要的數據結構。然而我們仍能得到這個保證！這使得這個結果令人吃驚。

練習題

試著使用函數分別在動態類型和靜態類型語言中編碼實現列表。你看到了什麼？這說明此類型系統對於編碼產生了何種影響？

這個結果展示了某種更深層次的東西。它表明，和你可能相信的——類型系統只是用來避免一些程序 BUG 在運行時才被發現——相反，類型系統可能改變語言的語義。之前我們一兩行就能寫出無限循環，現在我們怎麼都寫不出來。這也表明，類型系統不僅可以建立關於某個特定程序的不變數，還能建立關於語言本身的不變數。如果我們非常需要確保某個程序將會終止，只要用該語言來寫然後交由類型檢查器檢查通過即可。

一門語言，用其書寫的所有程序都將終止，有什麼用處？對於通用編程來說，當然沒用。但是在很多特殊領域，這是非常有用的保證。例如，你要實現一個複雜的調度演算法；你希望知道調度程序保證會終止，以便那些被調度的任務被執行。還有許多其他領域，我們將從這樣的保證中受益：路由器中的數據包過濾器；實時事件處理器；設備初始化程序；配置文件；單線程

JavaScript 中的回調；甚至編譯器或鏈接器。每種情況下，我們都有一個不成文的期望，即這些程序最終會終止。而現在我們有一個語言能保證這點——且這點是不可測試的。

這不是假想的例子。在Standard ML語言中，鏈接模塊基本上就是使用這種靜態類型語言來編寫模塊鏈接規範。這意味著開發人員可以編寫相當複雜的抽象概念——畢竟可以將函數作為值使用——且同時鏈接過程被保證會終止，產生最終的程序。

15.2.3.3 靜態類型的遞歸

這就意味著，之前我們可以只通過去語法糖來實現rec，現在則必須在我們的靜態類型語言中顯式的實現。簡單起見，我們僅考慮rec的一種特殊形式——它涵蓋了常見用法，即遞歸標識符被綁定到函數。因此，表層語法中，我們可能寫出如下的累加函數：

(rec (Σ num (n num) (if0 n 0 (n + (Σ (n + -1))))) ;譯註，原文如此，+應前置 (Σ 10))

其中，Σ是函數名，n為其參數，num為函數參數以及返回值的類型。表達式(Σ 10)表示使用該函數計算從 10 累加到 0 的和。

如何計算這個表達式的類型？顯然，求類型過程中，n在函數體中的類型需要綁定（但是在函數調用處就不需要了）；這一點計算函數類型的時候我們就知道了。那麼Σ呢？顯然，在檢查(Σ 10)的類型時，它應該在類型環境中被綁定，類型必須為num -> num。不過，在檢查函數體時，它同樣需要被綁定到此類型。（還要注意，函數體返回值的類型需要和事先聲明的返回類型相同。）

現在我們可以看到如何打破類型有限性的束縛。程序代碼中，我們只能編寫包含有限數量->的類型。但是，這種遞歸類型的規則在函數體中引用自身時複製了->，從而供應了無窮的函數調用。這是包含無窮箭矢的箭筒。

實現這種規則的代碼如下。假設f被綁定到函數的名字，aT是函數參數的類型，rT為返回類型，b是函數體，u是函數的使用：

<tc-lamC-case> ::= [recC (f a aT rT b u) (let ([extended-env (extend-ty-env (bind f (funT aT rT)) tenv)]) (cond [(not (equal? rT (tc b (extend-ty-env (bind a aT) extended-env)))) (error tc "body return type not correct")] ;函數體類型錯誤 [else (tc u extended-env)]))]

15.2.4 數據中的遞歸

我們已經見識了靜態類型的遞歸程序，但是它還不能使我們創建遞歸的數據。我們已經有一種遞歸數據——函數類型——但是這是內建的。現在還沒看到如何創建自定義的遞歸數據類型。

15.2.4.1 遞歸數據類型定義

當我們說允許程序員創建遞歸數據時，我們實際在同時談論三種東西：

創建新的類型
讓新類型的實例擁有一個或多個欄位
讓這些欄位中的某些指向同類型的實例

實際上，一旦我們允許了第三點，我們就必須再允許一點：

允許該類型中非遞歸的基本情況的存在

這些設計準則的組合產生了通常被稱為代數數據類型（algebraic datatype）的東西，比如我們的靜態語言中支持的類型。舉個例子，考慮下面這個數二叉樹的定義：【注釋】

(define-type BTnum [BTmt] [BTnd (n : number) (l : BTnum) (r : BTnum)])

後面我們會討論如何參數化類型。

請注意，如果這個新的數據類型沒有名字，BTnum，我們將不能在BTnd中引用回該類型。同樣地，如果只允許定義一種BTnum構造，那麼就無法定義 BTmt，這會導致遞歸無法終止。當然，最後我們需要多個欄位（如BTnd中的一樣）來構造有用、有趣的數據。換句話說，所有這三種機制被打包在一起，因為它們結合在一起才最有用。（但是，有些語言確實允許定義獨立結構體。後文我們將回來討論這個設計決策對類型系統的影響）。

我們關於遞歸表示的初步討論暫告一個段落，但這裡有個嚴重的問題。我們並沒有真正解釋這個新的數據類型BTum的來源。因為我們不得不假裝它已經在我們的類型檢查器中實現了。然而，為每個新的遞歸類型改變我們的類型檢查器有點不切實際——這就好比需要為每個新出現的遞歸函數去修改解釋器！相反，我們需要找到一種方法，使得這種定義成為靜態類型語言的固有能力。後面我們會回來討論這個問題。

這種風格的數據定義有時也被稱為乘積的和，「乘」指代欄位組合成不變數的方式：例如，BTnd的合法值是傳遞給BTnd構造器的每個欄位合法值的叉乘。「和」是所有這些不變數的總數：任何給定的BTnum值是其中之一。（將「乘」想作「且」，「加」想作「或」。）

15.2.4.2 自定義類型

想一想，數據結構的定義會產生哪些影響？首先，它引入了新的類型；其次它基於此類型定義若干構造器、謂詞和選擇器。例如，在上面的例子中，首先引入 BTnum，然後使用它創建以下類型：

BTmt : -> BTnumBTnd : number * BTnum * BTnum -> BTnumBTmt? : BTnum -> booleanBTnd? : BTnum -> booleanBTnd-n : BTnum -> numberBTnd-l : BTnum -> BTnumBTnd-r : BTnum -> BTnum

觀察幾個顯著的事實：

這裡的構造器創建BTnum的實例，而不是更具體的東西。稍後我們將討論這個設計抉擇。
這裡的謂詞函數都接受BTnum類型參數，而不是「Any」（任意值）。這是因為類型系統已經可以告訴我們某個值的類型是什麼，因此我們只需要區分該類型的不同形式。
選擇器只能作用於類型中相關形式的實例——例如，BTnd-n只對BTnd的實例有效，對BTmt的實例則不行——但是由於缺乏合適的靜態類型，我們無法在靜態類型系統中表示這點。

遞歸類型中還有很多值得討論的東西，我們不久將回到這個話題。

15.2.4.3 模式匹配和去語法糖

類型定義的討論告一段落，剩下要提供的功能就是模式匹配。例如，我們可以這樣寫：

(type-case BTnum t [BTnum () e1] [BTnd (nv lt rt) e2])

我們知道，這可以用前述的函數來實現。用 let 就可以模擬此模式匹配所實現的綁定：

(cond [(BTmt? t) e1] [(BTnd? t) (let ([nv (BTnd-n t)] [lt (BTnd-l t)] [rt (BTnd-r t)] e2)])

總之，它可以通過宏實現，所以模式匹配不需要被添加到核心語言中，直接用去語法糖即可實現。這也意味著一門語言可以有很多不同的模式匹配機制。

不過，這不完全正確。生成上面代碼中的cond表達式時，宏需要通過某種手段知道BTnd的三個位置選擇器分別是BTnd-n、BTnd-l和BTnd-r。這些信息在類型定義時顯式給出，但是在模式匹配時是隱含的（劃重點）。因此，這些信息必須要從類型定義處傳過來。因此宏擴展器需要使用類似類型環境的東西完成其任務。

此外，還要注意，例如e1和e2這樣的表達式無法類型檢查——事實上，甚至不能被可靠地識別為表達式——直到宏擴展器完成了type-case的擴展之後。因此，擴展依賴於類型環境，而類型檢查依賴於擴展的結果。換句話說這兩者是共生關係，不僅僅是並行運行，而是同步運行。因此，靜態類型語言中進行去語法糖操作時，如果語法糖需要對相關類型作出推測，要比動態類型語言中更複雜一些。

15.2.5 類型、時間和空間

明顯，類型已經賦予了類型安全語言一些性能優勢。因為一些本來需要運行時執行的檢查（例如，檢查加法的兩個參數的確是數）現在是靜態執行的。在靜態類型語言中，類似:number的註解已經回答了關於某個值是否是特定類型這種問題；無需在運行時再去檢查。因此，類型級別的謂詞以及程序中對它們的使用將會（並且需要）完全消失。

對於開發者來說這需要付出一些代價，他們必須說服靜態類型系統他們的程序不會導致類型錯誤；由於可判定性的限制，有些可以正確運行的程序也可能與類型系統衝突。不過，類型系統為滿足了它要求的程序提供了可觀的運行時性能優勢。

接下來我們來討論空間。到目前為止，語言的運行時系統需要對每個值附加存儲其類型信息。這也是其實現類型級別謂詞如 number? 的基礎，這些謂詞既可被開發人員使用也可被語言內部使用。如果不需要這些謂詞，那麼這些為了實現它們而存儲的信息所佔據的空間也將不再需要。因此（靜態語言）不需要類型標籤。

然而，垃圾回收器仍然需要它們，但其他表示法（如BIBOP(譯註BIg Bag Of Pages)）能極大減少它們對空間的需求。

類型變體相關的謂詞仍要保留：如上面例子中的BTmt?和BTnd?。它們的調用需要在運行時求值。例如，如前所述，選擇器BTnd-n就需要執行這種檢查。當然，進一步的優化是可能的。考慮模式匹配去語法糖後生成的代碼：其中的三個選擇器就無需執行這些檢查，因為只有BTnd?返回真值時才會執行對應代碼片。因此，運行時系統可以給去語法糖層面提供特殊的不安全（unsafe）指令，也就是不執行類型檢查的版本，從而生成如下所示的代碼：

(cond [(BTmt? t) e1] [(BTnd? t) (let ([nv (BTnd-n/no-check t)] [lt (BTnd-l/no-check t)] [rt (BTnd-r/no-check t)]) e2)])

但最終的結果是，運行時系統仍然需要存儲足夠的信息來準確回答這些問題。不過，相比於之前需要使用足夠的位來區分每種類型及類型變體，現在，由於類型被靜態地隔離了，對於沒有變體的類型（例如，只有一種類型的字元串），不再需要存儲任何變體相關的信息；這意味著運行時系統可以使用所有可用位來存儲實際的動態值。

與之相對，如果類型存在變體，運行時系統需要犧牲一些空間用於區分不同變體，不過一個類型中變體的數量顯然比所有類型和其變體的數量要小得多。在上面的例子中，BTnum只有兩個變體，因此運行時系統只需要使用一個比特來記錄某個值是BTnum的哪個變體。

特別要注意的是，類型體系的隔離可以防止混淆。如果有兩種不同的數據類型，每種都有兩種變體，在動態類型的世界中，所有這四種變體都需要有不同的表示法；與之相對，在靜態類型的世界中，這些表示法可以跨類型重疊，因為靜態類型系統會保證一種類型中的變體和另一種類型中的不被混淆。因此，類型系統對於程序的空間（節約表示所需空間）和時間（消除運行時檢查）上都有實打實的性能提升。

15.2.6 類型和賦值

我們已經覆蓋了核心語言中除賦值之外的大部分基本特性。從某些方面看，類型和賦值之間的相互作用很簡單，這是因為在經典環境中，它們根本不相互作用。例如，考慮下面動態類型程序：

(let ([x 10]) (begin (set! x 5) (set! x "某物")))

x的「類型」是什麼？它並沒有確定的類型，它在一段時間內是數，後來（注意裡面蘊含時間意味）是字元串。我們根本無法給它定類型。一般來說，類型檢查是種非時間性的活動：它只在程序運行之前執行一次，因此必須獨立於程序執行的特定順序。因此，跟蹤貯存中的精確值超出了類型檢查程序的能力範圍。

上面的例子當然可以簡單的靜態的被理解，不過我們不能被簡單的例子誤導。考慮下面的程序：

(let ([x 10]) (if (even? (read-number "輸入數字")) (set! x 5) (set! x "某物")))

現在，靜態檢查不可能得到關於x的類型的結論，因為只有在運行時我們才能獲得用戶輸入的值。

為了避免這種情況，傳統的類型檢查器採用了一個簡單策略：賦值過程中類型必須保持不變。也就是說，賦值操作，不論是變數賦值還是結構體賦值，都不能改變被賦值的量的類型。因此，上面的代碼在我們當前的語言中將不能通過類型檢查。給程序員提供多少靈活性就取決與語言了。例如，如果我們引入更加靈活的類型表示「數或字元串」，上面的例子將能通過類型檢查，但是x的類型就永遠不那麼精確，所有使用x的地方都需要處理這種降低了的精度，後面我們會回到這個問題。

簡而言之，在傳統的類型系統中賦值相對容易處理，因為它採用了簡單的規則，值可以在類型系統指定的限度下進行改變，但是類型不能被改變。在像set!這種操作的情況下（或者我們的核心語言中的setC），這意味著賦值的類型必須和變數的類型匹配。在結構體賦值的情況下，例如box，這意味著賦值的類型必須和box容器內容的類型匹配。

15.2.7 中心定理：類型的可靠性

之前我們說過，一些靜態類型語言可以為其書寫的程序所能達成某些特性作出很堅實的證明：例如，該語言書寫的程序肯定會終止。當然，一般來說，我們無法獲得這樣的保證（事實上，正是為了能寫出無限循環我們才添加的通用遞歸）。然而，一個有意義的類型系統——事實上，任何值得類型系統這一高貴頭銜的東西【注釋】——應該為所有靜態類型程序提供某種有意義的保證。這是給程序員的回報：通過給程序加上類型，她可以確保某些不好的事情不會發生。沒有類型的話，我們也能找到bug；這是有用的，但它不足以提供構建高級別工具（例如要保證安全性、隱私性或健壯性）的必要基礎。

我們一再使用「類型系統」這個術語。類型系統通常是三個組件的組合：類型的語言、類型規則，以及將這些規則應用於程序的演算法。我們的討論中將類型規則放入函數中，因此模糊了第二者和第三者之間的區別，但它們仍然可以在邏輯上加以區分。

我們可能希望類型系統給我們提供什麼樣的保證呢？請記住，類型檢查器在程序運行前靜態地對程序進行檢查。這意味著它本質上是對程序行為的預測：例如，當它指出某個複雜表達式的類型為num，它實際是在預測程序運行時，該表達式將產生一個數值。我們怎麼知道這個預測是正確的呢，也就是說檢查器從不撒謊？每種類型系統都應該附帶一個證明這一點的定理。

對於類型系統存疑有一個很好的理由，不是懷疑主義的那種。類型檢查器和程序求值器工作方式上有很多不同：

類型檢查器能見到的只有程序文本，求值器運行在真實的存儲器上。
類型環境將標識符綁定到類型，求值器的環境則綁定標識符到值或者存儲位置。
類型檢查器將值的集合（甚至是無限集合）壓縮成類型，而求值器處理的是值本身。
類型檢查器一定會終止，求值器不一定會。
類型檢查器僅需檢查表達式一遍，求值器運行時某個表達式的運行次數可能從零次到無窮次。

因此，我們不應假設這兩者將始終對應！

對於給定的類型系統，我們希望達到的核心目標是——該類型系統是可靠的（sound）。它的意思是：給定表達式（或者程序）e，類型檢查得出其類型為t，當我們運行e時，假設得到了值v，那麼v的類型是t。

證明這個定理的標準方法是分兩步進行，進展（progress）和保持（preservation）。進展的意思是，如果一個表達式能夠通過類型檢查，那麼它應該能進行進一步求值得到新的東西（除非它本身就是值）；保持的意思是，這個求值步驟前後類型不變。如果我們交錯進行這些步驟（先進展再保持，不斷重複），可以得出一個結論，最終的結果和最初被求值的表達式類型相同，因此類型系統確實是可靠的。

例如，考慮表達式：(+ 5 (* 2 3))。它的類型為num。在一個可靠的類型系統中，進展證明，由於該表達式能通過類型檢查，且其當前不是值，它可以進行一步求值——這裡它顯然可以。進行一步求值之後，它被規約成了(+ 5 6)。不出所料，正如保持給出的證明，它的類型也為num。進展表明它還能進行一步求值，得到11。保持再次表明它的類型和上一步的表達式類型相同，都為num。現在，進展發現我們已經得到最終結果，無後續要進行的求值步驟，該值的類型和最初的表達式類型相同。

但這不是完整的故事。有兩點需要說明：

程序可能不會得出最終的結果，它可能永遠循環。這種情況下，該定理嚴格來說並不適用。但是我們仍能看到，計算得到的中間表達式類型將一直保持不變，因此即使程序沒有最終產生一個值，它仍在進行著有意義的計算。
任何特性足夠豐富的語言中都存在一些不能靜態決定的屬性（有些屬性也許本來可以，但是語言的設計者決定將其推遲到運行時決定）。當這類屬性出錯時——比如，數組的索引越界——關於這種程序沒有很好的類型可以約束它們。因此，每個類型完備性定理中都隱含了一組已發布的、允許的異常或者可能發生的錯誤條件。使用該類型系統的開發者隱式的接受了這些條件。

作為第二點的一個例子，典型的靜態類型語言中，都會指明對於向量的定址、列表的索引等操作可能拋出異常。

後面這個說明好像站不住腳。事實上，我們很容易忘記這其實是一條關於運行時不能發生的事情的陳述：這一組異常之外的異常將能被證明不會產生。當然，對最開始就設計為靜態類型的語言，除了不那麼嚴格的類比外，可能搞不清這組異常具體是什麼，因為一開始本就無須定義它們。但是當我們將類型系統添加到已有的語言時——特別是動態類型語言，如Racket或Python——那麼這裡已經有一組明確定義的異常，類型檢查器將會指明其中一些異常（像「函數調用位置不是函數」或者「未找到方法」）不會發生。這就是程序員接納類型系統語法上限制所得到的回報。