haskell - GADT 模式匹配的封装

Question

在这段代码中有重复的片段：

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 类型。这意味着您需要更高级别的类型作为 insert2 的函数参数，以便它们可以用于任何类型的 aa。

这需要 {-# 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