Haskell/Curry-Howard 同構

Curry-Howard 同構 是一個引人注目的關係，它將數學的兩個看似無關的領域聯絡起來——型別論和結構邏輯。

簡介

Curry-Howard 同構，以下簡稱 CH，告訴我們，為了證明任何數學定理，我們所要做的就是構建一個反映該定理本質的特定型別，然後找到具有該型別的值。這乍一看非常奇怪：型別與定理有什麼關係？然而，正如我們將看到的，兩者密切相關。在開始之前，我們先說明一個要點：對於這些介紹性段落，我們忽略了諸如 error 和 undefined 之類的表示式的存在，它們的 指稱語義 是 ⊥。這些表達方式具有極其重要的作用，但我們將適時單獨考慮它們。我們還忽略了繞過型別系統的函式，例如 unsafeCoerce#。

我們可以使用 Haskell 的 高階函式 特性構建極其複雜的型別。我們可能會問：給定一個任意型別，它存在值的條件是什麼（我們說型別是可居住的）？第一個猜測可能是“一直都存在”，但這很快就會在例子中破滅。例如，不存在型別為 a -> b 的函式，因為我們沒有辦法將型別為 a 的東西轉換成完全不同的型別 b（除非我們預先知道 a 和 b 是哪種型別，在這種情況下，我們談論的是一個單態函式，例如 ord :: Char -> Int）。

令人難以置信的是，事實證明，只有當一個型別對應於數學邏輯中的一個真定理時，它才可居住。但這種對應關係的本質是什麼？像 a -> b 這樣的型別在邏輯的語境中意味著什麼？

形式邏輯速成課程

在我們開始探索形式邏輯與型別論的關係之前，我們需要一些形式邏輯的背景知識。這是一個非常簡短的介紹；為了更廣泛的理解，我們建議您參考形式邏輯方面的入門教科書。

在日常語言中，我們使用很多“如果…那麼…”句。例如，“如果今天天氣好，那麼我們就去城裡散步”。這類語句在數學中也很常見；我們可以說“如果x是正數，那麼它就有一個（實數）平方根”。形式邏輯是一種用布林邏輯來表示近似於英語含義的語句的方法，我們可以對其進行計算。我們使用符號 A→B（讀作“A 蘊含 B”）來表示只要 A 為真，B 就為真。例如，我們之前的語句可以改寫為“x 是正數 → x 存在一個實數平方根”，這意味著數字的正性蘊含了所需型別的根的存在。我們通常使用字母來代表整個語句，例如，如果W表示語句“天氣好”，而T表示語句“我們去城裡散步”，那麼我們可以說W→T。

我們對 P→Q 的定義有一些缺陷。如果Q是一些總是為真的語句——比如“太陽是熱的”——那麼P是什麼並不重要。P甚至可以是假語句，如果P為真，Q仍然為真，因此蘊含P→Q不被認為是錯誤的。P→Q被定義為只要P為假且Q為真，P→Q就為真。因此，→並不真正代表任何因果關係；像“天空是粉紅色的→太陽是熱的”這樣的語句被定義為真。除了布林邏輯之外，還有其他邏輯代數試圖解決這些“問題”，我們也可以在 Haskell 中構建它們。

在日常語言和數學中經常出現的其他東西被稱為合取和析取。前者表示包含“和”的語句，後者表示包含“或”的語句。我們可以用符號 $(M\wedge S)\to B$ 來表示語句“如果雜誌有貨，而且我有足夠的錢，我就買它”，其中M = “我有足夠的錢”，S = “雜誌有貨”，B = “我買雜誌”。本質上，我們可以將符號 $\wedge$ 讀作“和”。類似地，我們可以將符號 $\vee$ 讀作“或”，因此語句“我將步行或乘坐火車去上班，或兩者都做”可以表示為 $W\vee T$，其中W = “我步行去上班”，而T = “我乘坐火車去上班”。

使用這些符號，以及我們將在後面介紹的其他幾個符號，我們可以產生任意複雜的符號串。這些符號串有兩類：一類表示真命題，通常稱為定理；另一類表示假命題，稱為非定理。需要注意的是，一個符號串是定理還是非定理取決於字母代表的內容，所以$P\vee Q$ 是一個定理，例如，如果P表示“現在是白天”這個命題，而Q表示“現在是晚上”這個命題（忽略像黃昏這樣的例外情況），但如果P是“樹是藍色的”，而Q是“所有鳥都能飛”，它將是一個非定理。如果我們不知道一個符號串是定理還是非定理，我們通常稱它為命題。

邏輯這個學科還有很多細微之處（包括這樣一個事實：當我們說“如果你吃了晚飯，你就會得到甜點”時，我們實際上意味著“只有如果你吃了晚飯，你才會得到甜點”）。如果你對這個學科感興趣，市面上有很多教科書全面地涵蓋了這個學科。

命題是型別

因此，給定一個型別a -> b，在符號邏輯中它意味著什麼？方便的是，它僅僅意味著a → b。當然，只有當a和b是可以在我們的符號邏輯中進一步解釋的型別時，這才是有意義的。這就是CH的本質。此外，正如我們之前提到的，a → b是一個定理，當且僅當a -> b是一個可居住的型別。

讓我們用一個最簡單的Haskell函式來看一看。const的型別是a -> b -> a。翻譯成邏輯，我們有a → b → a。這必須是一個定理，因為型別a -> b -> a是透過const這個值來居住的。現在，表達a → b的另一種方式是“如果我們假設a為真，那麼b必須為真”。所以a → b → a意味著，如果我們假設a為真，那麼如果我們進一步假設b為真，那麼我們可以得出a。這當然是一個定理；我們假設了a，所以a在我們假設的情況下是成立的。

⊥的問題

我們已經提到，如果一個型別是可居住的，那麼它對應於一個定理。然而，在Haskell中，每個型別都是透過undefined這個值來居住的。事實上，更一般地說，任何具有forall a. a型別的，一個具有⊥的語義值的，都是一個問題。在型別論中，⊥對應於邏輯中的不一致性；我們可以使用Haskell型別證明任何定理，因為每個型別都是可居住的。因此，Haskell的型別系統實際上對應於一個不一致的邏輯系統。然而，如果我們使用Haskell型別系統的一個有限子集，特別是禁止多型型別，那麼我們就會得到一個一致的邏輯系統，我們可以在其中做一些很酷的事情。從今以後，我們假設我們正在使用這樣的型別系統。

現在我們有了CH的基礎知識，我們可以開始更多地解釋型別和命題之間的關係。

邏輯運算及其等價物

符號邏輯的本質是一組命題，例如P和Q，以及組合這些命題的不同方式，例如Q → P或$P\vee Q$。這些組合命題的方式可以被認為是對命題的運算。根據CH，命題對應於型別，所以我們應該有這樣的結論：這些命題組合器的CH等價物是型別運算，通常被稱為型別構造器。我們已經看到了一個例子：邏輯中的蘊含運算子→對應於型別構造器(->)。本節的其餘部分將繼續探索其餘的命題組合器，並解釋它們的對應關係。

合取和析取

為了使$A\wedge B$成為一個定理，A和B都必須是定理。因此，$A\wedge B$的證明相當於證明A和B。記住，為了證明一個命題A，我們找到一個型別為A的值，其中A和A是CH對應物。所以在這個例子中，我們希望找到一個包含兩個子值的值：第一個子值型別對應於A，第二個子值型別對應於B。這聽起來很像一個對。事實上，我們用(a, b)來表示符號串$A\wedge B$，其中a對應於A，b對應於B。

析取與合取相反。為了使$A\vee B$成為一個定理，A或B必須是一個定理。同樣，我們尋找一個包含型別為A的值或型別為B的值。這就是Either。Either A B是對應於命題$A\vee B$的型別。

假命題

在我們的邏輯系統中，偶爾需要表示一個假命題。根據定義，假命題是不能被證明的命題。所以我們正在尋找一個不可居住的型別。雖然這些型別在預設庫中都不存在（不要與()型別混淆，()型別恰好只有一個值），但我們可以定義一個（或者對於不支援Haskell2010的舊版本GHC，我們開啟-XEmptyDataDecls標誌）。

data Void

省略建構函式的效果意味著Void是一個不可居住的型別。所以Void型別對應於我們邏輯中的非定理。這裡有一些方便的推論

1. (Void, A) 和 (A, Void) 對於任何型別 A 都是不可居住型別，對應於 $F\wedge A$ 和 $A\wedge F$ 都是非定理，如果 F 是一個非定理。
2. Either Void A 和 Either A Void 本質上與任何型別 A 的 A 相同， 對應於 $F\vee A$ 和 $A\vee F$，其中 F 是一個非定理，只有當 A 是一個定理時才是定理。
3. 任何對應於非定理的型別都可以用 Void 替換。這是因為任何非定理型別都必須是不可居住的，所以用 Void 替換它不會改變任何東西。Void 實際上等同於任何非定理型別。

4. 正如我們在第一節中提到的，蘊涵 P → Q 如果 Q 為真則為真，無論 P 的真值如何。所以我們應該能夠找到一個型別為 Void -> a 的項。事實上，確實存在一個，但解釋起來有點複雜：答案是空函式。我們可以將一個函式 f :: A -> B 定義為一個（可能是無限的）對集合，其第一個元素是 A 中的一個元素（定義域），第二個元素是 f 在此項上的輸出，是 B 中的一個元素（陪域）。例如，自然數上的後繼函式表示為 {(0,1), (1,2), (2,3), ...}。請注意，為了成為一個（完全且定義良好的）函式，對於每個型別為 A 的項 a，我們必須有精確地一對 (a, f a)。

   空函式，我們稱之為 empty，用這種方式表示為空集。但是，由於我們必須為定義域的每個元素提供一個對，而我們的表示中沒有對，因此定義域型別必須為空，即 Void。範圍型別怎麼樣？empty 從不產生任何輸出，因此對範圍型別沒有任何限制。因此，假設範圍型別具有任何型別是有效的，因此我們可以說 empty :: forall a. Void -> a。不幸的是，不可能在 Haskell 中編寫此函式；理想情況下，我們希望編寫類似的東西

   empty :: Void -> a
   

   併到此為止，但這是非法的 Haskell。我們能做到的最接近的是以下

   empty :: Void -> a
   empty _ = undefined
   

   或者

   empty :: Void -> a
   empty = empty
   

   另一種合理的方法是編寫（在帶有 EmptyCase 擴充套件的 GHC 中有效）

   empty x = case x of { }
   

   case 語句是完美形成的，因為它處理了 x 的所有可能值。

   請注意，這完全安全，因為此函式的右側永遠不會被訪問（因為我們沒有要傳遞給它的東西）。因此，所有這些的結論是 Void -> a 是一個居住型別，就像如果 P 為假，則 P → Q 為真一樣。

否定

邏輯中的 ¬ 操作將定理轉換為非定理，反之亦然：如果 A 是一個定理，那麼 ¬A 是一個非定理；如果 A 是一個非定理，那麼 ¬A 是一個定理。如何在 Haskell 中表示它？答案很狡猾。我們定義一個類型別名

type Not a = a -> Void

所以對於型別 A，Not A 只是 A -> Void。這是怎麼運作的？好吧，如果 A 是一個定理型別，那麼 A -> Void 必須是不可居住的：沒有函式可以返回任何值，因為返回型別 Void 沒有值（函式必須為 A 的所有居住者提供值）！另一方面，如果 A 是一個非定理，那麼 A 可以用 Void 替換，正如我們在上一節中探討的那樣。那麼函式 id :: Void -> Void 是 Not A 的一個居住者，所以 Not A 是一個定理，如所要求的（函式不需要提供任何值，因為它在其定義域中沒有居住者。然而，它是一個函式 - 有一個空圖）。

公理邏輯和組合子演算

到目前為止，我們只使用了 Haskell 型別系統的一些非常基本的功能。事實上，我們提到的邏輯的大多數功能都可以使用一種非常基本的“程式語言”組合子演算來探索。為了充分理解 CH 如何將這兩個數學領域緊密地聯絡在一起，我們需要公理化我們對形式邏輯和程式語言的討論。

公理邏輯

我們從關於 → 操作如何工作的兩個公理開始（從現在開始，我們假設 → 是一個右結合函式，即 A → B → C 表示 A → (B → C))

1. A → B → A
2. (A → B → C) → (A → B) → A → C

第一個公理說，對於任何兩個命題 A 和 B，如果我們假設 A 和 B 都是真的，我們就知道 A 是真的。第二個公理說，如果 A 蘊涵 B 蘊涵 C（或者等效地，如果 C 為真只要 A 和 B 為真），並且 A 本身蘊涵 B，那麼知道 A 為真就足以得出 C 為真的結論。這可能看起來很複雜，但經過一番思考，你就會發現這是常識。想象我們有一組各種顏色的盒子，有些有輪子，有些有蓋子，所有有輪子的紅色盒子也有蓋子，所有紅色盒子都有輪子。選擇一個盒子。設 A =“所考慮的盒子是紅色的”，B =“所考慮的盒子有輪子”，C =“所考慮的盒子有蓋子”。那麼第二定律告訴我們，由於 A → B → C（所有有輪子的紅色盒子也有蓋子），並且 A → B（所有紅色盒子都有輪子），那麼如果 A（如果盒子是紅色的），那麼 C 必須為真（盒子有蓋子）。

我們還允許一條推理定律，稱為肯定前件

1. 如果 A → B，並且 A，那麼 B。

這條定律允許我們根據舊的定理建立新的定理。這應該是相當明顯的；它本質上是 → 的含義的定義。這個小基礎提供了一個足夠簡單的邏輯系統，它足夠表達以涵蓋我們大多數的討論。以下是我們系統中 A → A 定律的示例證明

首先，我們知道這兩個公理是定理

• A → B → A
• (A → B → C) → (A → B) → A → C

你會注意到，第二個公理的左側看起來有點像第一個公理。第二個公理保證，如果我們知道 A → B → C，那麼我們可以得出 (A → B) → A → C。在這種情況下，如果我們讓 C 與 A 是同一個命題，那麼我們有，如果 A → B → A，那麼 (A → B) → A → A。但我們已經知道 A → B → A，那是第一個公理。因此，我們有 (A → B) → A → A 是一個定理。如果我們進一步讓 B 為命題 C → A，對於另一個命題 C，那麼我們有，如果 A → C → A，那麼 A → A。但，同樣地，我們知道 A → C → A（它又是第一個公理），所以 A → A，正如我們所希望的那樣。

這個例子表明，給定一些簡單的公理和一種從舊的定理中建立新定理的簡單方法，我們可以推匯出更復雜的定理。這可能需要一段時間才能實現 - 在這裡，我們有幾行推理來證明顯然的語句 A → A 是一個定理！ - 但最終我們還是做到了。這種形式化很有吸引力，因為我們本質上定義了一個非常簡單的系統，並且很容易研究該系統如何工作。

組合子演算

lambda 演算 是一種從非常簡單的基礎定義簡單程式語言的方法。如果你還沒有閱讀剛剛連結到的章節，我們建議你至少閱讀關於演算的無型別版本的介紹部分。以下是一些複習資料，以防你感覺生疏。lambda 項是以下三種情況之一

• 一個值，v。
• 一個lambda 抽象 $\lambda x.t$，其中 t 是另一個 lambda 項。
• 一個應用$(t_{1}t_{2})$，其中$t_{1}$和$t_{2}$是 lambda 表示式。

也存在一個歸約法則，稱為beta 歸約

• $((\lambda x.t_{1})t_{2})$ → $t_{1}[x:=t_{2}]$，其中$t_{1}[x:=t_{2}]$表示$t_{1}$，其中所有x的自由出現都被替換為$t_{2}$。

如lambda 演算文章中所述，當試圖確定識別符號的自由出現的概念時，困難就出現了。組合子演算是由美國數學家哈斯凱爾·卡里（以他命名的某種程式語言）發明的，就是因為這些困難。組合子演算有許多變體，但我們這裡考慮最簡單的變體之一。我們從兩個所謂的組合子開始

• K接收兩個值並返回第一個。在 lambda 演算中，$\mathbf {K} =\lambda xy.\ x$.
• S接收一個二元函式、一個一元函式和一個值，並將傳遞給一元函式的值和該值應用於二元函式。同樣，在 lambda 演算中：$\mathbf {S} =\lambda xyz.\ xz(yz)$.

你應該將第一個函式識別為const。第二個更復雜，它是((->) e)么半群中的單子函式ap（本質上是 Reader）。這兩個組合子構成了整個 lambda 演算的完整基礎。每個 lambda 演算程式都可以只使用這兩個函式來編寫。

直覺主義邏輯與經典邏輯

到目前為止，我們已經證明的所有結果都是直覺主義邏輯的定理。讓我們看看當我們試圖證明經典邏輯的基本定理 Not Not A -> A 時會發生什麼。回想一下，這可以翻譯為 ((A -> Void) -> Void) -> A 。所以，給定一個型別為 (A -> Void) -> Void 的函式，我們需要一個型別為 A 的函式。現在，型別為 (A -> Void) -> Void 的函式的存在，當且僅當型別 A -> Void 是無居民的，換句話說，當且僅當型別 A 是有居民的。所以我們需要一個函式，它接收任何有居民的型別，並返回該型別的一個元素。雖然在計算機上執行起來很簡單——我們只需要找到每種型別的“最簡單”或“第一個”居民——但是沒有辦法使用標準的 lambda 演算或組合子技術來做到這一點。所以我們看到，這個結果無法使用這兩種技術來證明，因此其背後的邏輯是直覺主義的，而不是經典的。

相反，考慮一個傳統的錯誤處理函式，它在發生錯誤時呼叫throw，將計算轉移到catch。throw函式會取消原始函式的任何返回值，因此它的型別為A -> Void，其中A是其引數的型別。然後，catch函式將throw函式作為其引數，如果throw觸發（即返回一個Void），則會返回throw函式的引數。因此，catch的型別是 ((A -> Void) -> Void) -> A 。