Résumé
De nombreux langages de programmation utilisent le typage statique pour garantir, avant toute exécution du programme, des propriétés de sûreté de l'exécution telles que l'intégrité des structures de données. Au début de ce septième cours, nous avons montré comment des systèmes de types bien connus (types simples et polymorphisme paramétrique) s'étendent aux structures de contrôle évoluées : exceptions, gestionnaires d'effets, continuations non délimitées (opérateur call/cc), et continuations délimitées (opérateur cupto). Cette extension se fait sans grande peine à condition de déclarer explicitement les types des exceptions, des effets ou des points de programmes (prompts) avant utilisation, et de restreindre la généralisation des variables de types aux expressions qui sont des valeurs.
Le cours a ensuite abordé le problème des programmes qui s'arrêtent prématurément sur une exception non rattrapée ou un effet non géré. Nous avons passé en revue plusieurs mécanismes linguistiques qui ont été proposés pour maîtriser ces risques : les déclarations d'exceptions avec vérification dynamique (CLU, C++) ; les déclarations d'exceptions avec vérification statique (Java) ; et l'utilisation de capacités pour restreindre les levées d'exceptions (Scala 3). Enfin, nous avons introduit les systèmes de types et d'effets, qui gardent trace non seulement des valeurs possibles des expressions mais aussi des effets de bord que leur évaluation peut déclencher, et développé un tel système pour un langage avec effets algébriques, gestionnaires d'effets et polymorphisme de rangée.
