Comment déboguer les programmes au niveau du type

Question

J'essaye de faire de la programmation de type hoopy, et ça ne marche pas. Je m'arrache les cheveux à essayer de comprendre pourquoi GHC ne parvient pas à déduire les signatures de type que je veux.

Existe-t-il un moyen de faire en sorte que GHC dites-moi ce qu'il fait ?

J'ai essayé -ddump-tc qui ne fait qu'imprimer les signatures de type finales. (Oui, elles sont fausses. Merci, je le savais déjà).

J'ai aussi essayé -ddump-tc-trace qui jette ~70KB de charabia incompréhensible. (En particulier, je ne vois pas d'identifiants écrits par l'utilisateur qui soient mentionnés. partout .)

Mon code est le suivant si proche fonctionne, mais une variable de type supplémentaire continue d'apparaître. Pour une raison quelconque, GHC ne voit pas que cette variable doit être complètement déterminée. En effet, si je manuellement écrire la signature de type cinq-mile, GHC l'accepte joyeusement. Donc il me manque clairement une contrainte quelque part... mais où ? !? >_<

Answer 1

Comme cela a été mentionné dans les commentaires, j'utilise généralement :kind et :kind ! dans GHCi, mais l'endroit où vous placez les fonctions est étonnamment important, et ce qui semble être identique ne l'est pas toujours.

Par exemple, j'ai essayé de faire un équivalent de foncteur typé de manière dépendante, pour un projet personnel, qui ressemblait à ceci

class IFunctor f where 
  ifmap :: (a -> b) -> f n a -> f n b 

et j'écrivais l'instance pour

data IEither a n b where 
  ILeft :: a -> IEither a Z b 
  IRight :: b -> IEither a (S n) b 

Cela devrait être assez simple, ai-je pensé, il suffit d'ignorer f pour le cas de gauche, de l'appliquer dans le cas de droite.

J'ai essayé

instance IFunctor (IEither a) where
  ifmap _ l@(ILeft _) = l 
  ifmap f (IRight r) = IRight $ f r

mais pour la version spécialisée de ifmap dans ce cas étant ifmap :: (b -> c) -> IEither a Z b -> IEither a Z c Haskell a déduit que le type de l est IEither a Z b sur le LHS, ce qui est logique, mais a ensuite refusé de produire b ~ c .

Donc, j'ai dû déballer l, obtenir la valeur du type a, puis le remballer pour obtenir la valeur du type a. IEither a Z c .

Ce n'est pas seulement le cas avec les types dépendants, mais aussi avec les types de rang-n. Par exemple, j'essayais de convertir les isomorphismes d'une forme propre en transformations naturelles, ce qui devrait être assez facile, pensais-je.

Apparemment, je devais placer les déconstructeurs dans une clause where de la fonction, car sinon l'inférence de type ne fonctionnait pas correctement.