Haskell/多型性

引數多型性

章節目標 = 簡短，使讀者能夠閱讀包含 ∀ 的程式碼 (ParseP) 並使用庫 (ST) 而不感到恐懼。問題 Talk:Haskell/The_Curry-Howard_isomorphism#Polymorphic types 將由本節解決。

連結到以下論文：Luca Cardelli：理解型別、資料抽象和多型性。

forall a

一個多型函式是一個對許多不同型別都起作用的函式。例如，

  length :: [a] -> Int

可以計算任何列表的長度，無論是字串 String = [Char] 還是整數列表 [Int]。型別變數 a 表示 length 接受任何元素型別。其他多型函式的示例包括

  fst :: (a, b) -> a
  snd :: (a, b) -> b
  map :: (a -> b) -> [a] -> [b]

型別變數總是以小寫字母開頭，而諸如 Int 或 String 之類的具體型別總是以大寫字母開頭。這使我們能夠區分它們。

有一種更顯式的方式來表明 a 可以是任何型別

 length :: forall a. [a] -> Int

換句話說，“對於所有型別 a，函式 length 接受一個型別為 a 的元素列表並返回一個整數”。您應該將舊簽名視為帶 forall 關鍵字的新簽名的縮寫。也就是說，編譯器將在內部為您插入任何缺少的 forall。另一個例子：fst 的型別簽名實際上是 forall a b. (a, b) -> a 的簡寫

  fst :: forall a. forall b. (a,b) -> a

或等效地

  fst :: forall a b. (a,b) -> a

類似地，map 的型別實際上是

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

這個概念，即某事物適用於所有型別或對所有事物都成立，被稱為全稱量化。在數學邏輯中，符號 ∀（一個倒置的 A，讀作“對於所有”）通常用於此；它被稱為全稱量詞。

高階型別

使用顯式的 forall，現在可以編寫期望多型引數的函式，例如

  foo :: (forall a. a -> a) -> (Char,Bool)
  foo f = (f 'c', f True)

這裡，f 是一個多型函式，它可以應用於任何事物。特別是，foo 可以將它應用於字元 'c' 和布林值 True。

在 Haskell98 中無法編寫像 foo 這樣的函式，型別檢查器會抱怨 f 只能應用於型別 Char 或型別 Bool 的值，並拒絕定義。我們最接近 foo 的型別簽名的是

  bar :: (a -> a) -> (Char, Bool)

它與

  bar :: forall a. ((a -> a) -> (Char, Bool))

但它與 foo 大不相同。最外層的 forall 表示 bar 保證可以處理任何引數 f，只要 f 具有 a -> a 的形狀，對於某些 bar 不知道的型別 a 而言。將此與 foo 進行對比，在 foo 中，是引數 f 保證具有 a -> a 的形狀，對於所有型別 a 同時而言，並且是 foo 利用了該承諾，透過選擇 a = Char 和 a = Bool。

關於命名法，像 bar 這樣的簡單多型函式被稱為具有秩 1 型別，而型別 foo 被歸類為秩 2 型別。一般來說，秩 n 型別是一個函式，它至少有一個秩 (n-1) 引數，但沒有任何更高秩的引數。

高階型別的理論基礎是F 系統，也稱為二階 lambda 演算。為了更好地理解 forall 的含義及其在 foo 和 bar 中的位置，我們將在 F 系統 部分詳細介紹它。

Haskell98 基於 Hindley-Milner 型別系統，它是 F 系統的受限版本，不支援 forall 和秩 2 型別或更高秩的型別。您必須啟用 RankNTypes 語言擴展才能使用 F 系統的全部功能。

Haskell98 不支援高階型別是有充分理由的：針對完整 F 系統的型別推斷是不可判定的；程式設計師將不得不寫下所有型別簽名。因此，Haskell 的早期版本採用了 Hindley-Milner 型別系統，它只提供簡單的多型函式，但作為交換，它能夠實現完全型別推斷。近年來，研究的進展減少了編寫型別簽名的負擔，並在當前的 Haskell 編譯器中使秩 n 型別成為現實。

runST

對於實際的 Haskell 程式設計師來說，ST 單子 可能是野生狀態下秩 2 型別的第一個示例。類似於 IO 單子，它提供可變引用

  newSTRef   :: a -> ST s (STRef s a)
  readSTRef  :: STRef s a -> ST s a
  writeSTRef :: STRef s a -> a -> ST s ()

和可變陣列。型別變數 s 表示正在操作的狀態。但與 IO 不同，這些有狀態的計算可以在純程式碼中使用。特別是，函式

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

設定初始狀態，執行計算，丟棄狀態並返回結果。如您所見，它具有秩 2 型別。為什麼？

關鍵在於可變引用應該侷限在一個 `runST` 中。例如：

  v   = runST (newSTRef "abc")
  foo = runST (readSTRef v)

是錯誤的，因為在一個 `runST` 上下文中建立的可變引用在第二個 `runST` 中被再次使用。換句話說，`a` 在 `(forall s. ST s a) -> a` 中的結果型別可能不像 `v` 的情況下那樣是 `STRef s String` 這樣的引用。但是，二階型別保證了這一點！因為引數必須對 `s` 多型，所以它必須為所有狀態 `s` 返回相同型別 `a`；結果 `a` 不能依賴於狀態。因此，上面的錯誤程式碼片段包含型別錯誤，編譯器將拒絕它。

您可以在原始論文 Lazy functional state threads 中找到有關 ST 單子的更詳細解釋。

非謂詞性

• 謂詞性 = 型別變數例項化為單型別。非謂詞性 = 也是多型別。例如：`length [id :: forall a . a -> a]` 或 `Just (id :: forall a. a -> a)`。與高階型別略有不同。

• 多型型別根據其通用性（即 `isInstanceOf`）的關係。
• haskell-cafe：RankNTypes 簡短解釋。

有界引數多型性

型別類

待辦事項

系統 F

本節目標 = 一點 lambda 演算基礎，以防止隱式型別引數傳遞導致的腦損傷。

• 系統 F = 所有這些 ∀-stuff 的基礎。
• 顯式型別應用，例如 `map Int (+1) [1,2,3]`。∀ 類似於函式箭頭 ->。
• 項依賴於型別。大 Λ 用於型別引數，小 λ 用於值引數。

例子

本節目標 = 使讀者能夠判斷是否在自己的程式碼中使用具有 ∀ 的資料結構。

• Church 數，任意遞迴型別的編碼（正性條件）：`forall x. (F x -> x) -> x`
• 延續，模式匹配：`maybe`、`either` 和 `foldr`

也就是說，∀ 可以很好地用於在 Haskell 中實現資料型別。

其他形式的多型性

到目前為止，我們主要討論了引數多型性。然而，在其他程式語言中主要使用另外兩種形式的多型性。

• 特設多型性
• 子型別多型性

特設多型性

在 C++ 中，特設多型性可以看作等同於函式過載

int square(int x);
float square(float x);

我們可以在 Haskell 中使用型別類來做類似的事情

class Square a where
    square :: a -> a
    
instance Square Int where
    square x = x * x

instance Square Float where
    square x = x * x

特設多型性的主要要點是，總會有一些函式無法接受的型別，儘管函式可以接受的型別數量可能是無限的。將其與引數多型性形成對比，引數多型性在 C++ 中等同於模板函式

template <class T>
T id(T a) {
    return a;
}

template <class A, class B>
A const_(A first, B second) {
    return first;
}

template <class T>
int return10 (T a) {
    return 10;
}

它等同於 Haskell 中的以下內容

id :: a -> a
id a = a

const :: a -> b -> a
const a _ = a

return10 :: a -> Int
return10 _ = 10

引數多型性的主要要點是，任何型別都必須作為函式的輸入被接受，無論其返回型別是什麼。

注意，這兩種形式的多型性都不允許存在兩個僅返回值型別不同的同名函式。

例如，以下 C++ 程式碼無效

void square(int x);
int square(int x);

Haskell 版本也是如此

class Square a where
    square :: a -> a
    
instance Square Int where
    square x = x*x

instance Square Int where
    square x = ()

因為編譯器在給定任意函式呼叫時無法確定使用哪個版本。

子型別多型性

待辦事項 = 對比 OOP 中的多型性和相關內容。

自由定理

本節目標 = 使讀者能夠提出自由定理。無需證明，直覺就足夠了。

• 引數多型性的自由定理。

另請參閱

• Luca Cardelli. On Understanding Types, Data Abstraction, and Polymorphism.