Le puzzle du typage bidirectionnel

• Dans l’implémentation du typage bidirectionnel de Grace, le type du premier élément d’une liste était utilisé comme s’il s’agissait du type de tous les éléments, ce qui a supprimé le champ port: 8080 et produit un résultat d’évaluation erroné
• L’exemple problématique parcourait une liste contenant { domain: "google.com" } et { domain: "localhost", port: 8080 }, avec du code utilisant le port par défaut 443, et renvoyait [ "google.com:443", "localhost:443" ] au lieu de la valeur attendue [ "google.com:443", "localhost:8080" ]
• L’ancienne inférence de liste déduisait List { domain: Text } à partir du premier élément, puis vérifiait les autres éléments contre ce type, et le processus d’élaboration supprimait ensuite les champs port absents du supertype
• L’implémentation corrigée infère désormais le type de chaque élément, calcule ensuite le supertype le plus spécifique, puis revérifie chaque élément contre ce type afin de compléter les valeurs Optional manquantes avec null ou some
• Après correction, la liste d’origine est inférée comme List { domain: Text, port: Optional Natural } ; le port du premier enregistrement devient null, et le port: 8080 du second est conservé sous la forme some 8080, ce qui permet d’obtenir le résultat attendu

---

Bug d’inférence de type des listes dans Grace

• Grace utilise un système de typage bidirectionnel fondé sur Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, et les implémentations accumulées pour contourner les limites de cette approche ont fini par provoquer un bug étrange
• Le programme en cause parcourait une liste authorities, associait domain et port pour chaque enregistrement, puis utilisait 443 comme valeur par défaut si port était absent, sous la forme d’une compréhension de liste

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"

• Le résultat attendu était [ "google.com:443", "localhost:8080" ], mais la version boguée renvoyait [ "google.com:443", "localhost:443" ], ignorant complètement le champ port: 8080 du second enregistrement
• Le problème ne venait pas de l’évaluateur mais du vérificateur de types, avec un effet combiné entre l’inférence du type des listes et l’élaboration effectuée pendant la vérification de type

Typage bidirectionnel et limites de l’ancienne inférence de listes

• Le type attendu par Grace pour la liste authorities était le suivant

List { domain: Text, port: Optional Natural }

• Cela signifie que chaque enregistrement possède un champ obligatoire domain: Text, tandis que le champ port: Optional Natural peut être présent ou non
• En pratique, l’ancienne implémentation inférait un type plus étroit

>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }

• Le typage bidirectionnel se divise essentiellement en deux opérations
  • inférer le type d’une expression
  • vérifier qu’une expression correspond à un type attendu
• À elles seules, ces deux opérations ne permettent pas facilement de combiner les types de plusieurs éléments d’une liste pour construire le supertype des éléments de toute la liste
• L’ancienne implémentation de Grace inférait le type des listes de la manière suivante
  • inférer le type du premier élément de la liste
  • vérifier que tous les autres éléments correspondent au type inféré à partir du premier
• Comme le premier élément { domain: "google.com" } a pour type { domain: Text }, le type des éléments de toute la liste devenait également { domain: Text }
• Si l’on voulait un autre type, il fallait ajouter une annotation de type explicite, mais les JSON réels que Grace veut manipuler peuvent avoir des schémas volumineux et complexes, et l’objectif n’était pas d’obliger à écrire tout le schéma sous forme d’une énorme annotation de type

Pourquoi l’élaboration modifiait aussi le résultat de l’évaluation

• Le vérificateur de types de Grace ne se contente pas de détecter les erreurs de type : il effectue aussi une élaboration qui ajuste les expressions au cours de la vérification
• Lorsqu’un sous-type est vérifié contre un supertype et que les deux diffèrent, le vérificateur insère une coercition explicite
• En interne, l’évaluateur de Grace représente toutes les valeurs Optional avec des étiquettes null ou some x
• Si une valeur sans étiquette est placée là où un Optional est attendu, Grace insère automatiquement l’étiquette some

>>> [ some 1, 2 ]  # This would be a type mismatch without elaboration
[ some 1, some 2 ]

• Si le type du premier élément est inféré comme Optional Natural et que le second élément est un Natural non étiqueté, le vérificateur insère donc l’étiquette some au lieu de signaler une incompatibilité de types
• Il se passe la même chose avec les enregistrements, et Grace prend en charge le sous-typage des enregistrements en coercissant les enregistrements pour les adapter au supertype attendu

>>> { x: 1, y: true }: { x: Natural }
{ "x": 1 }

• Lorsqu’un enregistrement est annoté avec un type d’enregistrement plus petit, le vérificateur l’accepte tout en supprimant les champs absents du supertype
• Même en évaluant uniquement la liste authorities, l’ancienne implémentation supprimait ainsi le champ port

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com" }, { "domain": "localhost" } ]

• Ce résultat provenait du déroulement suivant
  • le type du premier élément était inféré comme { domain: Text }
  • le second élément était vérifié contre ce type attendu
  • le second élément correspondait bien à ce type, mais possédait en plus un champ port
  • le vérificateur supprimait alors le champ port pour conformer la valeur au type attendu
• La coercition d’enregistrement n’était pas en soi la cause profonde ; le vrai problème venait du fait que l’inférence de type des listes traitait le type du premier élément comme s’il représentait celui de toute la liste

La solution : calculer le supertype le plus spécifique

• Grace a ajouté une nouvelle opération pour inférer correctement le type global d’une liste
• Cette nouvelle opération calcule le supertype le plus spécifique (most-specific supertype), c’est-à-dire la borne supérieure minimale (least upper bound), de deux types
• Dire que C est un supertype de A et B signifie que C est à la fois un supertype de A et un supertype de B
• Dire que C est le supertype le plus spécifique de A et B signifie que C est un sous-type de tous les autres supertypes communs à A et B
• Avec cette nouvelle opération, l’inférence du type des listes suit désormais cet ordre
  • inférer le type de chaque élément de la liste
  • calculer le supertype le plus spécifique de l’ensemble des types d’éléments
  • vérifier que chaque élément correspond à ce supertype le plus spécifique
  • renvoyer ce supertype comme type des éléments de toute la liste
• Avec cette approche, la liste suivante reçoit le bon type

>>> :type [ { x: 1 }, { y: true } ]
List { x: Optional Natural, y: Optional Bool }

• Le déroulement interne est le suivant
  • { x: 1 } est inféré comme ayant le type { x: Natural }
  • { y: true } est inféré comme ayant le type { y: Bool }
  • le supertype le plus spécifique des deux types devient { x: Optional Natural, y: Optional Bool }
  • chaque élément est ensuite revérifié contre ce supertype
• La raison de cette seconde vérification est d’appliquer la bonne élaboration, notamment pour compléter les some et null manquants

>>> [ { x: 1 }, { y: true } ]
[ { "x": some 1, "y": null }, { "y": some true, "x": null } ]

Type et résultat d’évaluation de authorities après la correction

• Après la modification du vérificateur de types, la liste authorities d’origine reçoit bien le type attendu

>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
List { domain: Text, port: Optional Natural }

• Le résultat d’évaluation élaboré conserve aussi port comme champ optionnel

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com", "port": null }
, { "domain": "localhost", "port": some 8080 }
]

• Le port absent du premier enregistrement est complété par null, tandis que le port: 8080 du second est conservé sous la forme some 8080
• L’exemple initial de compréhension de liste renvoie lui aussi enfin le résultat attendu

[ "google.com:443", "localhost:8080" ]

Support de JSON et compromis sur la complexité d’implémentation

• Si Grace pousse aussi loin le typage bidirectionnel, c’est parce que cette approche est jugée suffisamment puissante pour inférer les types de JSON réels, même au prix d’une plus grande complexité
• L’inférence de Hindley-Milner, ou d’autres cadres de vérification de types plus simples et proches, ont du mal à traiter les formes que l’on rencontre dans de véritables données JSON
• Grace n’a pas été conçue uniquement comme un langage ergonomique pour manipuler du JSON, mais elle n’ignore pas non plus ce cas d’usage
• L’expérience acquise avec Dhall a montré que les utilisateurs sont sensibles à une interopérabilité JSON ergonomique, et la syntaxe ainsi que le système de types de Grace ont été conçus en tenant compte de cette compatibilité, même si cela augmente la complexité de l’implémentation

Ressources connexes à consulter

• Datatype unification using Monoids : présente un algorithme d’inférence pour les types de données simples, essentiellement équivalent à celui utilisé par Grace pour calculer le supertype le plus spécifique
• The appeal of bidirectional typechecking : explique pourquoi il vaut la peine d’apprendre le typage bidirectionnel lorsqu’on veut implémenter un langage qui utilise d’une manière ou d’une autre le sous-typage
• Local Type Inference : l’un des articles fondateurs sur le typage bidirectionnel, cité ici comme source de techniques telles que la borne supérieure minimale et l’élaboration d’expressions vers un langage interne

Annexe : pourquoi la coercition d’enregistrements est nécessaire

• L’expression Grace suivante montre pourquoi la coercition d’enregistrements est nécessaire

let f (input: { }) = input.x

in  f { x: 1 }

• Si cette expression passait la vérification de type, la question serait : quel devrait être le type de retour de f ?
• Ce type de retour ne doit pas être Natural

let f (record: { }): Natural = record.x  # WRONG: type error

in  f { x: 1 }

• Comme f reçoit un input de type enregistrement vide { }, elle ne peut pas en extraire une valeur Natural
• Même si, à l’appel, on lui passe par hasard un enregistrement doté d’un champ x, la fonction f doit fonctionner pour toute entrée du type { }
• Refuser les accès à des champs absents du type d’entrée déclaré serait aussi un choix cohérent du point de vue de la sûreté, mais cela ferait perdre des capacités nécessaires pour manipuler de vraies données JSON
• L’exemple initial avec authorities est essentiellement du sucre syntaxique pour l’expression suivante

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for authority of authorities

let default = fold{ some port: port, null: 443 }

in  "${authority.domain}:${show (default authority.port)}"

• Si l’accès à un champ absent était refusé, il deviendrait impossible de lier des champs potentiellement absents ou de leur appliquer une valeur par défaut
• Le choix de conception pour bien gérer des données JSON réelles est donc le suivant
  • renvoyer null lorsqu’un champ est absent
  • donner au type d’accès la forme forall (a: Type) . Optional a
• Ce type est un type qui ne peut contenir que null
• Avec cette approche, il faut absolument supprimer des enregistrements les champs absents du supertype
• Sans cette suppression des champs supplémentaires, l’exemple suivant renverrait 1 : forall (a: Type) . Optional a

let f (input: { }) = input.x

in  f { x: 1 }

• On obtiendrait alors une expression mal typée, puisque 1 apparaîtrait dans un type qui ne devrait contenir que null
• Une telle expression incorrecte pourrait même faire planter l’évaluateur

let f (input: { }) = input.x  # Inferred type: forall (a: Type). Optional a

let default (input: Optional Text) = fold{ some text: text, "" }

in  "${default (f { x: 1 })}!"  # Runtime error if `f` returns `1`

• Dans Grace, qui vise la manipulation de données JSON réelles, il est donc raisonnable de coercer explicitement les enregistrements vers le supertype attendu ; le bug réel ne venait pas de cette coercition, mais de l’ancien correctif provisoire utilisé pour l’inférence du type List

[GN⁺]

Commentaires sur Lobste.rs

• C’est à saluer d’avoir transformé l’article Complete And Easy en quelque chose qui fonctionne réellement. C’est aussi un bon exemple de la manière dont la nature gloutonne du typage bidirectionnel peut créer des problèmes subtils
  Ce n’est pas une critique : l’inférence pose toujours des problèmes, et au fond il s’agit surtout de choisir quels problèmes on est prêt à accepter. C’est pourquoi, personnellement, je considère généralement le sous-typage et les conversions de type forcées comme des anti-patterns
  Si l’on prend les données comme source de vérité du type, il devient plus difficile de vérifier si les données sont erronées, et on obtient alors un type incorrect au lieu d’une erreur utile, comme dans l’exemple. Cela dit, comme c’est la personne qui a créé Dhall, elle s’y connaît probablement bien mieux que moi. L’idée de générer un schéma à partir de plusieurs jeux de données mérite d’être étudiée, mais comme les types sont généralement vus comme prescriptifs plutôt que descriptifs, je ne sais pas vraiment si j’appellerais cela du « typage »

• Je ne comprends pas bien pourquoi on ne rejette pas simplement f. On accède à un champ dans un enregistrement d’un type qui ne pourra jamais posséder ce champ ; c’est donc presque certainement un bug dans le programme, et cela ressemble à un cas où le type checker devrait le signaler
  La différence avec l’exemple d’authority, c’est que le type de port n’est pas absent, mais Optional. Rejeter les champs absents n’implique pas qu’il faille aussi rejeter les champs optionnels. Si l’on effectue déjà des conversions de valeurs fondées sur les types, alors on peut aussi convertir { domain: "google.com" } en { domain: "google.com", port: null }

  • En bref, il n’est pas nécessaire de rejeter f, et ce serait une restriction inutile. Je pense qu’autoriser un accès à un champ invalide à renvoyer null : forall (a : Type) . Optional a est strictement préférable au fait de rejeter l’accès à un champ invalide
    Cela autorise davantage de programmes valides, et les programmes mal typés échouent toujours. Par exemple, un programme qui essaie d’utiliser la valeur accédée sans traiter le cas null continuera d’avoir une erreur de type

• Ma première pensée est que les row types résolvent ce problème. J’imagine que cela a déjà été envisagé. Est-ce qu’ici les row types s’effondrent à cause de leur interaction avec le sous-typage ?

  • Grace possède des row types et du polymorphisme de lignes. Dans Grace, les lignes sont appelées « fields », mais sinon c’est exactement la même chose
    En pratique, l’algorithme du plus petit supertype le plus spécifique prend aussi les row types en compte
    Par exemple, si on écrit quelque chose comme :

    \record0 record1 ->
    
    let _ = record0.x
    
    let _ = record1.y
    
    in  [ record0, record1 ]  
    

    Grace infère alors pour cette expression le type suivant :

    forall (a : Type) .  
    forall (b : Type) .  
    forall (c : Fields) .  
      { x: b, y: a, c } -> { y: a, x: b, c } -> List { x: b, y: a, c }  
    

• N’est-ce pas un exemple du problème d’instanciation gloutonne évoqué dans la section 5.1.1 de l’article Bidirectional Typing ?
  « Dans le cadre initial, il était assez malheureux que cette approche gloutonne soit sensible à l’ordre des arguments. Mais elle peut bien fonctionner dans un cadre de polymorphisme de haut rang prédicatif sans autres formes de sous-typage. Le “tabby-first problem” ne peut pas se produire, parce que la seule manière pour un type de devenir strictement plus petit est de devenir strictement plus polymorphe, et si le premier argument était polymorphe, alors il faudrait instancier 𝛼 avec un type polymorphe, ce qui violerait la prédicativité »