Vous pouvez trouver ici une brève description de quelques-uns de mes travaux de recherche.
La recherche théorique sur les langages de programmation a fait naître des langages dont la sémantique est beaucoup mieux comprise. Par exemple le langage Objective Caml, développé à l'INRIA (projet Cristal) se base sur des fondements solides (langage fonctionnel, typage...), ce qui lui permet d'offrir au programmeur un grand confort de programmation et donc rapidité de développement et plus grande fiabilité des applications. Tout en étant un descendant du lambda-calcul et du Lisp, ce langage a su s'adapter aux exigences concrètes des développeurs en privilégiant la rapidité de l'exécution des programmes et en incorporant de manière très propre des concepts issus des besoins pragmatiques de l'industrie, comme les modules, pour la programmation séparée, et les objets.
Le but de notre domaine de recherche est donc de donner aux programmeurs les bons outils, leur permettant de programmer mieux. C'est-à-dire notamment programmer plus rapidement, en diminuant les risques d'erreurs, en augmentant la réutilisabilité du code. Alors que les travaux théoriques se sont penchés jusqu'à présent surtout sur le calcul à petite échelle, l'enjeu se place maintenant de plus en plus sur l'assemblage de composants de grande taille : processus ou tout simplement bibliothèques de fonctions, auxquelles on accède à travers des interfaces bien définies.
Différents paradigmes ont été développés pour répondre à ce genre de problèmes, parmi lesquels :
La programmation par spécialisation (ou évaluation partielle) est une technique qui permet de générer automatiquement le code de versions spécialisées d'un programme générique pour des données particulières. Par exemple on peut imaginer écrire ainsi automatiquement des pilotes de périphérique à partir d'un pilote générique et des spécifications de chaque matériel.
L'évaluation partielle dirigée par les types (Type Directed Partial Evaluation, Olivier Danvy, nommée plus loin « TDPE ») est un algorithme très ingénieux permettant la spécialisation de programmes. Il est aussi appelé normalisation par évaluation et est issu de fondements théoriques très forts. TDPE utilise une approche entièrement dirigée par le type, par oppositions aux techniques plus classiques d'évaluation partielle, dites « on-line », lorsqu'elles déterminent automatiquement les portions de code à normaliser au vol, ou bien « off-line » lorsqu'elles sont basées sur une analyse statique du code source du programme, afin de repérer les parties pouvant être réduites. Une des spécificités de TDPE est de permettre de spécialiser des fonctions compilées, alors que les autres approches partent du code source d'un programme. Outre le comportement (assez surprenant) proche d'un décompilateur, cela a pour avantage de rendre la spécialisation plus rapide (puisque c'est l'exécution d'un programme compilé), ce qui est intéressant lorsque la spécialisation doit avoir lieu au moment de l'exécution. Un autre avantage est la possibilité d'utiliser les mêmes composants compilés que ce soit pour l'utilisation ou la spécialisation, laissant donc le choix à l'utilisateur (ou au programme client).
J'ai réalisé plusieurs implémentations de TDPE pour le langage Objective Caml afin de tester les différentes techniques d'implémentation. Quelques problèmes théoriques restent à résoudre pour rendre cet outil utilisable pour des programmes réels. Je suis en train de travailler notamment sur la prise en compte des types récursifs, fonctions récursives et effets de bord. J'envisage de rendre publique une implémentation d'ici quelques mois.
L'idée de considérer les types modulo une certaine relation d'équivalence permet de ne pas se préoccuper de détails non-essentiels comme par exemple l'ordre des paramètres d'une fonction. Cela peut être utile par exemple lors de la recherche de fonctions par leur type dans des bibliothèques (voir par exemple l'outil CamlSearch développé par Jérôme Vouillon et Roberto Di Cosmo pour le langage CamlLight). Grâce à la correspondance de Curry-Howard qui fait un parallèle entre preuve et programme, le même principe pourrait servir à chercher des énoncés de théorèmes. Un autre application, qui a été utilisée par IBM dans le projet Mocking Bird, consiste à faciliter l'inter-opérabilité entre langages, en permettant l'utilisation des données d'un programme par un autre, écrit dans un langage différent.
Les isomorphismes de types avaient été étudiés jusque là dans des cadres restreints et notamment celui du lambda-calcul typé avec paires surjectives, ce qui correspond à des langages fonctionnels comportant des types « produits cartésiens », ou encore aux isomorphismes entre objets d'une catégorie cartésienne fermée. Dans ce cas, il existe une axiomatisation simple des isomorphismes, ce qui permet de les utiliser très facilement.
Pendant ma thèse je me suis penché sur le problème des isomorphismes dans le cadre plus général des types avec sommes fortes, correspondant aux catégories bicartésiennes fermées. J'ai pu montrer que dans ce cas, il n'est plus possible de trouver une axiomatisation finie. Ce travail a débouché sur un article publié à LICS en 2002 en collaboration avec Roberto Di Cosmo (PPS, Paris 7) et Marcelo Fiore (Cambridge).
Pour trouver ce résultat, nous avons tiré partie de travaux de théorie des nombres. Il est assez surprenant en effet de remarquer que cette question d'informatique a des liens très étroits avec un problème connu sous le nom de problème des égalités du lycée de Tarski (Tarski high-school algebra problem), ce qui lui donne un intérêt théorique majeur. Alfred Tarski s'est demandé en 1969 si les égalités apprises au lycée (associativité commutativité, distributivité, etc.) permettent de montrer toutes les égalités entre expressions arithmétiques. Charles Martin a montré que la réponse est positive si l'on se limite à des expressions arithmétiques avec produit, puissance, constante 1 et variables numériques. Si l'on remplace les variables par des variables de types, le 1 par le type unité et le produit et la puissance respectivement par les types produit et flèche, on obtient exactement les isomorphismes de types correspondant au cas des catégories cartésiennes fermées ! Je me suis bien entendu demandé si ce mystérieux parallèle se poursuivait en présence de sommes. R. Gurevic a montré que dans ce cas, en arithmétique, il n'existait aucune axiomatisation finie des égalités. Nous avons pu montrer grâce à ses travaux qu'il en était de même pour les isomorphismes de types.
Le travail sur les égalités de Gurevic nous a amené à manipuler des termes très complexes. L'utilisation de TDPE pour prouver ces isomorphismes ont mis en évidence les problèmes de normalisation du lambda-calcul avec sommes fortes. Pour les résoudre, nous avons :