Haskell/GADT

型別樂趣

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

廣義代數資料型別，或簡稱為 GADT，是您熟悉的代數資料型別的推廣。基本上，它們允許您明確寫下建構函式的型別。在本章中，您將學習為什麼這很有用以及如何宣告您自己的 GADT。

我們從構建一個簡單的嵌入式領域特定語言 (EDSL) 的例子開始，該語言用於簡單的算術表示式，它可以透過 GADT 更穩固地構建。接下來是 GADT 語法概述，以及更簡單的說明，以及不同的應用來構建安全列表型別，其中 head [] 的等效操作無法進行型別檢查，因此不會出現通常的執行時錯誤：*** Exception: Prelude.head: empty list。

理解 GADT

那麼，什麼是 GADT 以及它們有什麼用？GADT 主要用於實現領域特定語言，因此本節將透過相應的例子來介紹它們。

算術表示式

讓我們考慮一個用於算術表示式的簡單語言，它由以下資料型別給出

data Expr = I Int         -- integer constants
          | Add Expr Expr -- add two expressions
          | Mul Expr Expr -- multiply two expressions

換句話說，該資料型別對應於抽象語法樹，類似於 (5+1)*7 這樣的算術項將表示為 (I 5 `Add` I 1) `Mul` I 7 :: Expr。

給定抽象語法樹，我們希望對其做些什麼；我們希望編譯它，最佳化它等等。首先，讓我們編寫一個評估函式，它接受一個表示式並計算它所表示的整數值。定義很簡單

eval :: Expr -> Int
eval (I n)       = n
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2

擴充套件語言

現在，假設我們希望將我們的語言擴充套件為除了整數之外的其他型別。例如，假設我們希望表示相等性測試，因此我們也需要布林值。我們擴充套件了 Expr 型別，使其變為

data Expr = I Int
          | B Bool           -- boolean constants
          | Add Expr Expr
          | Mul Expr Expr
          | Eq  Expr Expr    -- equality test

項 5+1 == 7 將表示為 (I 5 `Add` I 1) `Eq` I 7。

與之前一樣，我們希望編寫一個函式 eval 來評估表示式。但是這次，表示式現在可以表示整數或布林值，我們必須在返回型別中捕獲這一點

eval :: Expr -> Either Int Bool

前兩種情況很簡單

eval (I n) = Left n
eval (B b) = Right b

但是現在我們遇到了麻煩。我們希望編寫

eval (Add e1 e2) = eval e1 + eval e2  -- ???

但這無法進行型別檢查：加法函式 + 期望兩個整型引數，但 eval e1 的型別為 Either Int Bool，我們需要從中提取 Int。

更糟糕的是，如果 e1 實際上表示一個布林值 會怎樣？以下是一個有效的表示式

B True `Add` I 5 :: Expr

但很明顯，它沒有意義；我們不能將布林值加到整數！換句話說，評估可能會返回整數或布林值，但也可能失敗，因為表示式沒有意義。我們必須將這一點納入返回型別

eval :: Expr -> Maybe (Either Int Bool)

現在，我們可以很好地編寫這個函式，但這仍然不令人滿意，因為我們真正想要做的是讓 Haskell 的型別系統排除任何無效表示式；我們不想在解構抽象語法樹時自己檢查型別。

練習：儘管有我們的目標，但實現 eval 函式可能仍然具有指導意義；請執行此操作。

起點

data Expr = I Int
        | B Bool           -- boolean constants
        | Add Expr Expr
        | Mul Expr Expr
        | Eq  Expr Expr    -- equality test

eval :: Expr -> Maybe (Either Int Bool)
-- Your implementation here.

幽靈型別

所謂的幽靈型別是我們目標的第一步。這種技術是為 Expr 新增一個型別變數，使其變為

data Expr a = I Int
            | B Bool
            | Add (Expr a) (Expr a)
            | Mul (Expr a) (Expr a)
            | Eq  (Expr a) (Expr a)

注意，表示式 Expr a 根本不包含值 a；這就是為什麼 a 被稱為幽靈型別，它只是一個虛擬變數。將其與列表 [a] 相比較，列表 [a] 確實包含一堆 a。

關鍵思想是我們將使用 a 來跟蹤表示式的型別。而不是讓建構函式

Add :: Expr a -> Expr a -> Expr a

可供我們小型語言的使用者使用，我們將只提供一個型別更受限制的智慧建構函式

add :: Expr Int -> Expr Int -> Expr Int
add = Add

實現方式相同，但型別不同。對其他建構函式也這樣做，

i :: Int  -> Expr Int
i = I
b :: Bool -> Expr Bool
b = B

之前有問題的表示式

b True `add` i 5

不再進行型別檢查！畢竟，第一個引數的型別為 Expr Bool，而 add 期望一個 Expr Int。換句話說，幽靈型別 a 標記了表示式的預期型別。透過只匯出智慧建構函式，使用者無法建立型別不正確的表示式。

與之前一樣，我們希望實現一個評估函式。使用我們新的標記 a，我們可能希望賦予它以下型別

eval :: Expr a -> a

並像這樣實現第一個案例。

eval (I n) = n

但遺憾的是，這行不通：編譯器如何知道遇到建構函式I意味著a = Int？當然，對於使用者在我們的語言中建立的所有表示式來說，情況將如此，因為他們只被允許使用智慧建構函式。但從內部來說，像

I 5 :: Expr String

這樣的表示式仍然是有效的。事實上，正如你所看到的，a甚至不必是Int或Bool，它可以是任何東西。

我們需要一種方法來限制建構函式本身的返回型別，而這正是泛型資料型別所做的事情。

GADTs

要啟用此語言特性，請在檔案開頭新增{-# LANGUAGE GADTs #-}。

限制建構函式型別的明顯表示法是寫下它的型別，而這正是 GADTs 的定義方式。

data Expr a where
    I   :: Int  -> Expr Int
    B   :: Bool -> Expr Bool
    Add :: Expr Int -> Expr Int -> Expr Int
    Mul :: Expr Int -> Expr Int -> Expr Int
    Eq  :: Eq a => Expr a -> Expr a -> Expr Bool

換句話說，我們只需列出所有建構函式的型別簽名。特別是，標記型別a根據我們的需要專門化為Int或Bool，就像我們對智慧建構函式所做的那樣。

而 GADTs 的偉大之處在於我們現在可以實現一個利用型別標記的評估函式。

eval :: Expr a -> a
eval (I n) = n
eval (B b) = b
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq  e1 e2) = eval e1 == eval e2

特別是在第一個案例中

eval (I n) = n

編譯器現在能夠推斷出當我們遇到建構函式I時a=Int，並且返回n :: Int是合法的；其他案例也是如此。

總而言之，GADTs 允許我們限制建構函式的返回型別，從而使我們能夠利用 Haskell 的型別系統來實現我們的領域特定語言。因此，我們可以實現更多的語言，並且它們的實現變得更簡單。

摘要

語法

以下是關於宣告 GADTs 語法的快速摘要。

首先，考慮以下普通代數資料型別：熟悉的List和Maybe型別，以及一個簡單的樹型別RoseTree。

Maybe	List	Rose Tree
data Maybe a = Nothing \| Just a	data List a = Nil \| Cons a (List a)	data RoseTree a = RoseTree a [RoseTree a]

請記住，這些宣告引入的建構函式既可以用於模式匹配來解構值，也可以用作函式來構建值。（Nothing和Nil是具有“零個引數”的函式。）我們可以問一下後者是什麼型別。

Maybe	List	Rose Tree
> :t Nothing Nothing :: Maybe a > :t Just Just :: a -> Maybe a	> :t Nil Nil :: List a > :t Cons Cons :: a -> List a -> List a	> :t RoseTree RoseTree :: a -> [RoseTree a] -> RoseTree a

很明顯，關於Maybe、List和RoseTree建構函式的型別資訊等同於我們在最初宣告資料型別時提供給編譯器的資訊。換句話說，也可以透過簡單地列出所有建構函式的型別來宣告資料型別，而這正是 GADT 語法所做的。

Maybe	List	Rose Tree
data Maybe a where Nothing :: Maybe a Just :: a -> Maybe a	data List a where Nil :: List a Cons :: a -> List a -> List a	data RoseTree a where RoseTree :: a -> [RoseTree a] -> RoseTree a

此語法可以透過語言選項{-#LANGUAGE GADTs #-}使用。它應該很熟悉你，因為它與型別類宣告的語法非常相似。如果你習慣於將建構函式視為函式，那麼它也很容易記住。每個建構函式都由一個型別簽名定義。

新可能性

請注意，當我們詢問GHCi關於Nothing和Just的型別時，它返回了Maybe a和a -> Maybe a作為型別。在這些情況下以及其他情況下，與建構函式相關的函式的最終輸出型別是我們最初定義的型別 - Maybe a、List a或RoseTree a。總的來說，在標準 Haskell 中，Foo a的建構函式函式具有Foo a作為它們的最終返回型別。如果新語法與舊語法嚴格等效，那麼我們必須對它的使用進行此限制以進行有效的型別宣告。

那麼 GADTs 為我們添加了什麼？能夠精確控制你返回的Foo型別。使用 GADTs，Foo a的建構函式不必返回Foo a；它可以返回你能想到的任何Foo blah。例如，在下面的程式碼示例中，MkTrueGadtFoo建構函式返回一個TrueGadtFoo Int，即使它是針對型別TrueGadtFoo a的。

示例：GADT 讓你有更多控制權

data FooInGadtClothing a where
 MkFooInGadtClothing :: a -> FooInGadtClothing a

--which is no different from:  data Haskell98Foo a = MkHaskell98Foo a ,

--by contrast, consider:
 
data TrueGadtFoo a where
  MkTrueGadtFoo :: a -> TrueGadtFoo Int

--This has no Haskell 98 equivalent.

但請注意，你只能進行如此遠的泛化...如果你要宣告的資料型別是Foo，那麼建構函式函式必須返回某種Foo。返回任何其他東西根本行不通。

示例：試試這個。它行不通

data Bar where
  BarNone :: Bar -- This is ok

data Foo where
  MkFoo :: Bar Int-- This will not typecheck

示例

安全的列表

先決條件：我們假設在本節中你瞭解列表在函式式語言中是如何表示的

注意：本節中的示例還要求啟用副檔名 EmptyDataDecls 和 KindSignatures

我們現在已經瞭解了 GADT 語法賦予我們的額外控制權。唯一的新事物是你可以精確控制返回的資料結構型別。現在，我們能用它來做什麼呢？考慮一下簡單的 Haskell 列表。當你呼叫head []時會發生什麼？Haskell 會崩潰。你是否曾經希望有一個神奇的head版本，它只接受至少包含一個元素的列表，在這些列表上它永遠不會崩潰？

首先，讓我們定義一個新型別SafeList x y。我們的想法是擁有類似於普通 Haskell 列表[x]的東西，但在型別中包含一些額外的資訊。此額外資訊（型別變數y）告訴我們列表是否為空。空列表表示為SafeList x Empty，而非空列表表示為SafeList x NonEmpty。

-- we have to define these types
data Empty
data NonEmpty

-- the idea is that you can have either 
--    SafeList a Empty
-- or SafeList a NonEmpty
data SafeList a b where
-- to be implemented

由於我們有此額外資訊，我們現在可以僅對非空列表定義一個函式safeHead！在空列表上呼叫safeHead將簡單地拒絕型別檢查。

safeHead :: SafeList a NonEmpty -> a

那麼既然我們知道我們想要什麼，即safeHead，我們如何實際獲得它呢？答案是 GADT。關鍵是我們利用 GADT 特性返回兩種不同的a型別列表，對於Nil建構函式，返回SafeList a Empty，而對於Cons建構函式，則返回SafeList a NonEmpty。

data SafeList a b where
  Nil  :: SafeList a Empty
  Cons :: a -> SafeList a b -> SafeList a NonEmpty

如果沒有 GADT，這是不可能的，因為我們所有的建構函式都必須返回相同型別的列表；而使用 GADT，我們現在可以使用不同的建構函式返回不同型別的列表。無論如何，讓我們將所有這些內容整合在一起，以及SafeHead的實際定義。

示例：透過 GADT 實現安全的列表

{-#LANGUAGE GADTs, EmptyDataDecls #-}
-- (the EmptyDataDecls pragma must also appear at the very top of the module,
-- in order to allow the Empty and NonEmpty datatype declarations.)

data Empty
data NonEmpty

data SafeList a b where
     Nil :: SafeList a Empty
     Cons:: a -> SafeList a b -> SafeList a NonEmpty

safeHead :: SafeList a NonEmpty -> a
safeHead (Cons x _) = x

將此列表複製到一個檔案中，並在ghci -fglasgow-exts中載入。你應該注意到以下區別，分別在非空列表和空列表上呼叫safeHead。

示例：safeHead是...安全的

Prelude Main> safeHead (Cons "hi" Nil)
"hi"
Prelude Main> safeHead Nil

<interactive>:1:9:
    Couldn't match `NonEmpty' against `Empty'
      Expected type: SafeList a NonEmpty
      Inferred type: SafeList a Empty
    In the first argument of `safeHead', namely `Nil'
    In the definition of `it': it = safeHead Nil

這個抱怨是件好事：這意味著我們現在可以在編譯時確保是否在適當的列表上呼叫safeHead。但是，這也為潛在的風險設定了一個陷阱。考慮以下函式。你認為它的型別是什麼？

示例：GADTs 的問題

silly False = Nil
silly True  = Cons () Nil

現在嘗試在 GHCi 中載入該示例。你會注意到以下抱怨。

示例：GADTs 的問題 - 抱怨

Couldn't match `Empty' against `NonEmpty'
     Expected type: SafeList () Empty
     Inferred type: SafeList () NonEmpty
   In the application `Cons () Nil'
   In the definition of `silly': silly True = Cons () Nil

silly定義中的案例評估為不同型別的標記列表，導致型別錯誤。透過 GADT 強加的額外約束，函式無法同時生成空列表和非空列表。

如果我們真的想定義silly，我們可以透過放鬆Cons的型別來實現，以便它可以構建安全的列表和不安全的列表。

示例：另一種方法

{-#LANGUAGE GADTs, EmptyDataDecls, KindSignatures #-}
-- here we add the KindSignatures pragma,
-- which makes the GADT declaration a bit more elegant.

-- Note the subtle yet revealing change in the phantom type names.
data NotSafe
data Safe


data MarkedList             ::  * -> * -> * where
  Nil                       ::  MarkedList t NotSafe
  Cons                      ::  a -> MarkedList a b -> MarkedList a c


safeHead                    ::  MarkedList a Safe -> a
safeHead (Cons x _)          =  x

-- This function will never produce anything that can be consumed by safeHead,
-- no matter that the resulting list is not necessarily empty.
silly                       :: Bool -> MarkedList () NotSafe
silly False                  =  Nil
silly True                   =  Cons () Nil

上面的修復有一個代價：透過放鬆Cons的約束，我們放棄了它無法生成空列表的知識。根據我們最初版本的安全列表，例如，我們可以定義一個函式，它接受一個SafeList a Empty引數，並確保Cons產生的任何東西都不會被它接受。對於類似的MarkedList a NotSafe，情況並非如此；可以說，該型別正是因為它限制性較小而用途較小。雖然在這個例子中，問題可能看起來很小，因為空列表的作用不大，但總的來說，值得考慮。

練習
你能實現一個`safeTail`函式嗎？這裡介紹的兩個版本都可以作為有效的起點，以及其他類似的變體。

一個簡單的表示式求值器

插入 Wobbly Types 論文中使用的示例...我認為這很有教學意義。

本教程的第一部分已經涵蓋了這一點。

討論

更多示例、思考

我依稀記得在 2006 年的 FOSDEM 上，GADT 與以下內容之間存在某種關係...什麼？

幽靈型別

請參閱幻影型別。

存在型別

如果你喜歡存在量化的型別，你可能想注意到它們現在被 GADT 包含了。正如 GHC 手冊所說，以下兩個型別宣告給你同樣的東西。

data TE a = forall b. MkTE b (b->a)
data TG a where { MkTG :: b -> (b->a) -> TG a }

見證型別

GADT

練習解答

型別樂趣

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

編輯本章

Haskell

Haskell 基礎 >> 基礎 Haskell >> 中級 Haskell >> 單子
 高階 Haskell >> 型別玩樂 >> 更廣闊的理論 >> Haskell 效能

庫參考 >> 通用實踐 >> 專門任務

編輯書籍結構