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被定義為真。因此，→ 並不真正代表任何因果關係；像“天空是粉紅色的 → 太陽很熱”這樣的語句被定義為真。除了布林邏輯之外，還有其他邏輯代數試圖解決這些“問題”，我們也可以在 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\wedge B$ 表示為 (a, 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
   

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

   empty x = case x of { }
   

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

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

否定

邏輯中的 ¬ 操作將定理轉換為非定理，反之亦然：如果 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 演算 文章中所述，當試圖確定識別符號自由出現的概念時，就會遇到困難。組合子演算是由美國數學家 Haskell Curry（以某種程式語言命名）發明的，因為這些困難。組合子演算有許多基本變體，但我們這裡只考慮最簡單的一種。我們從兩個所謂的 **組合子** 開始

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

您應該認識到第一個函式是 const。第二個函式更復雜，它是在 ((->) e) 單子（本質上是 Reader）中的單子函式 ap。這兩個組合子構成了整個 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 。