設計模式奏鳴曲（八）：要不要相信類型

09-24

設計模式奏鳴曲（八）：要不要相信類型

來自專欄業餘程序員的個人修養23 人贊了文章

1. 一致性

直覺主義邏輯不承認經典邏輯中的排中律——對於任意命題P，或者P真，或者?P為真。

但是和經典邏輯一樣，接受無矛盾律——任何命題P，P和?P不能同時為真。

無矛盾的邏輯系統，稱為一致的，或者協調的。

一個有用的邏輯系統不能包含矛盾。

2. 完備性

上文關於一致性的討論中，我們並沒有區分邏輯公式的證明和語義，

所謂證明，就是一串符號推導序列，從一些合法的公式經過一步或多步，推導出另一些合法的公式。

而公式的語義則是人為選擇的，人們傾向於為公式選擇可靠的語義，

即，所有可證的公式，在語義上都為真。

但是可靠性並不意味著完備性，

即，所有語義上為真的命題，並不一定總是可證的。

3. 第一第二不完備性定理

人們在研究邏輯系統的時候，對一致性和完備性有著很強烈的追求，

誰都希望自己發明的邏輯系統中沒有矛盾，而且所有為真的命題都可證。

但是1931年，哥德爾發現了兩個定理，粉碎了這個幻想，

任何相容的形式系統，只要蘊涵皮亞諾算術公理，就可以在其中構造在體系中不能被證明的真命題，因此通過推演不能得到所有真命題（即體系是不完備的）。
—— 哥德爾第一不完備性定理

哥德爾定理，給出了符號推導方法的局限性，

如果要求系統無矛盾，那麼某些事實可能是不可證的。

此外，哥德爾第二不完備性定理指出，

任何邏輯自洽的形式系統，只要蘊涵皮亞諾算術公理，它就不能用於證明它本身的相容性。

好吧，連自身的一致性，也不能在系統之內證明了。

所以，在軟體開發過程中，檢查一個軟體系統是否符合設計要求，所使用的方法就是對它進行測試，在這個軟體系統之外進行證明。

4. 排除錯誤

在使用編程語言的時候，我們都或多或少的接觸過類型這個概念。

類型系統的一個重要作用就是，通過類型檢查排除可能會發生的錯誤。

和邏輯系統一樣，如果類型系統保證所有良類型的程序都按預期正常表現，

我們就說它是可靠的，

這是一個很好的性質，如果A成立，則B成立，建立了符號和行為之間的聯繫。

不幸的是，程序即使經過了類型檢查，

也保證不了那些不在預期範圍之內的特性，

即，如果A成立，則C是否成立，我們是不確定的。

例如，對除法表達式進行簡單的類型檢查，能保證除法操作數的類型合法，

但無法避免除0錯誤，

這可能需要更強大的類型系統才行。

另一方面，上面提到良類型的程序，預期會表現正常。

但是，類型不合法的程序，卻未必會出錯。

如果A不成立，那麼B是否成立也是不確定的。

這兩件事和停機問題是一脈相承的，

對於圖靈完備的編程語言來說，要想判定一段程序的所有運行時特徵，唯一的辦法運行它，僅依賴靜態檢查是行不通的。

不存在通用的過程，來判斷一段程序是否停機。

5. Believe the type

那麼我們還要相信類型嗎？

要相信。

我們要相信類型系統，可以幫我們排除那些已被證明的錯誤。

相信類型系統，能指導我們設計出一致的軟體。

Show me your type, and Ill show you your language.

然而，類型信息卻不等同於文檔，它只能提供一些輔助信息，

它不是用來傳遞知識的，真是如有雷同，實屬巧合，

這恰恰反映了在知識傳遞方面，所做的工作還不夠。

結語

本文從邏輯系統出發，介紹了人們經常提及的一些特性，

包括一致性，完備性，可靠性，進而還介紹了哥德爾不完備性定理。

類型檢查可看做是一種邏輯推導，

它可以排除某些已知的錯誤，但也不是萬能的。

要想寫出高質量的代碼，除了在設計方面多花一些心思之外，

更好的辦法就是對它進行測試，不論是靜態檢查還是運行時檢查，

不論是自動化的單元測試，還是人工測試。

完全依賴設計和檢查是行不通的，有時候唯一可以發現錯誤的方法就是運行它。

參考

計算機科學中的現代邏輯學

離散數學教程

數理邏輯

Type Systems

Type-driven Development with Idris

直覺主義邏輯

排中律

無矛盾律

可靠性

完備性

哥德爾不完備性定理

停機問題