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é !
