封裝GADT模式

Question

在這種code存在重複片段相匹配：

insert x (AATree t) = case insert' x t of 
    Same t -> AATree t 
    Inc t -> AATree t 

insertBlack :: (Ord a) => a -> AANode Black (Succ n) a -> AnyColor (Succ n) a 
insertBlack x (Black l y r) 
    | x < y  = case insert' x l of 
      Same l' -> AnyColor $ Black l' y r 
      Inc l' -> AnyColor $ skew l' y r 
    | otherwise = case insert' x r of 
      Same r' -> AnyColor $ Black l y r' 
      Inc r' -> AnyColor $ Red l y r' 

所以它試圖寫一個函數：

insert2 same inc x l = case insert' x l of 
      Same aa -> same aa 
      Inc aa -> inc aa 

而且在任何地方使用它，例如：

insert x (AATree t) = insert2 AATree AATree x t 

有沒有辦法寫insert2？幼稚的方法不會檢查。

Answer 1

由於您是在GADT上分支的情況，可能整個類型的aa在case表達式的外部是未知的。這意味着你需要insert2的函數參數的更高等級的類型，以便它們可以用於任何類型的事件。

這需要{ - ＃LANGUAGE Rank2Types＃ - }以及insert2的顯式類型註釋。所需的確切註釋取決​​於您的GADT並插入'類型。 看着你的鏈接代碼我想你想要的東西像

insert2 :: (Ord a) => 
    (AANode Black (Succ n) a -> b) 
    -> (forall c. AANode c n a -> b) 
    -> a -> AANode c n a -> b