Système de types

Un système de types est un ensemble de règles qui attribue une propriété appelée type aux différentes constructions d'un programme informatique, telles que des variables, des expressions, des fonctions ou des modules. 

Ces types formalisent et appliquent les stratégies implicites que le programmeur utilise pour les types de données algébriques, les structures de données ou d'autres composants (par exemple, "chaîne", "tableau de float", "fonction retournant des booléens").

L’objectif principal d'un système de types est de réduire les risques de bogues dans les programmes informatiques  en définissant des interfaces entre différentes parties d'un programme, puis en vérifiant que les parties ont été connectées de manière cohérente. Cette vérification peut être effectuée de manière statique (au moment de la compilation), dynamique (au moment de l'exécution) ou sous la forme d'une combinaison de vérifications statiques et dynamiques. Les systèmes de types ont également d'autres objectifs, tels que l'expression de règles métier, l'activation de certaines optimisations du compilateur, l’envoi multiple, la fourniture d'une forme de documentation, etc.

Un système de types associe un type à chaque valeur calculée et, en examinant le flux de ces valeurs, tente de garantir ou de prouver qu'aucune erreur de type ne peut se produire. Le système de types en question détermine exactement ce qui constitue une erreur de type, mais l'objectif est généralement d'empêcher que des opérations attendant un certain type de valeur soient utilisées avec des valeurs pour lesquelles cette opération n'a pas de sens (erreurs de logique). Les systèmes de types sont souvent spécifiés dans les langages de programmation et intégrés dans les interpréteurs et les compilateurs correspondants; bien que le système de types d'une langue puisse être étendu par des outils optionnels qui effectuent des types de vérifications supplémentaires en utilisant la syntaxe et la grammaire de type d'origine de la langue.