Dérivation automatique des contraintes de classe de type en utilisant GADTs

Question

J'écris une bibliothèque pour traiter des séquences infinies en utilisant l'évaluation paresseuse. Par souci de brièveté, j'utilise des types de données algébriques généralisées (GADT) pour affirmer une contrainte Ord sur l'index de chaque terme de la séquence. Par conséquent, les typable suivants:

{-# LANGUAGE GADTs #-} 

data Term ix cff where 
    Term :: (Ord ix) => ix -> cff -> Term ix cff 

data Sequence ix cff where 
    Seq :: [Term ix cff] -> Sequence ix cff 

f (Seq (Term i x:_)) (Seq (Term j y:_)) = i < j 

{- 
add :: Sequence ix cff -> Sequence ix cff -> Sequence ix cff 
add (Seq tms1) (Seq tms2) = Seq (addAlong (<) tms1 tms2) 
    where addAlong :: (ix -> ix -> Bool) -> 
         [Term ix cff] -> [Term ix cff] -> [Term ix cff] 
      addAlong ord (Term i x : tms1) (Term j y : tms2) = [] 
-} 

Comme prévu, GHCi me dit que f :: Sequence t t1 -> Sequence t t2 -> Bool. Faire la comparaison i < j nécessite une instance Ord, mais cela est pris en charge par la contrainte (Ord ix) dans la définition de Term.

Toutefois, lorsque le bloc inférieur est décommenté, la fonction add ne parvient pas à indiquer une erreur typographique avec l'erreur No instance for (Ord ix) arising from the use of ``<''. Ne devrait-il pas être en mesure de comprendre (Ord ix) du Term ix cff qui apparaît dans la définition de Sequence?

Answer 1

Les termes liés à un argument de fonction sont par défaut monomorphes (alias polymorphe de rang 0), car Haskell98 ne supporte que le polymorphisme de rang 1, et un argument polymorphe rend une fonction polymorphe de rang 2. Par conséquent, dans Seq (addAlong (<) tms1 tms2), le compilateur peut uniquement considérer < comme une comparaison monomorphe sur le type rigide ix. Pour considérer < comme une fonction monomorphique, le compilateur doit résoudre l'instance Ord. Cependant, à ce stade, l'instance Ord ix n'est pas disponible, car elle ne peut être comparée qu'à partir d'un Term!

La solution qui est la plus proche de votre code d'origine est de faire addAlong rang 2 polymorphes explicitement:

{-# LANGUAGE RankNTypes, UnicodeSyntax #-} 

add :: Sequence ix cff -> Sequence ix cff -> Sequence ix cff 
add (Seq tms1) (Seq tms2) = Seq (addAlong (<) tms1 tms2) 
    where addAlong :: (∀ ix' . Ord ix' -> ix' -> Bool) -> 
         [Term ix cff] -> [Term ix cff] -> [Term ix cff] 
      addAlong ord (Term i x : tms1) (Term j y : tms2) = [] 

De cette façon, < est tout simplement passé comme il est (comme méthode Ord => ... polymorphes), d'où le compilateur n'a pas besoin d'avoir l'instance disponible à Seq (addAlong (<) tms1 tms2) mais peut la résoudre plus tard lorsque vous avez Term s disponibles.

Vous devriez bien sûr considérer si vous en avez vraiment besoin. Garder un dictionnaire Ord dans chaque Term me semble plutôt inutile de - le problème ne tournerait pas si vous la contrainte gardé Seq à la place:

data Term ix cff where Term :: ix -> cff -> Term ix cff 

data Sequence ix cff where 
    Seq :: Ord ix => [Term ix cff] -> Sequence ix cff 

add :: Sequence ix cff -> Sequence ix cff -> Sequence ix cff 
add (Seq tms1) (Seq tms2) = Seq (addAlong (<) tms1 tms2) 
    where addAlong :: (ix -> ix -> Bool) -> 
         [Term ix cff] -> [Term ix cff] -> [Term ix cff] 
      addAlong ord (Term i x : tms1) (Term j y : tms2) = []