第 7 章 廣義代數資料型態

廣義代數資料型態，或稱 GADT，以兩種方式擴展了常見的總和型態：型態參數的約束可能會根據數值建構子而改變，並且某些型態變數可能會以存在量化的方式存在。添加約束是透過給定一個明確的回傳型態來完成的，其中型態參數被實例化。

type _ term = | Int : int -> int term | Add : (int -> int -> int) term | App : ('b -> 'a) term * 'b term -> 'a term

此回傳型態必須使用與正在定義的型態相同的型態建構子，並且具有相同數量的參數。當變數出現在建構子的參數中，但未出現在其回傳型態中時，變數會成為存在變數。由於使用回傳型態通常不需要在型態定義的左側命名型態參數，因此在這種情況下，可以使用匿名型態 _ 來取代它們。

與每個建構子相關聯的約束可以透過模式匹配來恢復。也就是說，如果模式匹配的檢視值的型態包含局部抽象型態，則可以根據所使用的建構子來細化此型態。這些額外的約束僅在模式匹配的相應分支內有效。如果建構子具有一些存在變數，則會產生新的局部抽象型態，並且它們不得超出此分支的範圍。

1 遞迴函式

我們撰寫一個 eval 函式

let rec eval : type a. a term -> a = function | Int n -> n (* a = int *) | Add -> (fun x y -> x+y) (* a = int -> int -> int *) | App(f,x) -> (eval f) (eval x) (* eval 在型態 (b->a) 和 b 上呼叫，以獲得新的 b *)

並使用它

let two = eval (App (App (Add, Int 1), Int 1))
val two : int = 2

重要的是要注意，函式 eval 正在使用局部抽象型態的多型語法。定義操作 GADT 的遞迴函式時，通常應使用明確的多型遞迴。例如，以下定義會產生型態錯誤

let rec eval (type a) : a term -> a = function | Int n -> n | Add -> (fun x y -> x+y) | App(f,x) -> (eval f) (eval x)
錯誤: 此表達式的型態為 ($b -> a) term，但預期表達式的型態為 'a。型態建構子 $b 會超出其範圍。提示：$b 是由建構子 App 綁定的存在型態。

在沒有明確的多型註釋的情況下，會為遞迴函式推論單型型態。如果在函式定義內以涉及存在 GADT 型態變數的型態發生遞迴呼叫，則此變數會流向遞迴函式的型態，因此會超出其範圍。在上面的範例中，當以 f 作為參數呼叫 eval 時，會在分支 App(f,x) 中發生這種情況。在此分支中，f 的型態為 ($App_'b -> a) term。$App_'b 中的前綴 $ 表示編譯器命名的存在型態 (請參閱 ‍7.5)。由於 eval 的型態為 'a term -> 'a，因此呼叫 eval f 會使存在型態 $App_'b 流向型態變數 'a 並超出其範圍。這會觸發上述錯誤。

2 型態推論

GADT 的型態推論眾所周知地困難。這是因為某些型態在超出分支時可能會變得模糊不清。例如，在上面的 Int 情況下，n 的型態可以是 int 或 a，並且它們在該分支之外並不等效。作為第一種近似，如果模式匹配標註的型態不包含自由型態變數（檢視值和回傳型態），則型態推論始終有效。由於包含的型態註釋僅包含局部抽象型態，因此上面的範例就是這種情況。

在實務上，型態推論比這更聰明一點：型態註釋不需要立即位於模式匹配上，並且型態不必始終是封閉的。因此，通常只需像上面的範例一樣註釋函式即可。型態註釋會以兩種方式傳播：對於檢視值，它們會遵循型態推論的流程，其方式類似於多型方法；對於回傳型態，它們會遵循程式的結構，它們會分割函式、傳播到模式匹配的所有分支，並穿過元組、記錄和總和型態。此外，所使用的模糊概念更強：只有當型態與不相容的型態混合（由約束等化），且它們之間沒有型態註釋時，才會將型態視為模糊。例如，以下程式碼會正確輸入。

let rec sum : type a. a term -> _ = fun x -> let y = match x with | Int n -> n | Add -> 0 | App(f,x) -> sum f + sum x in y + 1
val sum : 'a term -> int = <fun>

在這裡，回傳型態 int 永遠不會與 a 混合，因此它被視為非模糊的，並且可以推斷出來。當使用此類部分型態註釋時，我們強烈建議指定 -principal 模式，以檢查推論是否為主導。

窮舉性檢查會知道 GADT 的約束，並且可以自動推斷出某些情況不會發生。例如，以下模式匹配會被正確地視為窮舉 (不會發生 Add 情況)。

let get_int : int term -> int = function | Int n -> n | App(_,_) -> 0

3 反駁情況

通常，窮舉性檢查僅嘗試檢查模式匹配中省略的情況是否可輸入。但是，您可以透過添加以句點寫成的反駁情況來強制其更加努力地嘗試。在存在反駁情況時，窮舉性檢查會首先計算模式與其先前情況的補集的交集。然後，它會嘗試透過型態檢查來檢查產生的模式是否真的可以匹配任何具體的值。產生模式中的萬用字元會以特殊方式處理：如果它們的型態是僅具有 GADT 建構子的變體型態，則該模式會分割成不同的建構子，以便檢查它們中的任何一個是否有可能 (為了避免非終止，此分割不會針對這些建構子的參數執行)。我們還分割了僅具有一個情況的元組和變體型態，因為它們可能在內部包含 GADT。例如，以下程式碼會被視為窮舉

type _ t = | Int : int t | Bool : bool t let deep : (char t * int) option -> char = function | None -> 'c' | _ -> .

也就是說，推斷的剩餘情況是 Some _，它會分割成 Some (Int, _) 和 Some (Bool, _)，它們都不可輸入，因為 deep 期望一個不存在的 char t 作為元組的第一個元素。請注意，這裡可以省略反駁情況，因為當模式匹配中只有一種情況時，它會自動添加。

另一個新增功能是，冗餘檢查現在知道 GADT：如果可以使用相同的模式透過反駁情況取代情況，則會將其偵測為冗餘。

4 進階範例

我們在上面定義的 term 型態是一種索引型態，其中型態參數反映了數值內容的屬性。GADT 的另一個用途是單例型態，其中 GADT 值恰好代表一種型態。此值可以用作此型態的執行時間表示，並且接收它的函式可以具有多型行為。

以下是一個多型函式的範例，該函式採用某種型態 t 的執行時間表示和相同型態的值，然後將該值以字串形式漂亮地列印出來

type _ typ = | Int : int typ | String : string typ | Pair : 'a typ * 'b typ -> ('a * 'b) typ let rec to_string: type t. t typ -> t -> string = fun t x -> match t with | Int -> Int.to_string x | String -> Printf.sprintf "%S" x | Pair(t1,t2) -> let (x1, x2) = x in Printf.sprintf "(%s,%s)" (to_string t1 x1) (to_string t2 x2)

GADT 的另一個常見應用是相等見證。

type (_,_) eq = Eq : ('a,'a) eq let cast : type a b. (a,b) eq -> a -> b = fun Eq x -> x

這裡型態 eq 只有一個建構子，透過在它上面進行匹配，可以添加局部約束，從而允許在 a 和 b 之間進行轉換。透過建立此類相等見證，可以使語法上不同的型態相等。

以下是一個使用單例型態和相等見證來實作動態型態的範例。

let rec eq_type : type a b. a typ -> b typ -> (a,b) eq option = fun a b -> match a, b with | Int, Int -> Some Eq | String, String -> Some Eq | Pair(a1,a2), Pair(b1,b2) -> begin match eq_type a1 b1, eq_type a2 b2 with | Some Eq, Some Eq -> Some Eq | _ -> None end | _ -> None type dyn = Dyn : 'a typ * 'a -> dyn let get_dyn : type a. a typ -> dyn -> a option = fun a (Dyn(b,x)) -> match eq_type a b with | None -> None | Some Eq -> Some x

5 錯誤訊息中的存在型別名稱

在存在 GADT 的情況下，模式匹配的型別推導可能會產生許多存在型別。必要時，錯誤訊息會使用編譯器產生的名稱來指稱這些存在型別。目前，編譯器會根據以下命名慣例產生這些名稱

如最後一項所示，目前行為並不完善，未來版本可能會改進。

6 存在型別的明確命名

如上所述，對 GADT 建構子進行模式匹配可能會引入存在型別。已引入語法，允許明確命名它們。例如，以下程式碼命名 f 參數的型別，並使用這個名稱。

type _ closure = Closure : ('a -> 'b) * 'a -> 'b closure let eval = fun (Closure (type a) (f, x : (a -> _) * _)) -> f (x : a)

建構子的所有存在型別變數必須由 (type ...) 建構子引入，並由建構子參數外部的型別註釋綁定。

7 非局部抽象型別的方程式

GADT 模式匹配也可能會將型別方程式新增至非局部抽象型別。其行為與局部抽象型別相同。重新使用上述 eq 型別，可以寫成

module M : sig type t val x : t val e : (t,int) eq end = struct type t = int let x = 33 let e = Eq end let x : int = let Eq = M.e in M.x

當然，並非所有抽象型別都可以被精煉，因為這會與窮盡性檢查相矛盾。也就是說，內建模組（由編譯器本身定義的那些，例如 int 或 array），以及由局部模組定義的抽象型別，是不可實例化的，因此會導致型別錯誤，而不是引入方程式。

Copyright © 2024 Institut National de Recherche en Informatique et en Automatique