Didier Le Botlan — Travail de thèse : MLF

J'ai effectué ma thèse sous la direction de Didier Rémy, dans le projet CRISTAL à l'INRIA Rocquencourt. Elle s'intitule MLF : une extension de ML avec polymorphisme de second ordre et instanciation implicite

Contexte

Haskell et OCaml sont des langages fonctionnels typés dont la théorie, baptisée ML, date des années 80 (Luis Damas, Robin Milner, 1982). La qualité essentielle de ML est de permettre une forme de polymorphisme limitée, dite de seconde classe. En pratique, le polymorphisme de seconde classe permet d'écrire de nombreuses fonctions très utiles, et de vérifier automatiquement qu'elles sont bien typées. Citons par exemple les itérateurs (pour parcourir une structure de données), les opérations de transformation (les tris de tableaux ou de listes), et plus généralement toutes les fonctions liées aux structures de données (création, insertion d'éléments, accès).

Bien que ML soit un langage très expressif, il arrive des situations où la limitation sur le polymorphisme empêche de réaliser certaines constructions plus génériques et donc plus modulaires. Pour y parvenir, il faudrait du polymorphisme de première classe, comme dans le langage Système F (Jean-Yves Girard, 1972). Pour paraphraser Simon Peyton Jones, on peut écrire des programmes entiers en ML sans ressentir le besoin de polymorphisme de première classe, mais quand on commence à en avoir besoin, on ne peut plus y échapper. De fait, ML souffre d'une limitation : il n'est pas toujours possible d'abstraire par rapport à une valeur du langage. Cette limitation intrinsèque est un frein à la modularité. Si mon code utilise une fonction de tri, j'aurai peut-être envie, à l'avenir, d'abstraire cette fonction, i.e. de la remplacer par un paramètre. ML ne permet pas cela avec les fonctions polymorphes.

Depuis les années 80, de nombreux chercheurs visent à étendre ML avec du polymorphisme de première classe, c'est-à-dire à réconcilier ML et le Système F. Citons Boehm (1985), Giannini et Ronchi Della Rocca (1988), Pfenning (1988, 1993), Rémy (1994), Läufer et Odersky (1994, 1996), Wells (1994), Kfoury et Wells (1994, 1999), Schubert (1998), Pierce et Turner (1998), Garrigue et Rémy (1999), Odersky et Zenger et Zenger (2001), Vytiniotis et Weirich et Peyton Jones (2006).

Exposé du problème

En bref, il s'agit de combiner ML et le Système F. Le Système F est un langage issu de la logique, qui est en pratique inutilisable comme langage de programmation. En effet, un programme Système F doit inclure de très nombreuses annotations de types, qui compliquent la tâche du programmeur de manière inacceptable. Plus précisément, un programme Système F doit mentionner les abstractions de types, les applications de types et les annotations sur les arguments. Au contraire, un programme ML ne mentionne aucune de ces annotations. Le compilateur ML est capable de les inférer automatiquement, et de vérifier que le programme est bien typé. Rappelons que ML se limite au polymorphisme de seconde classe, ce qui simplifie l'inférence.

En 1994, soit plus de vingt ans après la formalisation du Système F, et dans la lignée de nombreux travaux sur la question, Joe Wells montre que le problème de l'inférence dans le Système F est indécidable. En clair, on ne pourra pas effacer toutes les annotations de types du Système F. Les travaux mentionnés ci-dessus requièrent donc des annotations dans les programmes, mais en s'efforçant de limiter leur volume. Différentes approches ont été développées, malheureusement, aucune des solutions proposées n'est satisfaisante : le programmeur doit toujours fournir un volume d'annotations trop important pour être acceptable.

L'objectif de ma thèse était de parvenir à une solution utilisable en pratique. Le point de départ était un travail précédent par Didier Rémy et Jacques Garrigue (1999).

Résultats

Le langage obtenu, MLF, est une extension de ML : tout programme ML reste typable tel quel. De plus, il permet le polymorphisme de première classe (de second ordre), comme dans le Système F. Le volume d'annotations de types requis est minimal : les abstractions de types et les applications de types sont toutes inférées, et seules les arguments utilisés de manière polymorphe doivent être annotés. Bref, il est facile de programmer en MLF : peu d'annotations sont nécessaires, et l'emplacement des annotations obligatoires est intuitif.

MLF est un système de types, i.e. une théorie, qui est prouvée correcte : un programme bien typé ne provoque pas d'erreur d'exécution. De plus, un algorithme d'inférence et un algorithme d'unification sont donnés. Tous deux ont été implémentés dans un prototype du langage, et prouvés corrects et complets.

MLF peut être vu comme une généralisation de ML, les deux systèmes ayant les mêmes propriétés essentielles. Ainsi, comme ML, MLF possède des types principaux. Ce parallèle va plus loin : les algorithmes d'inférence et d'unification ont exactement la même structure dans les deux langages. Mieux, on retrouve les algorithmes de ML (connus depuis 1982) comme cas particuliers de ceux de MLF.

Technique

MLF généralise ML en associant à chaque variable de type une borne. On distingue deux types de bornes : les bornes flexibles et les bornes rigides. Les premières s'écrivent (α ≥ σ), ce qui signifie que la variable α est une instance de σ. Les secondes s'écrivent (α = σ), ce qui signifie que la variable α est égale à σ, modulo une opération de partage appelée abstraction.

L'ensemble des variables d'un jugement de typage doit apparaître dans un préfixe, qui regroupe toutes les contraintes (bornes flexibles ou rigides) sur les variables. Quand une variable est quantifiée, sa borne doit être indiquée.

Comparaison entre ML et MLF

Dans ML	Dans MLF
α	α ≥ σ	α = σ
∀ α	∀ (α ≥ σ)	∀ (α = σ)

Quelques exemples de MLF en pratique sont disponibles sur la page de présentation du prototype.

MLF, les suites

Le travail sur MLF ne s'arrête pas avec ma thèse. Plusieurs travaux continuent à enrichir ce système. Ils sont détaillés sur ma page Recherche.