J'enseigne, en collaboration avec Xavier Leroy, le cours connu sous le numéro 2-4-2 au sein du MPRI. Mon objectif est principalement de décrire le système de types de Hindley et Milner, qui sert de fondation aux langages de programmation de la famille ML, dont Standard ML, Objective Caml et Haskell. Je présenterai ce système de types, son algorithme d'inférence de types, ainsi qu'un certain nombre de leurs extensions.
Consultez également la page maintenue par Xavier Leroy à propos de ce cours.
Le cours ne s'appuie pas explicitement sur un texte particulier. En particulier, le plan du cours, que l'on trouvera ci-dessous, ne correspond exactement à aucune des références bibliographiques que je propose. Néanmoins, celles-ci constituent un bon accompagnement au cours.
J'ai écrit récemment un embryon de nouvelles notes de cours dans lesquelles, pour l'instant, on ne trouve pas grand-chose, si ce n'est la démonstration du lemme de stabilité du typage par substitution (de types pour des variables de types), écrite en accordant une attention particulière aux arguments de renommage.
À ceux que le typage intéresse, je recommande fortement la lecture de tout ou partie de l'ouvrage Types and Programming Languages (TAPL), de Benjamin C. Pierce. Ce livre est accessible et très complet. En particulier, l'équivalent des chapitres 1 à 14 (lambda-calcul simplement typé) et 22 (inférence de types) sera soit supposé connu soit traité en cours.
Nous aborderons également en cours plusieurs sujets absents de TAPL: en particulier, l'inférence de types à la ML (donc avec polymorphisme) et l'inférence de types à base de contraintes. Le second chapitre de mon mémoire d'habilitation (HDR) constitue une brève introduction à ces questions. Ensuite, pour approfondir, on pourra se plonger dans The Essence of ML Type Inference (EMLTI). Ce chapitre, écrit par Didier Rémy et moi-même, est paru dans Advanced Topics in Types and Programming Languages. Il contient une présentation assez détaillée du système de types du langage ML, et s'attache à décrire de façon élégante un algorithme efficace d'inférence de types.
Je n'aurai probablement pas le temps d'aborder en cours deux aspects importants du langage Objective Caml, à savoir le système de modules et le système de classes et objets. Tous deux sont décrits dans les notes de cours de Didier Rémy, intitulées Using, Understanding, and Unraveling the OCaml Language, dont je conseille la lecture. On peut également se référer aux articles qui décrivent de façon formelle l'essentiel de ces systèmes, à savoir A Modular Module System, de Xavier Leroy, en ce qui concerne les modules, et Objective ML: An effective object-oriented extension to ML, de Didier Rémy et Jérôme Vouillon, en ce qui concerne les classes et objets.
Les notes de cours de DEA de l'année 2002-2003 sont encore disponibles, pour ceux que cela intéresserait, mais ne seront plus mises à jour. Vous pouvez consulter le code correspondant aux exercices de programmation des chapitres 1, 2, 3, 5, et 6, ainsi que celui correspondant à l'algorithme d'unification du chapitre 7.
Ce plan prévisionnel sera révisé au fur et à mesure si besoin.