Résumé
Après six cours consacrés aux langages impératifs, où l’opération de base est la modification d’un état, le septième cours a changé de paradigme et braqué le projecteur sur les langages fonctionnels, où les opérations de base sont l’abstraction et l’application de fonctions, comme dans le lambda-calcul. Pour faciliter la programmation, les langages fonctionnels ajoutent au lambda-calcul une stratégie de réduction ainsi que des types de données primitifs. On leur donne des sémantiques opérationnelles soit sous forme de réductions sous contextes, soit dans le style naturel. Nous avons mécanisé en Coq la syntaxe et la sémantique d’un petit langage fonctionnel, appelé « FUN », avec pour seule difficulté l’absence d’alpha-conversion, nous restreignant à l’évaluation faible de programmes clos.
Lorsqu’un langage offre plusieurs types de données, comme les fonctions et les booléens en FUN, des programmes absurdes apparaissent, comme true false (appliquer le booléen true comme si c’était une fonction). Le typage est un moyen de rejeter de tels programmes absurdes, dynamiquement (pendant l’exécution) ou statiquement (par analyse statique). Nous avons ajouté au langage FUN un système de types simples statiques, similaire au lambda-calcul simplement typé de Church. Pour démontrer la sûreté d’un système de types, c’est à dire le fait qu’aucun programme bien typé n’est absurde, plusieurs techniques existent suivant le style de sémantique utilisé : dénotationnelle, naturelle, ou à réductions. Dans ce dernier cas, la démonstration s’appuie sur deux propriétés reliant typage et réductions : la préservation (du typage par une réduction) et la progression (un programme bien typé est une valeur ou se réduit).
Le cours et la mécanisation ont suivi jusqu’ici une approche « extrinsèque » du typage, où le système de types s’applique comme un filtre sur un langage non typé. Une approche « intrinsèque » est également possible, où la syntaxe abstraite et la sémantique du langage ne sont définies que pour les termes bien typés. Il faut pour cela définir la syntaxe abstraite à l’aide de types dépendants, ou pour le moins de types algébriques généralisés (GADT). Le bénéfice de cette approche « intrinsèque » est qu’il est possible de définir une sémantique dénotationnelle du langage qui garantit par construction non seulement la sûreté du typage mais aussi la normalisation (tous les programmes bien typés terminent). Étendre cette approche à des langages et systèmes de types riches est un sujet de recherche encore actif.
