Polymorphisme à tous les étages ! Du système F au calcul des constructions

Résumé

La correspondance de Curry-Howard n’est-elle qu’une agréable coïncidence entre une logique intuitionniste et un lambda-calcul typé tous deux peu expressifs ? De nombreuses extensions qui apparaissent dans les années 1970 et 1980 montrent que ce n’est pas le cas.

Le typage polymorphe est la première de ces extensions. Il apparaît indépendamment dans les travaux de Girard (1971) et de Reynolds (1974). Reynolds est un informaticien et cherche à assouplir le typage du lambda-calcul de manière à pouvoir typer des fonctions génériques comme le tri, qui appliquent un même algorithme à des données de différents types. Girard est un logicien qui cherche une interprétation fonctionnelle (comme l’interprétation BHK) pour l’arithmétique du second ordre, une logique suffisamment puissante pour exprimer l’analyse. Ils convergent sur le même système de types, appelé lambda-calcul polymorphe par Reynolds et système F par Girard, qui se révèle extrêmement expressif.

D’autres formes de polymorphisme apparaissent ensuite : les constructeurs de types (types paramétrés par des types) et les types dépendants (types paramétrés par des termes). Ces formes de paramétrisation s’ajoutent à celles du lambda-calcul (termes paramétrés par des termes) et de système F (termes paramétrés par des types), débouchant sur des formalismes inutilement complexes.

Une « grande unification » apparaît dès le début des années 1970 avec la théorie intuitionniste des types de Martin-Löf, suivie en 1986 par le calcul des constructions de Coquand et Huet, puis en 1988 par les Pure Type Systems de Berardi. Les types et les termes partagent la même syntaxe ; un seul lambda et une seule application traitent toutes les formes de paramétrisation. Cependant, identifier entièrement types et termes via un type de tous les types, comme dans une première version de la théorie des types de Martin-Löf, mène à l’incohérence logique. Il reste nécessaire de stratifier types et termes, ce qui se fait à l’aide d’univers. De nombreux systèmes de types intéressants s’obtiennent en variant le nombre et les relations entre univers.

En l’espace de vingt ans, la correspondance de Curry-Howard s’est non seulement étendue à des logiques et des langages typés très expressifs, mais encore a inspiré des systèmes formels utilisables à la fois comme logiques et comme langages de programmation, tels la théorie des types de Martin-Löf et le calcul des constructions.