Bibliographie & annexes
Présentation
En anglais
RÉSUMÉ
Le typage dans les langages de programmation garantit l’absence de calculs erronés qui seraient dus à des opérations manipulant des données non-conformes. Cette vérification peut s’effectuer à l’exécution (typage dynamique) ou à la compilation (typage statique) et accroît la sûreté d’exécution des programmes. Le typage permet aussi de s’abstraire de la représentation des données pour faciliter la composition des éléments d’un programme tout en apportant un bon niveau de flexibilité grâce aux différentes classes de polymorphisme (paramétrique, ad hoc, sous-typage). Chaque langage de programmation possède sa propre discipline de typage afin d’assurer sûreté, abstraction et flexibilité des programmes.
Lire cet article issu d'une ressource documentaire complète, actualisée et validée par des comités scientifiques.
Lire l’articleABSTRACT
Typing in programming languages rules out faults in computations due to operations using inadequate data. This verification may take place either at runtime (dynamic typing) or during compilation (static typing) and increases program security. Through abstraction, typing makes it possible to hide some implementation details in order to smooth the composition of different components of a program while allowing some flexibility through different kinds of polymorphism (parametric, ad hoc, subtyping). Each programming language has its own typing discipline that aims to ensure safety, abstraction, and flexibility of programs.
Auteur(s)
-
Emmanuel CHAILLOUX : Professeur, Sorbonne Université
-
Romain DEMANGEON : Maître de conférences, Sorbonne Université
-
Michel MAUNY : Directeur de recherche, Inria
INTRODUCTION
En programmation, un type de données ou, plus simplement, un type, est un ensemble de données partageant des propriétés et des opérations. Par exemple, dans le langage C, le type int des entiers contient les nombres positifs ou négatifs représentables sur un nombre fixe de bits, qui peut dépendre de l’architecture du processeur (souvent 32 ou 64). Ces entiers peuvent être arguments ou résultats d’opérations arithmétiques. Le langage OCaml fournit un type bool ne contenant que les deux valeurs de vérité true et false, qui peuvent être testées (par une construction conditionnelle if−then−else), ou être résultats de fonctions à valeurs booléennes.
L'expertise technique et scientifique de référence
MOTS-CLÉS
KEYWORDS
Computer | programming | type checking | language
DOI (Digital Object Identifier)
Cet article fait partie de l’offre
Technologies logicielles Architectures des systèmes
(239 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Présentation
Conclusion
En anglais
5. Autres systèmes de types
Le typage dynamique, en vérifiant que les arguments passés à une fonction sont (de types) acceptables, garantit que les opérations exécutées le sont sur des données correctes, du point de vue des types. Pour cela, des tests sur les données transmises sont effectués avant l’appel à une fonction ou bien directement dans son code. Si l’un de ces tests de conformité de type échoue, cet échec est signalé soit en transmettant une valeur spécifique à l’appelant, soit en déclenchant une exception à cet endroit du programme. On obtient donc une garantie de fiabilité logicielle indiquant qu’il n’y aura pas de calculs sur des données non conformes à ce qui est attendu.
Le typage statique élimine les tests de typage à l’exécution en analysant le code source du programme pour vérifier qu’il est conforme au système de types du langage dans lequel ce programme est écrit. Si ce n’est pas le cas, le programme ne sera pas compilé et ne pourra donc pas être exécuté. Si c’est le cas, le compilateur peut alors traduire le programme source vers du code machine, en tirant parti de la correction de son système de types pour, en particulier, ne pas effectuer de tests de types comme ceux vérifiant la conformité des arguments passés à une fonction.
Dans ce cadre, un langage typé statiquement est dit fortement typé si le compilateur n’accepte aucune erreur de typage. En cas de succès, la correction du typage garantissant que le code engendré sera dépourvu d’erreur de type, le compilateur n’introduira aucun test de type dynamique.
Tant dans les langages typés dynamiquement que dans ceux qui sont typés statiquement, il peut être demandé au programmeur d’écrire des informations pour la vérification du typage. Pour les premiers, il lui est demandé d’écrire explicitement des tests de type qui vérifient la conformité des valeurs manipulées. Pour les seconds, le programmeur indique les types des variables et paramètres à l’endroit de leur déclaration. Néanmoins, dans un système de types riche, par exemple avec des types paramétrés et fonctionnels, il peut devenir pénible de devoir systématiquement fournir ces annotations. Pour cela, le compilateur peut décharger le programmeur de tout ou partie de ces annotations en déterminant automatiquement un type compatible avec le source du programme et son système de types. On parle alors d’inférence de types.
D’autres langages à...
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Technologies logicielles Architectures des systèmes
(239 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Autres systèmes de types
BIBLIOGRAPHIE
-
(1) - MILNER (R.) - A theory of type polymorphism in programming. - J. Comput. Syst. Sci (1978).
-
(2) - WRIGHT (A.K.) - Polymorphism for imperative languages without imperative types. - Technical Report TR93-200, Rice University Dept. of Computer Science (1993).
-
(3) - PIERCE (B.) - Types and Programming Languages MIT Press. - (2002).
DANS NOS BASES DOCUMENTAIRES
ANNEXES
-
Type abstrait (Wikipedia) : https://fr.wikipedia.org/wiki/Type_abstrait
-
Polymorphisme (Wikipedia) : https://fr.wikipedia.org/wiki/Polymorphisme_(informatique)
-
Sûreté du typage (Wikipedia en anglais) : https://en.wikipedia.org/wiki/Type_safety
-
Langages des exemples :
-
OCaml : https://ocaml.org/
-
Swift : https://swift.org/
-
Java : https://www.java.com/
-
JavaScript : https://fr.wikipedia.org/wiki/JavaScript
-
C (Wikipedia) : https://fr.wikipedia.org/wiki/C_(langage)
-
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Technologies logicielles Architectures des systèmes
(239 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
