Haskell/多型性

型別樂趣

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

引數多型性

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

連結到以下論文：Luca Cardelli: On Understanding Types, Data Abstraction, and Polymorphism.

`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 關鍵字的新簽名的縮寫^[1]。也就是說，編譯器會在內部為您插入任何缺失的 forall。另一個例子：fst 的型別簽名實際上是

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

或等效地

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

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

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

這種概念，即某些東西適用於所有型別或對所有事物都成立，被稱為全稱量化。在數學邏輯中，符號 ∀^[2]（一個倒置的 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 這樣的簡單多型函式被稱為具有rank-1 型別，而型別 foo 被歸類為rank-2 型別。一般而言，rank-n 型別是至少有一個 rank-(n-1) 引數但沒有更高秩引數的函式。

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

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

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

`runST`

對於實際的 Haskell 程式設計師來說，ST 單子可能是現實中 rank-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

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

重點是可變引用應該在單個 runST 中是區域性的。例如，

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

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

您可以在原始論文 Lazy functional state threads^[4] 中找到對 ST 單子的更詳細解釋。

非預言性

predicative = 型別變數被例項化為monotypes。impredicative = 也稱為polytypes。例如：length [id :: forall a . a -> a] 或 Just (id :: forall a. a -> a)。與高階型別略有不同。

透過其通用性來關聯多型型別，即 isInstanceOf。
haskell-cafe：RankNTypes 簡要說明。

有界引數多型性

型別類

待辦事項

System F

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

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

示例

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

Church 數，任意遞迴型別的編碼（正性條件）：&forall x. (F x -> x) -> x
Continuation，模式匹配：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 中的多型性及其相關內容。

自由定理

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

引數多型性的自由定理。

備註

↑ 請注意，關鍵字 forall 不是 Haskell 98 標準的一部分，但任何語言擴充套件 ScopedTypeVariables、Rank2Types 或 RankNTypes 都將在編譯器中啟用它。未來的 Haskell 標準將包含其中之一。
↑ UnicodeSyntax 擴充套件允許您在 Haskell 原始碼中使用符號 ∀ 代替 forall 關鍵字。
↑ 或者，如果您只想使用 rank-2 型別，則只需啟用 Rank2Types。
↑ John Launchbury (1994-??-??). "Lazy functional state threads". ACM Press": 24–35. {{cite journal}}: Cite journal requires |journal= (help); Check date values in: |date= (help); Unknown parameter |coauthor= ignored (|author= suggested) (help)