什麼是GADT？它有什麼作用？

Wiki 來來回回看了好多次，還是不太明了。

歡迎訪問我的博客：什麼是 GADT（廣義代數數據類型）？

先看看沒有 GADT 的時候我們在做啥。最簡單的，比如定義一個列表：

List a = Nil | Cons a (List a)


它是在做啥呢？

• 先看等號左邊，它首先定義了一個叫 List 的 type constructor，它接受一個類型，並返回一個新的類型。其實就是類型的函數。
• 再看右邊，它告訴我們有兩種方式獲得一個類型為 List a 的值，一個叫 Nil，一個叫 Cons a (List a)。
• Nil 的話，你直接寫 Nil，它就是一個 List a 類型的值，至於這個 a 具體是啥，需要結合上下文推導才知道。
• 而 Cons a (List a) 呢，它是接受兩個參數，一個類型是 a，一個類型是 List a，然後返回一個 List a 類型的值。至於這個 a 是啥，我們同樣是需要推導才能知道的，不過是這裡的推導比較顯著罷了，因為直接就是第一個參數的類型。

那麼我們可以用函數形式給這倆表示出來：

Nil :: List a
Cons :: a -&> List a -&> List a


可以看到它們接受一些參數，但返回類型都是 List a。GADT 唯一改的就是返回類型這個地方，我們不一定必須寫 a，而是可以把 a 替換為另外的類型。比如說我們可以有一個只能作為 Int 列表的頭的構造函數：

IntNil :: List Int


我們可以試驗一下（這個就是 GADT 的寫法了）：

data List a where
IntNil :: List Int
Nil :: List a
Cons :: a -&> List a -&> List a

-- 這個就是相容的
c :: List Char
c = Nil


當然左邊不一定得是 List Int 這樣直白的類型，只要是一個形如 List 的類型就可以了，你甚至可以把自己嵌套進去：

data Pair a b where Pair :: a -&> b -&> Pair a b

data List a where IntListNil :: List (List Int)
ListNil :: List (List a)
IntNil :: List Int
Nil :: List a
Cons :: a -&> List a -&> List a
-- 這個就不行，因為形如 Pair 而不是 List
-- Bad :: a -&> List a -&> Pair a (List a)


那麼它可以幹啥用呢？我所知道的有這麼一些（都不超出網上的 wiki 的範疇）：

一種就是最有名的，嵌入一種語言（的語法樹）。比如這麼一種簡單的表達式語言：

data Expr =
ILit Int
| BLit Bool
| Add Expr Expr
| Eq Expr Expr


這樣是足夠表達了，但是存在一些問題——比如我們不希望 Bool 被 Add（就是說我們要嵌入的語言，它本身也是有類型的，有些運算不能對某些對象做），但這個定義無法避免我們寫：

addBool :: Expr
addBool = Add (BLit True) (BLit False)


一個想法是把這個 Expr 的「返回值」類型記錄下來，就像我們對 List 做的那樣（在那裡我們記錄的是成員類型）：

data Expr a =
ILit Int
| BLit Bool
| Add (Expr Int) (Expr Int)
| Eq (Expr a) (Expr a)


這個看起來很美好，但是行不行呢？

實際上是不行的！你不要以為 BLit True 就是 Expr Bool 類型，從而會不能作為 Add 的參數了。其實，這裡的 BLit True 還是 Expr a 類型，其中 a 是任意類型，就像之前的 Nil 是 List a 類型、a 是任意的一樣。

這個時候就體現出 GADT 的重要性了——只有透過 GADT 才能限定一個「構造函數」的返回類型：

data Expr a where
ILit :: Int -&> Expr Int
BLit :: Bool -&> Expr Bool
Add :: Expr Int -&> Expr Int -&> Expr Int
-- 對 Eq 我們可以放寬要求，只用 typeclass 來限制，不必指定具體類型
Eq :: Eq a =&> Expr a -&> Expr a -&> Expr Bool


這時候它就能分辨是非了：

-- 報錯，因為 Expr Bool 和 Expr Int 不兼容
-- addBool = Add (BLit True) (BLit False)
addInt = Add (ILit 1) (ILit 2)
eqBool = Eq (BLit True) (BLit False)


很美妙，是不是？

這就是所謂的 initial embedding of a language，而我們最後得到的用 GADT 的版本，叫 tagless initial embedding。為什麼是 tagless 呢？因為原始的 ADT 是所謂的 「tagged union」。我們現在拋棄了它，所以叫 tagless。

這個 Expr 是很簡單的語言。實際上你完全可以將 simply typed lambda calculus 給這樣嵌入進去。

相對於 initial embedding，我們還可以有所謂 final embedding，不過跟 GADT 關係不大了。

我們還可以玩點更風騷的。比如這裡假如有一種簡單的、描述棧操作的語言，Push 表示推入一個數，Add 表示彈出兩個數，把它們的和推回去：

data StackLang where
Begin :: StackLang
Push :: Int -&> StackLang -&> StackLang
Add :: StackLang -&> StackLang

bug = Add (Push 1 Begin)


這裡的 bug 語句實際上是有 bug 的，因為你剛推進去一個 1，沒有人和它相加。那麼能不能從類型層面來消除這種 bug呢？

我們想，要是 StackLang 的類型裡面，帶上棧里有多少個數該多好啊！但是這時候 Begin 就不能返回一般的 StackLang 類型了，而是帶有 0 個數的 StackLang 類型，同理，Push 接受帶有 n 個數的 StackLang 類型，返回帶有 n+1 個數的 StackLang 類型，Add 則是 n+2 -&> n+1。此時 GADT 就可以派上用場了：

data Z
data S n

data SStackLang t where
SBegin :: SStackLang Z
SPush :: Int -&> SStackLang t -&> SStackLang (S t)
SAdd :: SStackLang (S (S t)) -&> SStackLang (S t)


這裡 Z 和 S 就是對自然數的 0 和後繼（successor）的模擬。這時候你會發現：

sBug = SAdd (SPush 1 SBegin)


會報錯

? Couldn』t match type 『Z』 with 『S t』

Expected type: SStackLang (S (S t))

Actual type: SStackLang (S Z)

非常安全。

其實這就是對所謂的「依賴類型」(dependent type) 的模擬。仿照這個你還可以造出「長度為 n」的列表的概念，並對其定義安全的操作。這就是後話了。

GADT 還可以把 type 轉化為 value。把類型保存在一個值里，本來你固然是可以：

data Witness a = Witness a


但這樣你得提供一個 a 類型的值才能把類型記錄進去。一方面很多時候沒法構造這個值，另一方面可能有的類型就沒有值，最後要求提供值的做法根本就是不科學的。

但是有 GADT 你就可以為所欲為——我不一定要接受一個值，才能得到這個類型了：

data Witness a where
IntWitness :: Witness Int
BoollWitness :: Witness Bool


這就是所謂的 「type witness」。至於這個有什麼用，怎麼用，為什麼要這麼用，（待續）。

少上知乎多看書，剛剛編譯出爐的。『

如果你學過C++的話，那大部分都是再說怎麼在Haskell裡面表達template&然後做偏特化這樣的事情。