2

このコードには、繰り返されるフラグメントがあります。

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か？素朴なアプローチはタイプチェックしません。

4

1 に答える 1

6

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
于 2012-09-04T02:13:17.937 に答える