IP Girl
  1. IP Girl
  3. Techniques de traçage des contraintes
Intereting Posts
Postgresql: comment créer une table uniquement si elle n’existe pas déjà? Pourquoi “sizeof (a? True: false)” donne-t-il une sortie de quatre octets? Comment allumer le flash avant par programmation sous Android? Pouvez-vous vérifier qu’une exception est lancée avec doctest en Python? Cordova: [Erreur: Veuillez installer la cible Android: “android-21” Comment est-ce que je fais le schéma automatique de couleur de changement automatique de fenêtre de terminal Apple quand je ssh à un serveur spécifique Résultat de l’exercice d’interview intéressant: retour, post-incrémentation et comportement ref Créer une twig Git avec les modifications en cours Git – raccourci de twig actuel Vérification de JToken vide / null dans un object JObject Comment supprimer et remplacer la dernière ligne du terminal en utilisant bash? Knockout: Comment vérifier si les liaisons ont été appliquées à la zone de la page Avec ng-bind-html-unsafe enlevé, comment puis-je injecter du HTML? Comment transformer du noir en n’importe quelle couleur en utilisant uniquement des filtres CSS Comment exécuter une tâche asynchrone pour chaque x minute dans Android?

Techniques de traçage des contraintes

Voici le scénario: J’ai écrit du code avec une signature de type et GHC n’a pas pu déduire x ~ y pour certains x et y . Vous pouvez généralement lancer GHC un os et simplement append l’isomorphisme aux contraintes de la fonction, mais c’est une mauvaise idée pour plusieurs raisons:

  1. Il ne met pas l’accent sur la compréhension du code.
  2. Vous pouvez vous retrouver avec 5 contraintes où l’on aurait suffi (par exemple, si les 5 sont impliquées par une contrainte plus spécifique)
  3. Vous pouvez vous retrouver avec de fausses contraintes si vous avez fait quelque chose de mal ou si GHC n’est pas utile

Je viens de passer plusieurs heures à affronter le cas 3. Je joue avec syntactic-2.0 et j’essayais de définir une version de share indépendante du domaine, similaire à la version définie dans NanoFeldspar.hs .

J’ai eu ceci: 

 {-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-} import Data.Syntactic -- Based on NanoFeldspar.hs data Let a where Let :: Let (a :-> (a -> b) :-> Full b) share :: (Let : (a -> b) -> b) fi) => a -> (a -> b) -> a share = sugarSym Let

et GHC could not deduce (Internal a) ~ (Internal b) , ce qui n’est certainement pas ce que j’allais faire. Donc, soit j’ai écrit du code que je n’avais pas l’intention (ce qui nécessitait la contrainte), soit GHC voulait cette contrainte en raison d’autres contraintes que j’avais écrites.

Il s’est avéré que je devais append (Syntactic a, Syntactic b, Syntactic (a->b)) à la liste des contraintes, aucune n’impliquant (Internal a) ~ (Internal b) . Je suis tombé essentiellement sur les bonnes contraintes; Je n’ai toujours pas de façon systématique de les trouver.

Mes questions sont:

  1. Pourquoi GHC a-t-il proposé cette contrainte? Nulle part dans la syntaxe n’est-il une contrainte Internal a ~ Internal b , alors d’où GHC tire-t-elle cela?
  2. En général, quelles techniques peuvent être utilisées pour tracer l’origine d’une contrainte dont le GHC estime avoir besoin? Même pour les contraintes que je peux découvrir moi-même, mon approche est essentiellement brutale en forçant le chemin offensant en écrivant physiquement des contraintes récursives. Cette approche va fondamentalement dans un environnement infini de contraintes et représente la méthode la moins efficace que je puisse imaginer.

    Tout d’abord, votre fonction a le mauvais type; Je suis à peu près sûr que ce devrait être (sans le contexte) a -> (a -> b) -> b . GHC 7.10 est un peu plus utile pour indiquer cela, car avec votre code d’origine, il se plaint d’une contrainte manquante Internal (a -> b) ~ (Internal a -> Internal a) . Après avoir fixé le type de share , GHC 7.10 rest utile pour nous guider:

    1. Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))

    2. Après avoir ajouté ce qui précède, nous obtenons Could not deduce (sup ~ Domain (a -> b))

    3. Après avoir ajouté cela, nous obtenons Could not deduce (Syntactic a) , Could not deduce (Syntactic b) et Could not deduce (Syntactic (a -> b))

    4. Après avoir ajouté ces trois éléments, il a finalement été détecté; donc on se retrouve avec 

       share :: (Let :<: sup, Domain a ~ sup, Domain b ~ sup, Domain (a -> b) ~ sup, Internal (a -> b) ~ (Internal a -> Internal b), Syntactic a, Syntactic b, Syntactic (a -> b), SyntacticN (a -> (a -> b) -> b) fi) => a -> (a -> b) -> b share = sugarSym Let

    Je dirais donc que GHC n’a pas été inutile pour nous guider.

    En ce qui concerne votre question sur le traçage où GHC obtient ses exigences de contrainte, vous pouvez essayer les indicateurs de débogage de GHC , en particulier -ddump-tc-trace , puis lire le journal résultant pour voir où Internal (a -> b) ~ t et (Internal a -> Internal a) ~ t sont ajoutés à l’ensemble Wanted , mais la lecture sera assez longue.