Encapsulation du modèle GADT correspond

Question

Dans ce code il y a des fragments REPETE:

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' 

Il est donc tentant d'écrire une fonction:

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

et l'utiliser partout, par exemple:

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

Existe-t-il un moyen d'écrire insert2? L'approche naïve ne caractérise pas.

Answer 1

Étant donné que vous effectuez une dérivation de cas sur un GADT, il est probable que le type entier de aa n'est pas connu à l'extérieur de l'expression de casse. Cela signifie que vous avez besoin de types de rang supérieur pour les arguments de la fonction insert2 afin qu'ils puissent être utilisés à n'importe quel type.

Cela nécessite {- # LANGUAGE Rank2Types # -} ainsi qu'une annotation de type explicite pour insert2. L'annotation exacte nécessaire dépend de vos types GADT et insert. En regardant votre code lié Je pense que vous voulez quelque chose comme

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