Résumé
On s’attend à ce qu’un type abstrait puisse être réalisé par différents types concrets sans que les utilisateurs du type abstrait observent de différences. C’est le principe d’indépendance vis-à-vis des représentations énoncé par Reynolds en 1983. Symétriquement, on s’attend à ce qu’une fonction polymorphe exécute le même algorithme lorsqu’on l’applique à des données de différents types.
La théorie de la paramétricité donne un sens mathématiquement précis à ces intuitions. Elle s’appuie sur la notion de relations logiques : des relations entre termes, indexées par des types, et compatibles avec la structure des types. En particulier, deux fonctions sont reliées au type τ → σ si et seulement si elles envoient des arguments reliés au type τ sur des résultats reliés au type σ. Ces relations logiques ont été introduites par Plotkin pour l’étude du lambda-calcul simplement typé. Reynolds étend les relations logiques au cas des types abstraits, lui permettant de formaliser et de démontrer le principe d’indépendance vis-à-vis des représentations. L’extension au lambda-calcul polymorphe est plus délicate car il est facile de tomber dans des définitions circulaires, mais est finalement résolue vers 1990 par Bruce, Meyer et Mitchell, en s’inspirant de la technique des candidats de réductibilité de Girard.
Une application spectaculaire de la paramétricité est les Theorems for free (théorèmes gratuits), titre d’un célèbre article de Wadler (1991). Toutes les fonctions du système F ayant un certain type polymorphe vérifient des équations qui ne dépendent que du type ; il est inutile de redémontrer ces équations pour chaque fonction. Ainsi, toute fonction f : ∀α. α → α vérifie f x = x et est donc l’identité. La paramétricité permet aussi de démontrer l’isomorphisme entre un type inductif et son codage fonctionnel mentionné au 3e cours.
Les travaux récents de Bernardy et de Lasson montrent que la paramétricité non seulement s’étend à la théorie des types, mais encore peut s’internaliser dans cette théorie. Un type A se traduit mécaniquement en une relation RA qui est la relation logique au type A ; un terme clos a : A se traduit en une preuve que a est relié à lui-même par RA. L’approche s’étend naturellement aux constructeurs de types et aux types dépendants.
