Haskell/存在量化的型別

存在量化的型別 (解決方案)

型別樂趣

多型性
存在量化的型別
高階型別類
幻影型別
廣義代數資料型別 (GADT)
資料型別代數
 型別構造器 & 種類

存在型別，或者簡稱為“存在”，是一種將一組型別“壓縮”成一個單一型別的型別。

存在是 GHC 的型別系統擴充套件的一部分。它們不是 Haskell98 的一部分，因此您必須使用額外的命令列引數 -XExistentialQuantification 編譯包含它們的任何程式碼，或者在使用存在的原始碼頂部新增 {-# LANGUAGE ExistentialQuantification #-} 。

`forall` 關鍵字

forall 關鍵字用於顯式地將新的型別變數引入作用域。例如，考慮一下您已經無意中寫過一百次的東西

示例： 多型函式

map :: (a -> b) -> [a] -> [b]

但這些 a 和 b 是什麼呢？嗯，它們是型別變數，你回答說。編譯器看到它們以小寫字母開頭，因此允許任何型別來填充該角色。另一種說法是這些變數是“普遍量化的”。如果您學習過形式邏輯，您一定遇到過量詞：“對所有”（或 $\forall$ ）和“存在”（或 $\exists$ ）。它們對後面的內容進行“量化”：例如， $\exists x$ 表示後面的內容對至少一個 x 值成立。 $\forall x$ 表示後面的內容對您可以想象的任何可能的 x 值都成立。例如， $\forall x,\,x^{2}\geq 0$ 和 $\exists x,\,x^{3}=27$ 。

forall 關鍵字以類似的方式對型別進行量化。我們將 map 的型別改寫如下

示例： 顯式地量化型別變數

map :: forall a b. (a -> b) -> [a] -> [b]

所以我們看到，對於我們可以想象的任何 a 和 b 型別組合，map 都採用 (a -> b) -> [a] -> [b] 型別。例如，我們可能選擇 a = Int 和 b = String。那麼說 map 的型別是 (Int -> String) -> [Int] -> [String] 是有效的。在這裡，我們將 map 的通用型別例項化為更具體的型別。

但是，在 Haskell 中，任何小寫型別引數的引入都隱含地以 forall 關鍵字開頭，因此前面兩個關於 map 的型別宣告是等價的，下面的宣告也是如此

示例： 兩個等效的型別語句

id :: a -> a
id :: forall a . a -> a

真正有趣的是，forall 的作用是你可以對它引入的型別變數施加額外的約束。這些約束， $P(x)$ ，充當對型別變數， $x$ ，的某種保證特定屬性的限制，（類似於 $\exists x,P(x)$ 或 $\forall x,P(x)$ 規定）。

讓我們直接深入瞭解，看看存在型別在實際中的強大功能。

示例：異構列表

Haskell 型別類系統的基本前提是將所有共享相同屬性的型別分組。因此，如果您知道一個型別是某個類 C 的成員，那麼您就知道該型別的某些資訊。例如，Int 是類 Eq 的成員，所以我們知道 Int 的元素可以比較相等。

假設我們有一組值。我們不知道它們是否都屬於相同的型別，但我們知道它們都是某個類的成員（並且，透過擴充套件，所有值都具有一定的屬性）。將所有這些值放入一個列表中可能很有用。我們通常無法做到這一點，因為列表元素必須具有相同的型別（型別方面是同構的）。但是，存在型別允許我們透過定義“型別隱藏器”或“型別框”來放鬆此要求。

示例：構建異構列表

 data ShowBox = forall s. Show s => SB s
 
 heteroList :: [ShowBox]
 heteroList = [SB (), SB 5, SB True]

我們不會詳細解釋資料型別定義的含義，但其含義應該很直觀。重要的是，我們正在對三種不同型別的三個值呼叫建構函式，[SB (), SB 5, SB True]，但我們能夠將它們全部放入一個列表中，因此我們必須以某種方式為每個值擁有相同的型別。本質上，是的。這是因為我們對 forall 關鍵字的使用為我們的建構函式提供了型別 SB :: forall s. Show s => s -> ShowBox。如果我們現在要編寫一個打算將 heteroList 傳遞給它的函式，我們不能對 SB 中的值應用像 not 這樣的函式，因為它們的型別可能不是 Bool。但我們確實知道每個元素的一些資訊：它們可以透過 show 轉換為字串。實際上，這幾乎是我們知道的關於它們唯一的知識。

示例：使用我們的異構列表

 instance Show ShowBox where
  show (SB s) = show s        -- (*) see the comment in the text below
 
 f :: [ShowBox] -> IO ()
 f xs = mapM_ print xs

 main = f heteroList

讓我們更詳細地說明一下。在 ShowBox 的 show 定義中 - 標記為 (*) 請參閱下面的文字中的註釋 的行 - 我們不知道 s 的型別。但正如我們提到的，我們確實知道該型別是 Show 的例項，因為 SB 建構函式上的約束。因此，對 s 使用函式 show 是合法的，如函式定義的右側所示。

至於 f，請回憶 print 的型別

示例：相關函式的型別

 print :: Show s => s -> IO () -- print x = putStrLn (show x)
 mapM_ :: (a -> m b) -> [a] -> m ()
 mapM_ print :: Show s => [s] -> IO ()

正如我們剛剛宣告 ShowBox 是 Show 的例項，我們可以列印列表中的值。

進一步解釋

理解 forall 的一種方法是將型別視為一組可能的值。例如，Bool 是集合 {True, False, ⊥}（記住，底部，⊥，是每種型別的成員！），Integer 是整數的集合（以及底部），String 是所有可能的字串的集合（以及底部），等等。forall 充當斷言指定型別（即值的集合）之間共性或交集的一種方式。例如，forall a. a 是所有型別的交集。這個子集恰好是隻有底部元素 {⊥} 的集合，因為它是在每種型別中的一個隱式值。也就是說，只有底部的值可用的型別。但是，由於每個 Haskell 型別都包含底部，{⊥}，因此這種量化實際上規定了所有 Haskell 型別。但是，允許對它的唯一操作是那些可用於其唯一元素是底部的型別的操作。

更多示例

列表 [forall a. a] 是元素型別均為 forall a. a 的列表的型別，即底部列表。
列表 [forall a. Show a => a] 是元素型別均為 forall a. Show a => a 的列表的型別。Show 類約束要求可能的型別也是類 Show 的成員。但是，⊥ 仍然是所有這些型別的唯一公共值，因此這也是一個底部列表。
列表 [forall a. Num a => a] 要求每個元素都是類 Num 的成員。因此，可能的值包括數字文字，其具有特定型別 forall a. Num a => a，以及底部。
forall a. [a] 是元素型別均為 a 的列表的型別。由於我們根本無法假定任何特定型別，因此這也是一個底部列表。

我們看到，大多數型別上的交集只會導致底部，因為型別通常沒有任何共同的值，因此無法對它們的聯合值做出假設。

但是，請記住，在上節中，我們使用“型別隱藏器”開發了一個異構列表。這個“型別隱藏器”充當包裝型別，透過暗示對允許型別施加的謂詞或約束來保證某些功能。在這種情況下，它們必須是型別類 Show 的成員。一般來說，這似乎是 forall 的目的，即對型別宣告中允許的型別施加型別約束，從而保證使用此類型別的某些功能。

讓我們宣告一個。

示例：存在型別

 data T = forall a. MkT a

這意味著

示例：這定義了一個多型建構函式，或一個用於 T 的建構函式系列。

MkT :: forall a. (a -> T)

因此，我們可以將任何我們想要傳遞給 MkT 的型別 a 傳遞給它，它將建立一個 T。那麼，當我們使用模式匹配來解構 T 值時會發生什麼？…

示例：對我們的存在建構函式進行模式匹配

 foo (MkT x) = ... -- what is the type of x?

正如我們剛剛提到的，x 可以是任何型別。這意味著它是一些任意型別的成員，因此具有型別 forall a. a。換句話說，只有底部 ⊥ 可用的集合。

但是，我們可以建立一個異構列表

示例：構建異構列表

 heteroList = [MkT 5, MkT (), MkT True, MkT map]

當然，當我們對 heteroList 進行模式匹配時，我們不能對它的元素做出任何假設^[1]。因此，從技術上講，除了將它們簡化為 WHNF^[2] 之外，我們不能對它的元素做任何有用的操作。但是，如果我們引入類約束

示例：一個新的存在資料型別，帶有類約束

 data T' = forall a. Show a => MkT' a

類約束用於限制我們正在交叉的型別，這樣我們現在在 T' 中的值是屬於 Show 的成員 的某些任意型別的元素。這意味著我們可以將 show 應用於解構後型別為 a 的值。無論該值實際是什麼型別都無關緊要。

示例：使用我們新的異構設定

 heteroList' = [MkT' 5, MkT' (), MkT' True, MkT' "Sartre"]
 main = mapM_ (\(MkT' x) -> print x) heteroList'

 {- prints:
 5
 ()
 True
 "Sartre"
 -}

總之，通用量詞與資料型別的互動產生了一個限定的型別子集，保證了由一個或多個類約束描述的某些功能。

示例：`runST`

您可能尚未遇到的一種單子是 ST 單子。這本質上是 State 單子的一個更強大的版本：它具有更復雜的結構，並且涉及一些更高階的主題。它最初是為了為 Haskell 提供 IO 而編寫的。正如我們在Understanding monads 章節中提到的，IO 本質上只是具有包含有關現實世界的所有資訊的“環境”的 State 單子。實際上，至少在 GHC 內部，使用 ST，並且環境是一種稱為 RealWorld 的型別。

要退出 State 單子，您可以使用 runState。ST 的類似函式稱為 runST，它具有一種非常特殊的型別

示例：runST 函式

runST :: forall a. (forall s. ST s a) -> a

這實際上是更復雜語言特徵（稱為 rank-2 多型性）的示例，我們在此不做詳細介紹。重要的是要注意，沒有用於初始狀態的引數。實際上，ST 使用與 State 不同的狀態概念；雖然 State 允許您 get 和 put 當前狀態，但 ST 提供了對引用的介面。您可以使用 newSTRef :: a -> ST s (STRef s a) 建立引用（型別為 STRef），提供初始值，然後您可以使用 readSTRef :: STRef s a -> ST s a 和 writeSTRef :: STRef s a -> a -> ST s () 來操作它們。因此，ST 計算的內部環境不是一個特定值，而是一個從引用到值的對映。因此，您不需要為 runST 提供初始狀態，因為初始狀態只是不包含任何引用的空對映。

但是，事情並不像看起來那樣簡單。是什麼阻止您在一個 ST 計算中建立引用，然後在另一個計算中使用它？我們不想允許這樣做，因為（出於執行緒安全的原因）不應該允許任何 ST 計算假設初始內部環境包含任何特定引用。更具體地說，我們希望以下程式碼無效

示例：錯誤的 ST 程式碼

 let v = runST (newSTRef True)
 in runST (readSTRef v)

是什麼能阻止這種情況？runST 型別中 rank-2 多型性的效果是限制類型變數 s 的範圍 在第一個引數內。換句話說，如果型別變數 s 出現在第一個引數中，它就不能出現在第二個引數中。讓我們看一下這到底是如何完成的。假設我們有一些類似以下程式碼的程式碼

示例：更簡潔的錯誤 ST 程式碼

... runST (newSTRef True) ...

編譯器嘗試將型別組合在一起

示例：編譯器的型別檢查階段

newSTRef True :: forall s. ST s (STRef s Bool)
runST :: forall a. (forall s. ST s a) -> a
together, (forall s. ST s (STRef s Bool)) -> STRef s Bool

第一個方括號中 forall 的重要性在於我們可以更改 s 的名稱。也就是說，我們可以寫

示例：型別不匹配！

together, (forall s'. ST s' (STRef s' Bool)) -> STRef s Bool

這很有道理：在數學中，說 $\forall x.x>5$ 與說 $\forall y.y>5$ 完全相同；你只是給變數起了不同的標籤。然而，我們上面的程式碼存在一個問題。請注意，因為 forall 不作用於 runST 的返回值型別，我們也沒有將那裡的 s 重新命名。但突然之間，我們出現了型別不匹配！第一個引數中 ST 計算的結果型別必須與 runST 的結果型別匹配，但現在它們不匹配了！

存在量詞的關鍵特徵在於，它允許編譯器泛化第一個引數中狀態的型別，因此結果型別不能依賴於它。這巧妙地繞開了我們的依賴性問題，並將對 runST 的每次呼叫“隔離”到它自己的小堆中，引用無法在不同的呼叫之間共享。

量化型別作為積和和

一個全稱量化型別可以被解釋為型別的無限積。例如，像

示例： 恆等函式

 id :: forall a. a -> a
 id a = a

這樣的多型函式可以理解為一個積，或者一個元組，其中包含每個可能的型別 a 的單個函式。要構造這種型別的的值，我們必須一次性提供元組的所有組成部分。對於函式型別來說，由於多型性，這是可能的——一個公式生成無限多個函式。

對於數值型別，可以使用一個數值常量來一次性初始化多個型別。例如，在

示例： 多型值

 x :: forall a. Num a => a
 x = 0

中，x 可以被理解為一個元組，它包含一個 Int 值、一個 Double 值等等。

類似地，一個存在量化型別可以被解釋為一個無限和。例如，

示例： 存在型別

 data ShowBox = forall s. Show s => SB s

可以被理解為一個和

示例： 和型別

 data ShowBox = SBUnit | SBInt Int | SBBool Bool | SBIntList [Int] | ...

要構造這種型別的的值，我們只需要選擇一個建構函式。一個多型建構函式 SB 將所有這些建構函式組合成一個。

量化作為一種基元

全稱量化對於定義尚未定義的資料型別很有用。假設 Haskell 中沒有內建的配對。可以使用量化來定義它們。

{-# LANGUAGE ExistentialQuantification, RankNTypes #-}

newtype Pair a b = Pair (forall c. (a -> b -> c) -> c)

makePair :: a -> b -> Pair a b
makePair a b = Pair $ \f -> f a b

在 GHCi 中

 λ> :set -XExistentialQuantification
 λ> :set -XRankNTypes
 λ> newtype Pair a b = Pair {runPair :: forall c. (a -> b -> c) -> c}
 λ> makePair a b = Pair $ \f -> f a b
 λ> pair = makePair "a" 'b' 
 
 λ> :t pair
 pair :: Pair [Char] Char
 
 λ> runPair pair (\x y -> x)
 "a"
 
 λ> runPair pair (\x y -> y)
 'b'