OCaml的 - GADT - 布爾表達式

Question

我想知道是否有有這樣的一些方法：

​​

這裏的問題是，我不能定義BinOp兩次，而我想這取決於參數類型。 PS：「canonical」的意思是「包含在表達式中的n個變量用範圍從0到（n-1）的整數」表示。這是一個不變的，我需要強制我的一些職能。

Answer 1

你必須給出類型constuctors不同的名稱，因爲有些情況下gadt確實表現得像adt的情況。

讓我們假設你想定義你的類型如下：

type 'canonical boolean_expression = 
    | Bool : bool -> canonical boolean_expression (* here I assume that you wanted to have that case too *) 
    | Var : int -> not_canonical boolean_expression 
    | Not : 'canonical boolean_expression -> 'canonical boolean_expression 
    | BinOpC : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression 
    | BinOpNC : _ boolean_expression * binary_operator * _ boolean_expression -> not_canonical boolean_expression 
;; 

現在考慮類型稍作修改：

type 'canonical boolean_expression = 
    | Bool : bool -> canonical boolean_expression 
    | Var : int -> not_canonical boolean_expression 
    | Not : 'canonical boolean_expression -> 'canonical boolean_expression 
    | BinOpC : canonical boolean_expression * binary_operator * canonical boolean_expression -> canonical boolean_expression 
    | BinOpNC : 'a boolean_expression * binary_operator * 'a boolean_expression -> 'a boolean_expression 
;; 

現在，你可以用二進制操作結束canonical boolean_expression使用最後兩個構造函數中的任何一個。顯然，通過任意選擇結果值的類型而獲得的自由具有其後果：您可以創建具有重疊「類型案例」的gad具。這樣做時，任何採用這些值的函數都必須測試這兩種情況。因此，構造函數的名稱不能相同，因爲類型可能不足以知道我們正在處理的值。

例如，下面的功能：

let rec compute = function 
    | Bool b -> b 
    | BinOpC (a,And,b) -> compute a && compute b 
    | BinOpC (a,Or,b) -> compute a || compute b 
;; 

給你的定義，應進行類型檢查和照顧規範表述的沒有問題。通過我的修改，編譯器會正確地抱怨BinOpNC也可能包含canonical表達式。

這似乎是一個愚蠢的例子（的確是它）揭露這方面的問題，因爲我修改後的布爾表達式的定義明顯不正確（語義上講），但編譯器不關心類型的實用含義。

從本質上講，gadt仍然是adt，因爲你仍然可以發現情況是你必須依靠構造函數來選擇正確的行爲。