GADTs

傳統的代數資料型別在其型別變數中是引數化的。例如，如果我們定義 ADT 之類的

data Expr a = IntLit Int 
            | BoolLit Bool 
            | If (Expr Bool) (Expr a) (Expr a)

希望這將靜態排除非良好型別的條件，這將不會像預期的那樣表現，因為 IntLit::Int -> Expr a 的型別是普遍量化的：對於 a 的任何選擇，它產生 Expr a 型別的值。特別是對於 a ~ Bool，我們有 IntLit::Int -> Expr Bool，允許我們構造類似 If (IntLit 1) e1 e2 的東西，這是 If 建構函式試圖排除的型別。

廣義代數資料型別允許我們控制資料建構函式的結果型別，使它們不僅僅是引數化的。我們可以像這樣重寫我們的 Expr 型別作為 GADT：

data Expr a where
  IntLit::Int -> Expr Int
  BoolLit::Bool -> Expr Bool
  If::Expr Bool -> Expr a -> Expr a -> Expr a

這裡，建構函式 IntLit 的型別是 Int -> Expr Int，因此 IntLit 1 :: Expr Bool 不會進行型別檢查。

GADT 值上的模式匹配會導致返回的術語型別的細化。例如，可以為 Expr a 編寫一個評估器，如下所示：

crazyEval::Expr a -> a
crazyEval (IntLit x) = 
   -- Here we can use `(+)` because x::Int
   x + 1 
crazyEval (BoolLit b) = 
   -- Here we can use `not` because b::Bool
   not b
crazyEval (If b thn els) = 
  -- Because b::Expr Bool, we can use `crazyEval b::Bool`.
  -- Also, because thn::Expr a and els::Expr a, we can pass either to 
  -- the recursive call to `crazyEval` and get an a back
  crazyEval $ if crazyEval b then thn else els 

請注意，我們可以在上面的定義中使用 (+)，因為當 IntLit x 模式匹配時，我們也會知道 a ~ Int（同樣對於 not 和 if_then_else_ 當 a ~ Bool）。