17/01/2008
Didier Rémy (INRIA)
MLF, réexpliqué

MLF est un système de type qui généralise le Système F tout en permettant l'inférence de type comme dans le langage ML. Les types des paramètres de fonctions utilisés de façon monomorphe, toutes les abstractions et toutes applications de types sont inférés. Les paramètres de fonctions utilisées de façon polymorphe et seulement ceux-ci doivent être annotés.

La première présentation de MLF, bien que simple du point de vue de l'utilisateur, était lourde, peu modulaire et assez peu intuitive pour le concepteur.

Dans cet exposé, je vous raconterai l'histoire de MLF dans sa version moderne, en utilisant une représentation graphique des types et en m'appuyant sur une interprétation des types de MLF comme des ensembles de types du système F. Cette approche éclaire les faces cachées de la présentation d'origine, souligne bien mieux les liens très étroits avec le le langage ML. Elle débouche également sur des algorithmes d'unification et d'inférence de type qui généralisent ceux de ML tout en préservant leur complexité.

NB: Cet exposé s'appuie sur des travaux en collaboration avec Didier Le Botlan et Boris Yakobowski.