Systèmes de types
Les systèmes de types sont des disciplines formelles qui classifient les expressions de programme selon les types de valeurs qu'elles calculent, permettant d'éliminer de larges catégories d'erreurs avant l'exécution d'un programme.
Definition
Un système de types est une méthode syntaxique traitable permettant de prouver l'absence de certains comportements de programme en classifiant les expressions selon les types de valeurs qu'elles calculent.
Scope
Ce domaine couvre la théorie et la conception des systèmes de types : le typage statique versus dynamique, le polymorphisme paramétrique et ad hoc, le sous-typage, l'inférence de types, et les systèmes avancés tels que les types dépendants et substructurels. Il aborde la sûreté des types (type soundness), la relation entre les types et la logique via la correspondance de Curry-Howard, et la manière dont les disciplines de typage arbitrent entre l'expressivité, les garanties et la décidabilité.
Sub-topics
Core questions
- Quelles garanties un système de types offre-t-il, et qu'est-ce que la sûreté des types ?
- Comment le polymorphisme et le sous-typage augmentent-ils l'expressivité sans sacrifier la sécurité ?
- Les types peuvent-ils être inférés automatiquement, et quand l'inférence est-elle décidable ?
- Jusqu'où les types peuvent-ils encoder des propriétés de programme riches, voire des spécifications complètes ?
Key theories
- Sûreté des types via le progrès et la préservation
- L'approche syntaxique de Wright et Felleisen prouve la sûreté d'un système de types en établissant que les programmes bien typés ne se bloquent pas : les types sont préservés lors de l'évaluation et les termes bien typés peuvent toujours progresser.
- Typologie du polymorphisme et de l'abstraction
- Cardelli et Wegner organisent l'espace des concepts de typage, distinguant le polymorphisme paramétrique et ad hoc, l'inclusion (sous-typage) et l'abstraction de données au sein d'un cadre unifié.
- La théorie des types comme fondement des langages de programmation
- Harper développe une méthodologie uniforme de statique et de dynamique dans laquelle les fonctionnalités du langage sont définies par des règles de typage et d'évaluation, traitant la théorie des types comme le fondement organisateur de la conception des langages.
Clinical relevance
Les systèmes de types comptent parmi les méthodes formelles les plus largement déployées : ils détectent les erreurs à la compilation, documentent les interfaces, permettent un refactoring sécurisé et alimentent les outils d'édition. Des avancées telles que les génériques, le typage graduel et les types de propriété (ownership types) ont été directement intégrées dans les langages industriels courants.
History
Les langages typés sont apparus avec des systèmes précoces comme Algol et le lambda-calcul simplement typé. L'inférence de types polymorphe de Milner (1978) a servi de base à ML ; Girard et Reynolds ont indépendamment conçu le Système F pour le polymorphisme paramétrique. L'étude de Cardelli et Wegner de 1985 a systématisé le domaine, et la méthode de progrès et préservation (1994) est devenue la technique standard de sûreté que Pierce et Harper ont ensuite canonisée dans des manuels.
Debates
- Typage statique versus typage dynamique
- Un débat de longue date met en balance la détection précoce des erreurs et la documentation du typage statique par rapport à la flexibilité et l'itération rapide du typage dynamique, le typage graduel étant proposé comme une réconciliation.
Key figures
- Benjamin Pierce
- Robert Harper
- Luca Cardelli
- Robin Milner
- Matthias Felleisen
Related topics
Seminal works
- pierce2002
- harper2016
- cardelli1985
- wright1994
Frequently asked questions
- Que signifie pour un système de types d'être sûr ?
- La sûreté signifie que les programmes bien typés ne peuvent pas présenter les erreurs que le système de types est conçu pour prévenir, généralement prouvée en montrant que les types sont préservés pendant l'évaluation et que les programmes bien typés ne se bloquent jamais.
- Les langages à typage dynamique ont-ils des systèmes de types ?
- Ils possèdent des types et effectuent des vérifications de types à l'exécution, mais ils sont dépourvus d'un système de types statique qui rejette les programmes mal typés avant l'exécution ; les erreurs de type se manifestent plutôt comme des défaillances à l'exécution.