découlant automatiquement des instances de spectacle pour GADTs

Question

Supposons que j'ai un GADT complexe avec de nombreux paramètres de type cachés comme les constructeurs:

data T where 
    A :: Num n => n -> T 
    B :: (Num n, Integral m) => n -> m -> T 
    C :: Floating a => [a] -> T 
    -- and so on 
    Z :: Num n => n -> n -> T 

Je veux faire de ce type de données montrable sans avoir à écrire manuellement l'instance. Le problème est que, puisque Show n'est plus une super-classe de Num, ajouter un simple deriving instance Show T ne suffit pas pour que le compilateur déduise qu'il doit ajouter des contraintes Show à tous les paramètres de type cachés internes.

Pour chaque paramètre de type caché, il émet quelque chose comme

Could not deduce (Show n) arising from a use of 'showsPrec' 
from the context Num n 
    bound by a pattern with constructor 
      A :: forall n. Num n => n -> T 
... 
Possible fix: 
    add (Show n) to the context of the data constructor 'A' 

Ajout d'une contrainte Show au type de données n'est pas une option non plus, car elle limite les habitants possibles de T. Il semble que deriving instanec Show T devrait introduire la contrainte Show sur les types de données cachés, bien que je ne sois pas sûr.

Comment puis-je faire à ce sujet?

Answer 1

J'ai eu une pensée intéressante, je ne sais pas comment c'est pratique. Mais si vous voulez que T soit visible lorsque les paramètres sont visibles, mais aussi utilisable avec des paramètres non affichables, vous pouvez paramétrer T sur une contrainte, en utilisant ConstraintKinds.

{-# LANGUAGE GADTs, ConstraintKinds #-} 

import Data.Kind 

data T :: (* -> Constraint) -> * where 
    A :: (Num n, c n) => n -> T c 
    B :: (Num n, c n, Integral m, c m) => n -> m -> T c 
    ... 

Alors T Show sera montrable ... peut-être

deriving instance Show (T Show) 

(avec StandaloneDeriving extension) fonctionnera, mais à tout le moins, T est montrable en principe et vous pouvez écrire l'instance manuellement.

Bien que mon conseil pratique est de réifier les existentiels. Un type existentiel est équivalent à la collection de ses observations. Par exemple, si vous aviez une classe comme

class Foo a where 
    getBool :: a -> Bool 
    getInt :: a -> Int 

alors le

existentiel

data AFoo where 
    AFoo :: Foo a => a 

est exactement équivalent à (Bool,Int), parce que la seule chose que vous pouvez faire avec un Foo dont le type vous ne savez pas est appelez le getBool ou le getInt dessus. Vous utilisez Num dans votre type de données et Num a pas d'observation, car si vous avez un a inconnu avec Num a, la seule chose que vous pouvez faire en appelant des méthodes de Num est d'obtenir plus a Sout, et rien de plus concret. Donc, votre constructeur A

A :: (Num n) => n -> T 

vous donne rien et vous pourriez aussi bien dire que

A :: T 

Integral, d'autre part, a toInteger comme une observation.Donc, vous pourriez probablement remplacer

B :: (Num n, Integral m) => n -> m -> T 

avec

B :: Integer -> T 

(nous avons perdu l'argument n et remplacé m avec Integer). Je ne pense pas que ce soit techniquement équivalent puisque nous aurions pu mettre en place ses opérations différemment que Integral, mais nous commençons à être assez techniques en ce moment et je doute que vous en ayez besoin (je serais intéressé de savoir si vous le faites).