Avertissement

Jusqu'en 2009-2010, j'ai enseigné, en collaboration avec Giuseppe Castagna et Didier Rémy, le cours 2-4-2 du MPRI.

En 2010-2011, je n'enseigne plus mais m'occupe du projet de programmation. Cette page reste pour le moment en l'état et propose diverses ressources datant des années précédentes.

Programmation fonctionnelle et systèmes de types

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, OCaml 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. Je consacrerai également un certain temps à des techniques de compilation préservant le typage.

En 2006-2007 et 2007-2008, Xavier Leroy a participé à ce cours; ses transparents sont toujours en ligne.

Plan du cours (2009-2010)

  1. Types simples: sûreté du typage; paires, sommes, récursivité (15 septembre 2009).
  2. Types simples, suite: références; inférence de types (22 septembre 2009, séance assurée par Didier Rémy).
  3. Polymorphisme: le système F; le système de Damas et Milner (29 septembre 2009).
  4. Polymorphisme, suite: sûreté du typage pour ML, puis pour ML avec références (6 octobre 2009).
  5. Inférence de types à base de contraintes pour ML (13 octobre 2009).
  6. Extensions diverses: annotations de types; récursivité polymorphe; unification sous préfixe mixte; types récursifs et types algébriques (20 octobre 2009).
  7. Types existentiels (27 octobre 2009).
  8. Closure conversion préservant le typage (3 novembre 2009).
  9. Giuseppe Castagna, sous-typage (24 novembre, 1er, 8 et 15 décembre 2009).
  10. Didier Rémy, modularité, (5, 12, 19 et 26 janvier 2010).

Projet

L'évaluation des étudiants s'effectue pour partie via un partiel et un examen écrits, pour partie via un projet de programmation.

Références bibliographiques

Le cours ne s'appuie pas explicitement sur un texte particulier. En particulier, le plan du cours 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 début 2007 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 pas le temps d'aborder en cours deux aspects importants du langage OCaml, à 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.

Devoirs à la maison

Sujets et corrigés des précédents examens

2006-2007 était un bon cru.


EnglishPage principale Email Dernière modification : 06 January 2017