Site d’Emmanuel Saint-James
Philologie de la programmation
Du type à la preuve

Le contrôle de type consiste à vérifier, idéalement une fois pour toutes avant l’exécution, que toute opération s’applique à des arguments conformes. Ce contrôle est plus ou moins difficile selon les langages :

• pour les langages impératifs classiques, il est consiste essentiellement à vérifier que les opérations arithmétiques portent sur des variables déclarées numériques, c’est facile et c’est d’ailleurs apparu très tôt ;
• pour les langages dits fonctionnels ou s’en inspirant, les fonctions d’ordre supérieur induisent un contrôle plus abstrait, par exemple que deux variables sont de même type sans savoir lequel ;
• ce contrôle est limité par la théorie sous-jacente du lambda-calcul, toute fonction récursive n’y étant pas typable : pour éviter la référence en avant des appels récursifs, il faut donner la fonction en argument d’elle-même, d’où une circularité dans le calcul du type ;
• lorsque la récursivité n’est pas utilisée, l’utilisation d’un système de type peut prendre l’aspect d’une programmation par preuves, cas particulier de la programmation dite fonctionnelle ;
• certains langages vont jusqu’à interdire non seulement la récursivité mais aussi les boucles ayant un nombre d’itérations inconnu d’avance ; c’est le cas notamment des langages d’interrogation de bases de données, mais on perd alors en expressivité ;
• le contrôle de type revendique de s’occuper de la sémantique du langage, après son contrôle syntaxique vu précédemment ; mais il s’agit en fait de ne contrôler qu’une cohérence définie par le système de type, le sens du programme échappant à cette opération ;
• cette cohérence définit donc autoritairement un bon usage reflétant les limites des théories de types en cours ; c’est pourquoi que la capture de continuation et la réflexivité sont interdites dans les langages imposant le contrôle de type.