Force GHC à ignorer la contrainte de type manquant

Question

J'ai construit un type Sup qui incorpore une valeur d'un autre type t en utilisant le sous-typage constructeur.

data Sup t = ... 
      | Sub t 
      deriving Eq 

Parce que la partie omise de Sup contient beaucoup de constructeurs, dont aucun n'utilisent t, je veux Eq (Sup t) tirent plutôt que de donner un exemple manuel.

Une contrainte de type Eq t est maintenant en place sur l'instance de (==) pour Sup t:

(==) :: Eq t => Sup t -> Sup t -> Bool

Le prédicat isSub :: Sup t -> Bool est défini comme suit:

isSub :: Sup t -> Bool 
isSub (Sub _) = True 
isSub _  = False 

Avec l'aide de ce prédicat Je souhaite définir l'opérateur suivant:

supEq :: Sup t -> Sup t -> Bool 
supEq x y = not (isSub x) && not (isSub y) && x == y 

La définition ci-dessus n'est pas acceptée par GHC, car la contrainte de type Eq t est manquante. Cependant, grâce à l'évaluation paresseuse, je sais que l'égalité entre les valeurs de type t n'est jamais réellement utilisée.

Existe-t-il un moyen de forcer GHC à ignorer la contrainte de type manquante? Sinon, est-il possible d'avoir défini Sup ou supEq pour obtenir le résultat souhaité: une définition de supEq sans avoir à propager une contrainte de type redondant où supEq est utilisé et sans avoir à donner une instance manuelle pour Eq (Sup t).

Answer 1

Probablement la chose la plus facile à faire est de définir une instance personnalisée Eq (Sup t).

instance (Eq t) => Eq (Sup t) where 
    (Sub a) == (Sub b) = a == b 
    A == A = True 
    ... 

Alternativement, si vous voulez == à se comporter comme supEq, vous pouvez écrire l'instance (de sorte que vous n'avez pas besoin supEq du tout) sans la contrainte:

instance Eq (Sup t) where 
    (Sub a) == (Sub b) = False 
    A == A = True 
    ... 

Une autre approche est de diviser Sup t en deux types de données:

data Sup' = A | B | ... | Z deriving (Eq) -- nothing depends on `t` 
data Sup t = Sub t | Sup' 

supEq :: Sup t -> Sup t -> Bool 
supEq (Sub _) _ = False 
supEq _ (Sub _) = False 
supEq a b = a == b 

Bien sûr, encore une dernière option est de renverser le système de type. C'est certainement la mauvaise chose à faire, mais je vais vous laisser cette détermination.

{-# LANGUAGE ScopedTypeVariables #-} 
import Data.Constraint 

supEq :: forall t . Sup t -> Sup t -> Bool 
supEq x y = let Dict = unsafeCoerce (Dict :: Dict()) :: Dict (Eq t) 
      in not (isSub x) && not (isSub y) && x == y 

Answer 2

Il n'y a aucun moyen de se débarrasser de la contrainte Eq si vous utilisez (==) tout en collant avec l'instance dérivée sans surprise. De plus, en ce qui concerne supEq, votre invariant n'est pas appliqué (considérez ce qui se passerait si vous commettiez une erreur et que vous échangiez True et False dans isSub).Vous êtes probablement mieux écrire supEq en termes de Sup seul motif correspond:

data Sup t = Foo 
      | Bar 
      | Sub t 
      deriving Eq 

supEq :: Sup t -> Sup t -> Bool 
supEq (Sub _) _ = False 
supEq _ (Sub _) = False 
supEq Foo Foo = True 
supEq Bar Bar = True 
supEq _ _ = False 

S'il y a des cas assez que l'écriture supEq de cette façon devient ennuyeux, vous pouvez diviser les Sub non des cas dans un type distinct, comme dans l'exemple suivant à la dernière dans la réponse de crockeea, reproduite ci-dessous pour être complet:

data Sup' = Foo | Bar deriving (Eq) 
data Sup t = Sub t | NotSub Sup' deriving (Eq) 

supEq :: Sup t -> Sup t -> Bool 
supEq (Sub _) _ = False 
supEq _ (Sub _) = False 
supEq (NotSub a) (NotSub b) = a == b 

Answer 3

Bien sûr, la solution la plus simple est de diviser votre type en deux types, comme d'autres l'ont suggéré. Mais cela crée un bruit syntaxique - un niveau supplémentaire de constructeurs. Si vous voulez le meilleur des deux, vous pouvez utiliser reflection:

import Data.Reflection 
import Data.Proxy 
import Data.Coerce 

data Sup t = Sub t | A | B | C | D | E -- .. etc 
    deriving (Eq, Show) 

Nous allons maintenant utiliser le code généré pour EqSup, mais le remplaçant dans une autre fonction, non (==), lorsque l'on compare avec SubSub.

Tout d'abord vous avez besoin d'une certaine configuration (je pense que cela devrait être dans le même paquet reflection - il a le code similair pour Monoid et Applicative):

newtype ReifiedEq a = ReifiedEq { eq :: a -> a -> Bool } 
newtype ReflectedEq s a = ReflectedEq a 

instance Reifies s (ReifiedEq a) => Eq (ReflectedEq s a) where 
    (==) = coerce (eq (reflect (Proxy :: Proxy s))) 

C'est le cœur de la solution - une valeur de type ReflectedEq s a est juste un a, mais lorsque comparé pour l'égalité utilise la fonction d'égalité fournie par Reifies, que vous pouvez spécifier à tout moment. Notez que le package reflection utilise des machines de niveau machine pour empêcher l'utilisation de plusieurs instances Eq dans le même contexte.

Maintenant, vous pouvez écrire une fonction encore plus générale que votre choix un:

supEqWith :: (t -> t -> Bool) -> Sup t -> Sup t -> Bool 
supEqWith k x y = reify (ReifiedEq k) (\p -> h p x == h p y) where 
    h :: Proxy s -> Sup a -> Sup (ReflectedEq s a) 
    h _ = coerce 

Cette fonction compare simplement les valeurs Sup pour l'égalité, en utilisant la fonction spécifiée (k) pour comparer les valeurs t à l'intérieur Sub. La fonction h est nécessaire pour spécifier correctement le paramètre de type fantôme (s), sinon elle est ambiguë.

Votre fonction souhaitée est simplement:

supEq = supEqWith (\_ _ -> False) 

Answer 4

Si votre type Sup peut être un foncteur dans t (deriving Functor travaillerait sur l'exemple que vous avez donné), et vous savez qu'aucun des autres constructeurs utilisent t, alors vous pouvez fmap (const()) il.

Ensuite, vous avez une garantie que le t n'affectera pas le contrôle d'égalité de façon intéressante et n'a pas besoin de l'original t pour avoir Eq. Vous avez juste besoin de garder le cas lorsque les deux entrées étaient Sub _ afin que vous retourniez false au lieu de vrai.

subEq (Sub _) _ = False 
subEq _ (Sub _) = False 
subEq x y = fmap (const()) x == fmap (const()) y 

Même si vous ne voulez pas faire Sup un foncteur, vous pouvez toujours mettre en œuvre submap :: (a -> b) ->Sup a -> Sup b et l'utiliser.