Résumé
Le 3e cours a introduit les types et prédicats inductifs, un mécanisme général pour définir et raisonner sur les structures de données finies. Comment faire de même pour les structures de données potentiellement infinies, par exemple les flux (streams) ou les graphes vus comme des arbres infinis ? On parle alors de types et de prédicats coinductifs.
Dans la présentation ensembliste classique, les types coinductifs correspondent à des plus grands points fixes d’opérateurs croissants, alors que les types inductifs sont des plus petits points fixes. La théorie des types suit une autre présentation, en termes d’arbres bien fondés (toute branche est finie) pour le cas inductif et possiblement mal fondés (avec des branches infinies) pour le cas coinductif. Un critère de garde garantit la bonne formation des définitions : récursions structurelles pour le cas inductif, corécursions productives pour le cas coinductif.
Une présentation plus moderne et d’inspiration plus algébrique caractérise les types inductifs comme engendrés par leurs constructeurs (nil et cons pour les listes), et les type coinductifs comme engendrés par leurs observations (projections) (head et tail pour les flux). Cette présentation débouche sur un élégant style de programmation à base de cofiltrage et de copatterns (Abel et al., 2013).
Le cours a présenté deux des nombreuses applications de la coinduction : la monade de partialité (Capretta, 2005) qui permet de définir des récursions générales en théorie des types et de raisonner coinductivement sur leur terminaison ou leur divergence, et la modélisation de la programmation réactive à l’aide de fonctions causales sur les flux de données.
