Des armes de construction massive : types inductifs et prédicats inductifs

Résumé

Le cours a débuté par un historique des types de données dans les langages de programmation : tableaux en Fortran, enregistrements (records) en Cobol, unions disjointes en Algol 68, références et pointeurs en Algol W, ainsi que les types universels des S-expressions en Lisp et des termes en Prolog. Les types algébriques, introduits dans le langage HOPE et popularisés par ML et Haskell, unifient toutes ces notions. Les types algébriques sont des sommes de produits, récursives et nommées. Ils peuvent exprimer de nombreuses structures de données informatiques, ainsi que la conjonction et la disjonction dans une approche de Curry-Howard.

Les lambda-calculs étudiés dans les cours précédents ne fournissent pas de types de données, car ils peuvent être définis en termes de fonctions, généralisant l’astucieux codage fonctionnel des nombres entiers introduit par Church. Ce codage est bien typé dans les systèmes F et Fω, mais avec des restrictions sur les analyses de cas que l’on peut faire sur les données. Ainsi, on ne peut pas démontrer 0 ≠ 1 avec le codage de Church typé !

Pour dépasser ces restrictions, Paulin-Mohring et Pfenning introduisent en 1989 les types inductifs, une variante des types algébriques compatibles avec la théorie des types. En moins, la récursion est restreinte et une condition de positivité est ajoutée afin de préserver la normalisation forte et la cohérence logique. En plus, les types inductifs peuvent être dépendants. Par la correspondance de Curry-Howard, ils deviennent des prédicats inductifs, avec lesquels on peut définir les connecteurs logiques « et », « ou », « il existe ». Une extension naturelle, les familles inductives, permet d’exprimer tous les prédicats définissables par règles d’inférence, y compris l’égalité et les ordres bien fondés.

Le cheminement des idées continue : des types algébriques en programmation vers les types et familles inductifs en logique, puis retour en programmation avec les types algébriques généralisés, Generalized Algebraic Data Types (GADT). Imaginés par Augustsson et Petersson en 1994, puis intégrés dans Haskell en 2007 et OCaml en 2012, les GADT sont une extension des types algébriques permettant d’exprimer certaines propriétés des données dans le style des prédicats inductifs, incluant des égalités entre types et des quantificateurs existentiels, sans pour autant nécessiter toute la mécanique des types dépendants.

La recherche autour des types inductifs reste active : quelles sont les bonnes conditions de garde qui garantissent la normalisation ? Peut-on identifier des valeurs d’un type inductif, réalisant ainsi le quotient de ce type par une relation d’équivalence ? Le dixième cours est revenu sur cette dernière question.