Algorithme d’unification

Le contexte général 

Les langages modernes polymorphes de haut niveau comme OCaml et Haskell ont des systèmes de type avancés qui permettent la détection d’expressions mal typées à la compilation. Pour conserver un typage au maximum implicite, ils s’appuient sur des algorithmes d’inférence de type, traditionnellement dérivés des algorithmes J et W de Milner ([7]) et basés sur l’unification de types et peuvent devenir complexes lorsque l’on étend le langage ML avec d’autres constructions (enregistrements, objets, sous-typage, GADT, polymorphisme de première classe etc..).

Inférer le type d’une expression se ramène à lui assigner une variable de type fraîche qui va être contrainte par la forme de l’expression mais aussi par son contexte. Par exemple, le type d’une abstraction est de la forme α → β où α et β sont respectivement unifiées avec le type du paramètre de l’abstraction et celui de sa valeur de retour. C’est ensuite la résolution des contraintes ainsi générées puis la reconstruction du terme élaboré qui résulte en une expression explicitement typée. L’inférence de types se décompose donc en trois étapes : génération de contraintes, résolution et élaboration. Les algorithmes traditionnels mélangent génération et résolution. En plus de rendre les preuves plus compliquées, cela les rend moins modulaires : chaque extension du langage impose de refaire des parties de la résolution, alors qu’elle ne dépend pas du langage source. L’inférence de types par contrainte propose de résoudre ces problème en séparant les deux étapes : le programme est traduit en contraintes qui sont ensuite résolues. La résolution ne dépend alors que du langage de contraintes qui fait le lien entre les deux étapes. Cette méthode a été largement explorée dans l’article [9] pour le système de type de ML ou à laHindley-Milner [3], en prouvant la décidabilité de l’inférence, la principauté et en montrant la robustesse de l’algorithme à l’ajout de diverses extensions du langage.

La contribution proposée 

La difficulté de l’inférence avec les abréviations de type réside principalement dans trois points (1) la définition de nouveaux alias de type peut créer une multitude de cas de types pathologiques ; (2) le coût de l’expansion est potentiellement élevée ; (3) à l’élaboration, on dispose non plus d’un unique type solution mais d’un ensemble de types équivalents. Pour résoudre ces problèmes, je me suis d’abord concentrée sur la définition de la bonne formation d’une abréviation, en particulier dans les cas de types récursifs. J’ai aussi traité le cas particulier des abréviations non productives, i.e. qui s’expansent complétement vers une variable de type et qui demandent un traitement particulier. Pour résoudre les points (2) et (3), j’ai enrichi la structure des multi-équations des contraintes pour permettre la mémorisation des expansions réalisées et j’ai adapté les règles de génération et les règles de réécriture qui constituent l’algorithme d’unification et décrites dans [9] pour gérer les abréviations. La sémantique de la structure de multi-équations proposée est exprimée au travers d’invariants dont j’ai prouvé la préservation par les règles d’unification. Je décris aussi que les bonnes propriétés de cet algorithme (préservation des solutions et terminaison). Ensuite, je propose une stratégie d’application des règles d’unification pour essayer de minimiser les expansions réalisées. L’approche choisie permet à l’utilisateur d’implémenter facilement sa propre stratégie d’élaboration des abréviations. Enfin, j’ai réalisé l’implémentation de l’algorithme d’unification  avec abréviations dans Inferno.

Les arguments en faveur de sa validité
L’algorithme d’unification proposée est intéressant car il reste proche de la version sans abréviation, utilisant ainsi les mêmes intuitions. Il permet de plus de laisser le choix de la stratégie d’élaboration à l’utilisateur. Sa validité est prouvé au travers de ses propriétés essentielles : chaque règle préserve les solutions des contraintes, l’algorithme termine et ces formes normales sont celles attendues. Enfin, le travail d’implémentation réalisé – même incomplet – montre que l’algorithme d’unification proposé est adaptable à Inferno.

Langage source 

Le langage source choisi est ML auquel on ajoute (1) des définitions d’abréviations de types, possiblement mutuellement récursives, et toutes placées au début du programme pour simplifier leur gestion (leur portée est tout le programme  ) ; (2) des annotations de types (nécessaires pour utiliser les abréviations) ; (3) l’introduction explicite des nouvelles variables de type. Contrairement à ML, les variables de type ne sont pas liées implicitement : pour être utilisées dans une annotation, les variables de type doivent avoir été introduites auparavant.

Sur les abréviations

Les abréviations permettent d’introduire des alias de types. Peu de règles limitent leur définition en OCaml : abréviations non productives (par exemple, type α F = α, cf 2.2), mutuellement récusives (2.5), ou avec des paramètres fantômes (par exemple, type (α, β) F = α → α, cf 2.4) mais la bonne formation d’abréviations y est peu documentée. On donne ici une définition (incomplète) de la bonne formation des abréviations et de l’opération d’expansion (2.1) qui permet d’unifier des types avec les abréviations.

Expansion

Expanser une abréviation consiste à remplacer l’abréviation par son expansion, en substituant ses paramètres par les arguments de l’abréviation, c’est-à-dire, si F α = τ0, alors F τ s’expanse vers τ0 [α ← τ ]. C’est une opération nécessaire lors de l’unification de deux types F τ = G τ 0 dont les constructeurs de tête sont différents. Sans abréviation, il s’agit d’un conflit (unification impossible), mais avec des abréviations, il est nécessaire d’expanser F et/ou G pour les unifier. Une première stratégie pourrait consister à expanser complétement les deux pour se ramener à une situation d’unification sans abréviation. Cependant, cette stratégie a deux défauts principaux : (1) elle peut être coûteuse et (2) elle limite l’élaboration. Expanser est une opération potentiellement coûteuse car le type expansé peut avoir une taille arbitrairement grande – pensons aux objets notamment.

La stratégie d’expansion agressive des abréviations limite aussi les stratégies d’élaboration possible. En effet, il est impossible de savoir quel est le type le moins expansé qui permet de réaliser une unification. L’exemple précédent illustre ce point : en expansant agressivement, le type retourné pour y est int ∗ int → int, alors que le type F permet de signifier de façon plus concise l’égalité entre de les types de x et y, et pourrait donc être préférable. On va chercher par la suite à développer une stratégie de résolution des contraintes qui, contrairement à une stratégie d’expansion agressive, minimise les nombres d’expansions réalisées et mémorise les expansions réalisées pour permettre une meilleure élaboration . On définit deux systèmes de réécriture liées à l’expansion. Le premier ▷ . correspond à l’expansion en tête, utilisée dans la résolution de contraintes et la seconde ; représente l’expansion sous un contexte et est utile pour décrire l’égalité entre des types avec abréviations.

Table des matières

Introduction
1 Langage source
1.1 Grammaire
1.2 Syntaxe des types
1.3 Types clos
2 Sur les abréviations
2.1 Expansion
2.2 Abréviations non productives
2.3 Représentation des abréviations
2.4 Décomposition et paramètres fantômes
2.5 Définitions valides et abréviations récursives
3 Génération de contraintes
3.1 Syntaxe du langage des contraintes
3.2 Génération de contraintes
4 Algorithme d’unification
4.1 Interprétation et satisfiabilité des contraintes
4.2 Algorithme d’unification sans abréviation
4.3 Algorithme d’unification avec abréviations
5 Stratégie d’unification
5.1 Rang et représentant
5.2 La stratégie
5.3 Limites de la stratégie
6 Élaboration
6.1 Contraintes à valeurs
6.2 Stratégies d’élaboration
7 Conclusion
A Références
B Table des matières
C Exemple
D Preuves

Lire le rapport complet