柯里化的前生今世（十）：類型和類型系統

03-06

1. 形式化方法

在計算機科學中，尤其在軟體工程和硬體工程領域，

形式化方法（Formal method），是一種數學方法，用於軟體和硬體系統的描述（specification）、開發（development）和驗證（verification）。旨在能像其它工程學科一樣，通過用數學進行分析，來提高設計的可靠性（reliability）和健壯性（robustness）。

為了讓系統表現的和規範（specification）一致，現代軟體工程採用了一系列的形式化方法。其中包括一些強有力的框架，例如，霍爾邏輯（Hoare logic），Algebraic specification language（Specification language），模態邏輯（Modal logic），指稱語義（Denotational semantics）。它們雖然功能強大，但是對程序員來說門檻較高。

另一方面，還有一些輕量級的技術，可以被植入編譯器，連接器或程序分析器中，進行自動校驗。從而，那些不熟悉底層理論的程序員也可以使用它們。模型檢測（Model checking），運行時驗證（Runtime verification）和類型系統（Type system）是常見的輕量級形式化方法。其中類型系統最流行，發展最完善。

2. 歷史

在計算機科學中，最早的類型系統用來區別數字的整數和浮點數。

在20世紀五六十年代，這種分類擴展到了結構化的數據和高階函數中。

70年代，研究者們引入了幾個更為豐富的概念，例如，參數化類型，抽象數據類型，模塊系統，子類型等等，類型系統作為一個獨立的領域形成了。

計算機科學家們也開始意識到，程序語言中的類型與直覺主義邏輯中的命題，之間的聯繫，稱為Curry–Howard correspondence，開始了兩方面的交叉研究。後經範疇論（category theory）的探索，得到了三方面的同構關係，Curry-Howard-Lambek correspondence。

3. 類型系統

類型系統使用了證明論（Proof theory）方法，通過給程序中的值指定不同的種類，來證明程序的某些行為不會發生。

使用類型系統的初衷，是想保證程序不會出現運行時錯誤（Execution error），然而，

一方面，對於什麼是一個『錯誤』，還需要詳細說明，

另一方面，程序是否會出現運行時錯誤，是不可判定的。

（可判定性：Decidability

因此，這裡的『錯誤』應該是所有運行時錯誤的一個子集，

那些類型系統被證明為具有可靠性（Soundness）的程序設計語言，

類型合法的程序才能保證不會出現給定的『錯誤』。

（1）運行時錯誤

當程序被要求做一些未定義的事情時，就會產生Execution error，導致程序崩潰（crash）。Execution error會在運行時表現出來，因此也稱為運行時錯誤（run-time error）。

運行時錯誤，通常包括以下兩種。

有一種運行時錯誤不會立即表現出來，比如數組越界，或者程序跳轉到錯誤的地址。它們不會被立即注意到，但是過了一會就會產生一個出乎意料的結果，我們將這種錯誤稱為『未捕獲的錯誤』（untrapped errors）。

而另外一種運行時錯誤，比如除零，或者訪問非法的內存地址。程序會馬上出錯並停止執行，這種錯誤稱為『被捕獲的錯誤』（trapped errors）。

（2）安全性

如果一塊代碼不會產生『未捕獲的錯誤』，就稱它為安全的（safe）。

如果語言中的所有程序都是安全的，就稱該語言是安全的。

因此，語言如果具有安全性，就不會發生潛在的運行時錯誤。

無類型語言和類型化的語言都可以保障安全性。

無類型語言可以使用運行時檢測來實現，而類型化的語言通過類型來拒絕那些可能會出現不安全性質的程序，類型化的語言也可能會混用運行時檢測和類型校驗。

（3）類型化

程序中的變數在程序執行期間，可能會有不同的取值範圍，

我們把變數可取值的最大範圍稱為這個變數的類型（type）。

例如，具有類型Boolean的變數x，在程序執行期間，只能取布爾值。

指定類型之後的程序設計語言，稱為類型化的語言（typed language）。

如果一個語言，不限制變數的取值，就稱為無類型語言（untyped language），我們既可以說它不具有類型，也可以說它具有一個通用類型，這個類型的取值範圍是程序中所有可能的值。

（4）類型標記

類型系統是類型化語言的一個組成部分，它用來計算和跟蹤程序中所有表達式的類型，從而判斷某段程序是否表現良好（well behaved）。

類型化語言是得益於類型系統，而與代碼中是否具有類型標記無關。

如果程序語言的語法中含有類型標記，就稱該語言是顯式類型化的（explicitly typed），否則就稱為隱式類型化的（implicitly typed）。

主流類型化的語言，都是顯式類型化的。

但是，ML和Haskell可以省略類型聲明，它們的類型系統會自動推斷出程序的類型。

（5）什麼是『錯誤』

判斷一塊代碼是否具有運行時錯誤，這個問題是不可判定的，

即，在不運行這塊代碼的情況下，不存在一個通用演算法回答是或否。

因此，實際操作上，我們需要縮小待排除的運行時錯誤的範圍。

我們指定一個運行時錯誤的子集，它包含所有的『未捕獲的錯誤』，還包含一部分『被捕獲的錯誤』，我們稱這些錯誤為『被禁止的錯誤』（forbidden error）。

如圖所示：

如果程序不會產生『被禁止的錯誤』，就說該程序『行為良好』（well behaved），因此『行為良好』的程序一定是安全的。

程序的安全性比『行為良好』更重要，類型系統的主要目標就是保證程序的安全性——在運行時不會出現『未捕獲的錯誤』。

然而，實際操作中，大部分類型系統被設計成保證程序的『行為良好』，從而也能保證程序的安全性。

（6）靜態檢測和動態檢測

為了避免歧義，下文不再使用靜態類型和強類型這樣的術語，來表示語言的全局特徵，而是使用了靜態檢測（statically check）和強類型檢測（strongly check），來表示某個階段或者這個階段的性質。

如果某個類型化的語言可以不通過運行，只通過編譯時的靜態檢測（statically check），來保證程序的『行為良好』，這樣的語言稱為『被靜態檢測』的語言。

如果某個無類型語言，可以在運行時排除『被禁止的錯誤』，就稱為『被動態檢測』的語言。（這裡指的是動態檢測，而不一定是動態類型檢測

語言被動態檢測，也並不意味著運行時可以不加檢測的執行。

被靜態檢測的語言，通常也需要一些運行時檢測，來保證安全性。

例如，數組越界，通常使用動態檢測來確定。

（7）類型系統的強弱

一個類型化的語言，如果所有合法的程序都是『行為良好』的，就稱該語言是被『強類型檢測』的（strongly checked）。

因此，強類型檢測的語言具有以下特徵：

a) 不會發生『未捕獲的錯誤』——安全性。

b) 那些指定為『被禁止的錯誤』的『被捕獲的錯誤』不會發生。

c) 一些『被捕獲的錯誤』可能發生，需要程序員來避免。

相反，如果某些『未捕獲的錯誤』不能被靜態檢測，就有可能出現不安全的代碼，我們就稱該語言是被『弱類型檢測』的（weakly checked）。

下文

有了這些鋪墊以後，我們就可以用Haskell來學習類型系統了，

這是一個不錯的體驗。

參考

Types and Programming Languages

Type systems: Luca Cardelli